This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem setsvtx

Description: The vertices of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 18-Jan-2020) (Revised by AV, 16-Nov-2021)

Ref Expression
Hypotheses setsvtx.i 
|- I = ( .ef ` ndx )
setsvtx.s 
|- ( ph -> G Struct X )
setsvtx.b 
|- ( ph -> ( Base ` ndx ) e. dom G )
setsvtx.e 
|- ( ph -> E e. W )
Assertion setsvtx 
|- ( ph -> ( Vtx ` ( G sSet <. I , E >. ) ) = ( Base ` G ) )

Proof

Step Hyp Ref Expression
1 setsvtx.i 
 |-  I = ( .ef ` ndx )
2 setsvtx.s 
 |-  ( ph -> G Struct X )
3 setsvtx.b 
 |-  ( ph -> ( Base ` ndx ) e. dom G )
4 setsvtx.e 
 |-  ( ph -> E e. W )
5 1 fvexi 
 |-  I e. _V
6 5 a1i 
 |-  ( ph -> I e. _V )
7 2 6 4 setsn0fun 
 |-  ( ph -> Fun ( ( G sSet <. I , E >. ) \ { (/) } ) )
8 1 eqcomi 
 |-  ( .ef ` ndx ) = I
9 8 preq2i 
 |-  { ( Base ` ndx ) , ( .ef ` ndx ) } = { ( Base ` ndx ) , I }
10 2 6 4 3 basprssdmsets 
 |-  ( ph -> { ( Base ` ndx ) , I } C_ dom ( G sSet <. I , E >. ) )
11 9 10 eqsstrid 
 |-  ( ph -> { ( Base ` ndx ) , ( .ef ` ndx ) } C_ dom ( G sSet <. I , E >. ) )
12 funvtxval 
 |-  ( ( Fun ( ( G sSet <. I , E >. ) \ { (/) } ) /\ { ( Base ` ndx ) , ( .ef ` ndx ) } C_ dom ( G sSet <. I , E >. ) ) -> ( Vtx ` ( G sSet <. I , E >. ) ) = ( Base ` ( G sSet <. I , E >. ) ) )
13 7 11 12 syl2anc 
 |-  ( ph -> ( Vtx ` ( G sSet <. I , E >. ) ) = ( Base ` ( G sSet <. I , E >. ) ) )
14 baseid 
 |-  Base = Slot ( Base ` ndx )
15 basendxnedgfndx 
 |-  ( Base ` ndx ) =/= ( .ef ` ndx )
16 15 1 neeqtrri 
 |-  ( Base ` ndx ) =/= I
17 14 16 setsnid 
 |-  ( Base ` G ) = ( Base ` ( G sSet <. I , E >. ) )
18 13 17 eqtr4di 
 |-  ( ph -> ( Vtx ` ( G sSet <. I , E >. ) ) = ( Base ` G ) )