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 ) )