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 } )