This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem usgrexmpl2vtx

Description: The vertices 0 , 1 , 2 , 3 , 4 , 5 of the graph G = <. V , E >. . (Contributed by AV, 3-Aug-2025)

Ref Expression
Hypotheses usgrexmpl2.v ⊢ V = 0 … 5
usgrexmpl2.e ⊢ E = ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
usgrexmpl2.g ⊢ G = V E
Assertion usgrexmpl2vtx ⊢ Vtx ⁡ G = 0 1 2 ∪ 3 4 5

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ V = 0 … 5
2 usgrexmpl2.e ⊢ E = ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩
3 usgrexmpl2.g ⊢ G = V E
4 3 fveq2i ⊢ Vtx ⁡ G = Vtx ⁡ V E
5 1 ovexi ⊢ V ∈ V
6 s7cli ⊢ ⟨“ 0 1 1 2 2 3 3 4 4 5 0 3 0 5 ”⟩ ∈ Word V
7 2 6 eqeltri ⊢ E ∈ Word V
8 opvtxfv ⊢ V ∈ V ∧ E ∈ Word V → Vtx ⁡ V E = V
9 5 7 8 mp2an ⊢ Vtx ⁡ V E = V
10 4 9 eqtri ⊢ Vtx ⁡ G = V
11 fz0to5un2tp ⊢ 0 … 5 = 0 1 2 ∪ 3 4 5
12 10 1 11 3eqtri ⊢ Vtx ⁡ G = 0 1 2 ∪ 3 4 5