add vertex/edge access theorems to iset.mm #5139

jkingdon · 2025-12-16T19:24:02Z

This ended up a lot longer than I expected, but there's always a lot of machinery involved in extensible structures, and in this case the definition (unaltered from set.mm) allows either an extensible structure or an ordered pair of vertexes and edges.

Most of the discouraged theorems are also discouraged in set.mm, although I did re-intuitionize 2strstr to reflect changes in set.mm since the first one, and that accounts for a few of the entries.

One of the biggest differences from set.mm is that 2o ~<_ A is well behaved, in iset.mm, for saying a set has at least two elements (https://us.metamath.org/mpeuni/rex2dom.html is provable and is added here) whereas 2 <_ ( # ` A ) is not (at least with current theorems, # works on finite sets or on infinite sets, but not on arbitrary sets).

avekens · 2025-12-23T06:55:34Z

iset.mm

+      ( vf wcel w3a wf1o wa cen wbr cv wex f1oeq1 spcegv imp 3ad2antl1 wb breng
+      3adant1 adantr mpbird ) CDHZAEHZBFHZIZABCJZKABLMZABGNZJZGOZUEUFUIUMUGUEUI
+      UMULUIGCDABUKCPQRSUHUJUMTZUIUFUGUNUEABGEFUAUBUCUD $.
+    $( $j usage 'f1oen4g' avoids 'ax-un'; $)


'ax-rep' and 'ax-pow' shold be added (as mentioned in the comment).

Hmm, interesting. Totally agree that the comment should match the $j usage. Looks like we can add 'ax-coll' for both f1oen4g f1dom4g. But ax-pow is used in f1oen4g (via breng) and f1dom4g (via brdom2g) so I'll adjust the comment.

In set.mm, we have $( $j usage 'f1oen4g' avoids 'ax-pow' 'ax-rep' 'ax-un'; $).
And ~breng does not use ~ax-pow in set.mm.
So things are diffent in set.mm and iset.mm...

iset.mm

avekens

Reviewed up to "GRAPH THEORY". Only minor remarks. I will review section about graph theory later.

iset.mm

avekens

Graph Theory reviewed, still only minor remarks about wording

It's fantastic to see how graph theory becomes intuitonized. Hopefully, the definition of graphs either as ordered pairs or as extensible structures was the most difficult part, and the rest can be done more easily.

This is the syntax and df-edgf . Copied without change from set.mm.

Stated as in set.mm. The proof is the set.mm proof with small changes to use strnfvnd

This is the syntaxes , df-vtx , and df-iedg . Copied without change from set.mm.

This is vtxval from set.mm with a set existence condition added. The proof is taken from a portion of the set.mm proof with changes for set existence.

This is iedgval from set.mm with a set existence condition added. The proof is taken from a portion of the set.mm proof, modified for differences in set existence.

Stated as in set.mm. The proof is based on the set.mm proof but needs to be significantly longer for differences in set existence theorems.

Stated as in set.mm. The proof is the set.mm proof with a very small change for set existence.

Stated as in set.mm. The proof is the set.mm proof with a small change for differences in set existence.

Although this is similar to various existing theorems, we don't seem to have quite this form until now.

Stated as in set.mm. The proof is based on the iset.mm proof of en1 .

This is hashdmpropge2 from set.mm with a change to how we specify that a set has at least two elements. The proof is the set.mm proof with some adjustments to use rex2dom in place of hashge2el2difr .

This is structvtxvallem from set.mm but changes the way we say that a set has at least two elements. The proof is the set.mm proof with a number of small changes.

This is like 2strstrg in iset.mm but adapted to current conventions around extensible structure indexes. It is the same as 2strstr in set.mm but with set existence conditions added. The proof is slightly modified from the 2strstrg proof. Mark 2strstrg as discouraged because it hardcodes the index one.

Stated as in set.mm. The proof is the set.mm proof with some adjustments (including some set existence ones which make the proof longer).

Stated as in set.mm. The proof is the set.mm proof with small changes in various places.

This is structgrssvtxlem from set.mm with changes to how we specify that a set has at least two elements. The proof is the set.mm proof with several small changes.

Stated as in set.mm. The proof is the set.mm proof with small changes.

Stated as in set.mm. The proof is the set.mm proof with several small changes.

This is struct2grstr from set.mm with set existence conditions added. The proof is the set.mm proof with small changes.

Stated as in set.mm. The proof is the set.mm proof with small changes.

Stated as in set.mm. The proof is the set.mm proof with one small change.

This is grstructd from set.mm with a change to how we specify that a set has at least two elements. The proof is the set.mm proof with small changes.

This is grstructeld from set.mm with changes to how we specify that a set has at least two elements. The proof is the set.mm proof with small changes.

Update text for basprssdmsets

Add ax-coll to the $j usage. Remove ax-pow from the comment because it is used via breng and brdom2g , respectively.

Change "unordered pair" to "proper unordered pair" (meaning the two elements of the pair are unequal). Suggested by avekens .

Change "pair" to "unordered pair". As suggested by avekens .

Per "iset.mm versus set.mm names" at https://us.metamath.org/ileuni/conventions.html , the name structvtxvallem isn't available. So struct2slots2dom perhaps is a less awkward name.

Seems like the obvious name by analogy to struct2slots2dom .

(this is just to undo some odd ordering which happened during rebasing - the desired order is the order in set.mm) also, update mmil.html entries for structvtxvallem and structgrssvtxlem

jkingdon · 2025-12-24T02:57:08Z

It's fantastic to see how graph theory becomes intuitonized. Hopefully, the definition of graphs either as ordered pairs or as extensible structures was the most difficult part, and the rest can be done more easily.

I've only gotten slightly further than what is in this pull request, so I'm not too sure.

Do we assume that graphs are finite throughout? Sets not known to be finite are one place where excluded middle can potentially creep in but to be honest I have been taking things one step at a time rather than studying the set.mm treatment enough to see what happens later on.

avekens · 2025-12-24T05:57:25Z

iset.mm

+    $d f A $.  $d f B $.  $d f F $.
+    $( The domain and range of a one-to-one, onto set function are
+       equinumerous.  This variation of ~ f1oeng does not require the Axiom of
+       Replacement nor the Axiom of Union.  (Contributed by BTernaryTau,


Maybe we should use "Axiom of Collection" here, because in iset.mm, we do not have the Axiom of Replacement (it is a theorem proven by ax-coll, see ~repizf)

avekens · 2025-12-24T06:09:18Z

Do we assume that graphs are finite throughout? Sets not known to be finite are one place where excluded middle can potentially creep in but to be honest I have been taking things one step at a time rather than studying the set.mm treatment enough to see what happens later on.

No, in general, graphs can be infinite. There is a special definition for finite graphs (~df-fusgr), but only for undirected simple graphs. So let's wait until we get problems with potentially infinite graphs...