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

Metamath Proof Explorer

Theorem usgrexmplvtx

Description: The vertices 0 , 1 , 2 , 3 , 4 of the graph G = <. V , E >. . (Contributed by AV, 12-Jan-2020) (Revised by AV, 21-Oct-2020)

Ref Expression
Hypotheses usgrexmpl.v ⊢ 𝑉 = ( 0 ... 4 )
usgrexmpl.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
usgrexmpl.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
Assertion usgrexmplvtx ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )

Proof

Step Hyp Ref Expression
1 usgrexmpl.v ⊢ 𝑉 = ( 0 ... 4 )
2 usgrexmpl.e ⊢ 𝐸 = ⟨“ { 0 , 1 } { 1 , 2 } { 2 , 0 } { 0 , 3 } ”⟩
3 usgrexmpl.g ⊢ 𝐺 = ⟨ 𝑉 , 𝐸 ⟩
4 1 2 3 usgrexmpllem ⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 )
5 id ⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( Vtx ‘ 𝐺 ) = 𝑉 )
6 fz0to4untppr ⊢ ( 0 ... 4 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )
7 1 6 eqtri ⊢ 𝑉 = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )
8 5 7 eqtrdi ⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } ) )
9 8 adantr ⊢ ( ( ( Vtx ‘ 𝐺 ) = 𝑉 ∧ ( iEdg ‘ 𝐺 ) = 𝐸 ) → ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } ) )
10 4 9 ax-mp ⊢ ( Vtx ‘ 𝐺 ) = ( { 0 , 1 , 2 } ∪ { 3 , 4 } )