Metamath Proof Explorer

Theorem 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 ⁡ G = if G ∈ V × V 1 st ⁡ G Base G

Proof

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