Metamath Proof Explorer


Theorem konigsbergiedg

Description: The indexed edges 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 konigsbergiedg ( iEdg β€˜ 𝐺 ) = βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 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 ⊒ ( iEdg β€˜ 𝐺 ) = ( iEdg β€˜ ⟨ ( 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 opiedgfv ⊒ ( ( ( 0 ... 3 ) ∈ V ∧ βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ© ∈ Word V ) β†’ ( iEdg β€˜ ⟨ ( 0 ... 3 ) , βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ© ⟩ ) = βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ© )
10 7 8 9 mp2an ⊒ ( iEdg β€˜ ⟨ ( 0 ... 3 ) , βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ© ⟩ ) = βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ©
11 6 10 eqtri ⊒ ( iEdg β€˜ 𝐺 ) = βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ©