vtxval

Description: The set of vertices of a graph. (Contributed by AV, 9-Jan-2020) (Revised by AV, 21-Sep-2020)

		Ref	Expression
	Assertion	vtxval	⊢ ( Vtx ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 1^st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) )

Step	Hyp	Ref	Expression
1		eleq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 ∈ ( V × V ) ↔ 𝐺 ∈ ( V × V ) ) )
2		fveq2	⊢ ( 𝑔 = 𝐺 → ( 1^st ‘ 𝑔 ) = ( 1^st ‘ 𝐺 ) )
3		fveq2	⊢ ( 𝑔 = 𝐺 → ( Base ‘ 𝑔 ) = ( Base ‘ 𝐺 ) )
4	1 2 3	ifbieq12d	⊢ ( 𝑔 = 𝐺 → if ( 𝑔 ∈ ( V × V ) , ( 1^st ‘ 𝑔 ) , ( Base ‘ 𝑔 ) ) = if ( 𝐺 ∈ ( V × V ) , ( 1^st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) ) )
5		df-vtx	⊢ Vtx = ( 𝑔 ∈ V ↦ if ( 𝑔 ∈ ( V × V ) , ( 1^st ‘ 𝑔 ) , ( Base ‘ 𝑔 ) ) )
6		fvex	⊢ ( 1^st ‘ 𝐺 ) ∈ V
7		fvex	⊢ ( Base ‘ 𝐺 ) ∈ V
8	6 7	ifex	⊢ if ( 𝐺 ∈ ( V × V ) , ( 1^st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) ) ∈ V
9	4 5 8	fvmpt	⊢ ( 𝐺 ∈ V → ( Vtx ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 1^st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) ) )
10		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( Base ‘ 𝐺 ) = ∅ )
11		prcnel	⊢ ( ¬ 𝐺 ∈ V → ¬ 𝐺 ∈ ( V × V ) )
12	11	iffalsed	⊢ ( ¬ 𝐺 ∈ V → if ( 𝐺 ∈ ( V × V ) , ( 1^st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) ) = ( Base ‘ 𝐺 ) )
13		fvprc	⊢ ( ¬ 𝐺 ∈ V → ( Vtx ‘ 𝐺 ) = ∅ )
14	10 12 13	3eqtr4rd	⊢ ( ¬ 𝐺 ∈ V → ( Vtx ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 1^st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) ) )
15	9 14	pm2.61i	⊢ ( Vtx ‘ 𝐺 ) = if ( 𝐺 ∈ ( V × V ) , ( 1^st ‘ 𝐺 ) , ( Base ‘ 𝐺 ) )

Metamath Proof Explorer