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
	snstrvtxval.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ }
Assertion	snstrvtxval	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( Vtx ‘ 𝐺 ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		snstrvtxval.v	⊢ 𝑉 ∈ V
2		snstrvtxval.g	⊢ 𝐺 = { ⟨ ( Base ‘ ndx ) , 𝑉 ⟩ }
3		necom	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) ↔ ( Base ‘ ndx ) ≠ 𝑉 )
4		fvex	⊢ ( Base ‘ ndx ) ∈ V
5	4 1 2	funsndifnop	⊢ ( ( Base ‘ ndx ) ≠ 𝑉 → ¬ 𝐺 ∈ ( V × V ) )
6	3 5	sylbi	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ¬ 𝐺 ∈ ( V × V ) )
7	6	iffalsed	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → if ( 𝐺 ∈ ( V × V ) , ( 1st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐺 ) )
8		vtxval	⊢ ( Vtx ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 1st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) )
9	8	a1i	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( Vtx ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 1st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) ) )
10	2	1strbas	⊢ ( 𝑉 ∈ V → 𝑉 = ( Base ‘ 𝐺 ) )
11	1 10	mp1i	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → 𝑉 = ( Base ‘ 𝐺 ) )
12	7 9 11	3eqtr4d	⊢ ( 𝑉 ≠ ( Base ‘ ndx ) → ( Vtx ‘ 𝐺 ) = 𝑉 )