Theorem snstrvtxval

Description: The set of vertices of a graph without edges represented as an extensible structure with vertices as base set and no indexed edges. See vtxvalsnop for the (degenerate) case where V = ( Basendx ) . (Contributed by AV, 23-Sep-2020)

	Ref	Expression
Hypotheses	snstrvtxval.v	|- V e. _V
	snstrvtxval.g	|- G = { <. ( Base ` ndx ) , V >. }
Assertion	snstrvtxval	|- ( V =/= ( Base ` ndx ) -> ( Vtx ` G ) = V )

Proof

Step	Hyp	Ref	Expression
1		snstrvtxval.v	|- V e. _V
2		snstrvtxval.g	|- G = { <. ( Base ` ndx ) , V >. }
3		necom	|- ( V =/= ( Base ` ndx ) <-> ( Base ` ndx ) =/= V )
4		fvex	|- ( Base ` ndx ) e. _V
5	4 1 2	funsndifnop	|- ( ( Base ` ndx ) =/= V -> -. G e. ( _V X. _V ) )
6	3 5	sylbi	|- ( V =/= ( Base ` ndx ) -> -. G e. ( _V X. _V ) )
7	6	iffalsed	|- ( V =/= ( Base ` ndx ) -> if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) = ( Base ` G ) )
8		vtxval	|- ( Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) )
9	8	a1i	|- ( V =/= ( Base ` ndx ) -> ( Vtx ` G ) = if ( G e. ( _V X. _V ) , ( 1st ` G ) , ( Base ` G ) ) )
10	2	1strbas	|- ( V e. _V -> V = ( Base ` G ) )
11	1 10	mp1i	|- ( V =/= ( Base ` ndx ) -> V = ( Base ` G ) )
12	7 9 11	3eqtr4d	|- ( V =/= ( Base ` ndx ) -> ( Vtx ` G ) = V )