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 ⊢ 𝑉 = ( 0 ... 5 )
usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
usgrexmpl2.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion usgrexmpl2vtx ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )

Proof

Step Hyp Ref Expression
1 usgrexmpl2.v ⊢ 𝑉 = ( 0 ... 5 )
2 usgrexmpl2.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩
3 usgrexmpl2.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 3 fveq2i ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ )
5 1 ovexi ⊢ 𝑉 ∈ V
6 s7cli ⊢ ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 3 } { 3 , 4 } { 4 , 5 } { 0 , 3 } { 0 , 5 } ”⟩ ∈ Word V
7 2 6 eqeltri ⊢ 𝐸 ∈ Word V
8 opvtxfv ⊢ ( ( 𝑉 ∈ V ∧ 𝐸 ∈ Word V ) → ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉 )
9 5 7 8 mp2an ⊢ ( Vtx ‘ ⟨ 𝑉 , 𝐸 ⟩ ) = 𝑉
10 4 9 eqtri ⊢ ( Vtx ‘ 𝐺 ) = 𝑉
11 fz0to5un2tp ⊢ ( 0 ... 5 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )
12 10 1 11 3eqtri ⊢ ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 , 5 } )