add vertex/edge access theorems to iset.mm #5139
Open
+1,108
−5
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 .
Stated as in set.mm. The proof is the set.mm proof with some small changes for differences in set existence theorems.
This is edgfiedgval from set.mm with a change to how we say a set has at least two elements. The proof is the set.mm proof with small changes.
This is funvtxval and funiedgval from set.mm with set existence conditions added. The proofs are the set.mm proofs with small changes.
This is implied by a comment, so say it explicitly.
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
avekens
reviewed
Dec 23, 2025
| ( 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'; $) |
Contributor
There was a problem hiding this comment.
'ax-rep' and 'ax-pow' shold be added (as mentioned in the comment).
Contributor
Author
There was a problem hiding this 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.
avekens
reviewed
Dec 23, 2025
| en2prd.4 $e |- ( ph -> D e. Y ) $. | ||
| en2prd.5 $e |- ( ph -> A =/= B ) $. | ||
| en2prd.6 $e |- ( ph -> C =/= D ) $. | ||
| $( Two unordered pairs are equinumerous. (Contributed by BTernaryTau, |
Contributor
There was a problem hiding this comment.
"Two proper unordered pairs ..."
avekens
reviewed
Dec 23, 2025
|
|
||
| ${ | ||
| $d A f x y $. | ||
| $( A set equinumerous to ordinal 2 is a pair. (Contributed by Mario |
Contributor
There was a problem hiding this comment.
"... is an unordered pair."
avekens
reviewed
Dec 23, 2025
Contributor
avekens
left a comment
avekens
left a comment
There was a problem hiding this comment.
Reviewed up to "GRAPH THEORY". Only minor remarks. I will review section about graph theory later.
avekens
reviewed
Dec 23, 2025
| structvtxvallem.g $e |- G = { <. ( Base ` ndx ) , V >. , <. S , E >. } $. | ||
| $( Lemma for ~ structvtxval and ~ structiedg0val . (Contributed by AV, | ||
| 23-Sep-2020.) (Revised by AV, 12-Nov-2021.) $) | ||
| structvtxvallem2dom $p |- ( ( V e. X /\ E e. Y ) -> 2o ~<_ dom G ) $= |
Contributor
There was a problem hiding this comment.
I think this should still be called "structvtxvallem", because it is still a lemma for ~ structvtxval and ~ structiedg0val only.
Contributor
There was a problem hiding this comment.
Alternatively, this lemma could become a stand alone theorem, maybe called ~struct2slots2dom
avekens
reviewed
Dec 23, 2025
| <. ( .ef ` ndx ) , E >. } C_ G ) $. | ||
| $( Lemma for ~ structgrssvtx and ~ structgrssiedg . (Contributed by AV, | ||
| 14-Oct-2020.) (Proof shortened by AV, 12-Nov-2021.) $) | ||
| structgrssvtxlem2dom $p |- ( ph -> 2o ~<_ dom G ) $= |
Contributor
There was a problem hiding this comment.
See comment for ~structvtxvallem2dom.
avekens
reviewed
Dec 23, 2025
Contributor
There was a problem hiding this comment.
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.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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
2strstrto 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 ~<_ Ais 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) whereas2 <_ ( # ` A )is not (at least with current theorems,#works on finite sets or on infinite sets, but not on arbitrary sets).