Metamath Proof Explorer


Theorem konigsbergvtx

Description: The set of vertices of the Königsberg graph G . (Contributed by AV, 28-Feb-2021)

Ref Expression
Hypotheses konigsberg.v 𝑉 = ( 0 ... 3 )
konigsberg.e 𝐸 = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
konigsberg.g 𝐺 = ⟨ 𝑉 , 𝐸
Assertion konigsbergvtx ( Vtx ‘ 𝐺 ) = ( 0 ... 3 )

Proof

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