Theorem funvtxval0

Description: The set of vertices of an extensible structure with a base set and (at least) another slot. (Contributed by AV, 22-Sep-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)

	Ref	Expression
Hypothesis	funvtxval0.s	|- S e. _V
Assertion	funvtxval0	|- ( ( Fun ( G \ { (/) } ) /\ S =/= ( Base ` ndx ) /\ { ( Base ` ndx ) , S } C_ dom G ) -> ( Vtx ` G ) = ( Base ` G ) )

Proof

Step	Hyp	Ref	Expression
1		funvtxval0.s	|- S e. _V
2		necom	|- ( S =/= ( Base ` ndx ) <-> ( Base ` ndx ) =/= S )
3		fvex	|- ( Base ` ndx ) e. _V
4	3 1	funvtxdm2val	|- ( ( Fun ( G \ { (/) } ) /\ ( Base ` ndx ) =/= S /\ { ( Base ` ndx ) , S } C_ dom G ) -> ( Vtx ` G ) = ( Base ` G ) )
5	2 4	syl3an2b	|- ( ( Fun ( G \ { (/) } ) /\ S =/= ( Base ` ndx ) /\ { ( Base ` ndx ) , S } C_ dom G ) -> ( Vtx ` G ) = ( Base ` G ) )