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\in \mathrm{V}$$
	snstrvtxval.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\right\}$$
Assertion	snstrvtxval	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \mathrm{Vtx}\left(G\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		snstrvtxval.v	$$⊢V\in \mathrm{V}$$
2		snstrvtxval.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\right\}$$
3		necom	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\leftrightarrow {\mathrm{Base}}_{\mathrm{ndx}}\ne V$$
4		fvex	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
5	4 1 2	funsndifnop	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne V\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
6	3 5	sylbi	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
7	6	iffalsed	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\to if\left(G\in \left(\mathrm{V}\times \mathrm{V}\right),1^{st}\left(G\right),{\mathrm{Base}}_G\right)={\mathrm{Base}}_G$$
8		vtxval	$$⊢\mathrm{Vtx}\left(G\right)=if\left(G\in \left(\mathrm{V}\times \mathrm{V}\right),1^{st}\left(G\right),{\mathrm{Base}}_G\right)$$
9	8	a1i	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \mathrm{Vtx}\left(G\right)=if\left(G\in \left(\mathrm{V}\times \mathrm{V}\right),1^{st}\left(G\right),{\mathrm{Base}}_G\right)$$
10	2	1strbas	$$⊢V\in \mathrm{V}\to V={\mathrm{Base}}_G$$
11	1 10	mp1i	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\to V={\mathrm{Base}}_G$$
12	7 9 11	3eqtr4d	$$⊢V\ne {\mathrm{Base}}_{\mathrm{ndx}}\to \mathrm{Vtx}\left(G\right)=V$$