Metamath Proof Explorer

Theorem konigsbergiedgw

Description: The indexed edges of the KΓΆnigsberg graph G is a word over the pairs of vertices. (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 konigsbergiedgw 𝐸 ∈ Word { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 }

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 3nn0 ⊒ 3 ∈ β„•0
5 0elfz ⊒ ( 3 ∈ β„•0 β†’ 0 ∈ ( 0 ... 3 ) )
6 4 5 ax-mp ⊒ 0 ∈ ( 0 ... 3 )
7 1nn0 ⊒ 1 ∈ β„•0
8 1le3 ⊒ 1 ≀ 3
9 elfz2nn0 ⊒ ( 1 ∈ ( 0 ... 3 ) ↔ ( 1 ∈ β„•0 ∧ 3 ∈ β„•0 ∧ 1 ≀ 3 ) )
10 7 4 8 9 mpbir3an ⊒ 1 ∈ ( 0 ... 3 )
11 0ne1 ⊒ 0 β‰  1
12 6 10 11 umgrbi ⊒ { 0 , 1 } ∈ { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 }
13 12 a1i ⊒ ( ⊀ β†’ { 0 , 1 } ∈ { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 } )
14 2nn0 ⊒ 2 ∈ β„•0
15 2re ⊒ 2 ∈ ℝ
16 3re ⊒ 3 ∈ ℝ
17 2lt3 ⊒ 2 < 3
18 15 16 17 ltleii ⊒ 2 ≀ 3
19 elfz2nn0 ⊒ ( 2 ∈ ( 0 ... 3 ) ↔ ( 2 ∈ β„•0 ∧ 3 ∈ β„•0 ∧ 2 ≀ 3 ) )
20 14 4 18 19 mpbir3an ⊒ 2 ∈ ( 0 ... 3 )
21 0ne2 ⊒ 0 β‰  2
22 6 20 21 umgrbi ⊒ { 0 , 2 } ∈ { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 }
23 22 a1i ⊒ ( ⊀ β†’ { 0 , 2 } ∈ { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 } )
24 nn0fz0 ⊒ ( 3 ∈ β„•0 ↔ 3 ∈ ( 0 ... 3 ) )
25 4 24 mpbi ⊒ 3 ∈ ( 0 ... 3 )
26 3ne0 ⊒ 3 β‰  0
27 26 necomi ⊒ 0 β‰  3
28 6 25 27 umgrbi ⊒ { 0 , 3 } ∈ { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 }
29 28 a1i ⊒ ( ⊀ β†’ { 0 , 3 } ∈ { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 } )
30 1ne2 ⊒ 1 β‰  2
31 10 20 30 umgrbi ⊒ { 1 , 2 } ∈ { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 }
32 31 a1i ⊒ ( ⊀ β†’ { 1 , 2 } ∈ { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 } )
33 15 17 ltneii ⊒ 2 β‰  3
34 20 25 33 umgrbi ⊒ { 2 , 3 } ∈ { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 }
35 34 a1i ⊒ ( ⊀ β†’ { 2 , 3 } ∈ { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 } )
36 13 23 29 32 32 35 35 s7cld ⊒ ( ⊀ β†’ βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ© ∈ Word { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 } )
37 36 mptru ⊒ βŸ¨β€œ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } β€βŸ© ∈ Word { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 }
38 1 pweqi ⊒ 𝒫 𝑉 = 𝒫 ( 0 ... 3 )
39 38 rabeqi ⊒ { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 } = { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 }
40 39 wrdeqi ⊒ Word { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 } = Word { π‘₯ ∈ 𝒫 ( 0 ... 3 ) ∣ ( β™― β€˜ π‘₯ ) = 2 }
41 37 2 40 3eltr4i ⊒ 𝐸 ∈ Word { π‘₯ ∈ 𝒫 𝑉 ∣ ( β™― β€˜ π‘₯ ) = 2 }