Metamath Proof Explorer


Theorem konigsberglem3

Description: Lemma 3 for konigsberg : Vertex 3 has degree three. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Revised by AV, 4-Mar-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 konigsberglem3 ( ( VtxDeg ‘ 𝐺 ) ‘ 3 ) = 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 ovex ( 0 ... 3 ) ∈ V
5 s6cli ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ∈ Word V
6 5 elexi ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ∈ V
7 4 6 opvtxfvi ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ⟩ ) = ( 0 ... 3 )
8 7 eqcomi ( 0 ... 3 ) = ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ⟩ )
9 3nn0 3 ∈ ℕ0
10 nn0fz0 ( 3 ∈ ℕ0 ↔ 3 ∈ ( 0 ... 3 ) )
11 9 10 mpbi 3 ∈ ( 0 ... 3 )
12 4 6 opiedgfvi ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ⟩ ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩
13 12 eqcomi ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ = ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ⟩ )
14 s1cli ⟨“ { 2 , 3 } ”⟩ ∈ Word V
15 df-s7 ⟨“ { 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 } ”⟩ )
16 eqid ( 0 ... 3 ) = ( 0 ... 3 )
17 eqid ⟨“ { 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 } ”⟩
18 eqid ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ⟩ = ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ⟩
19 16 17 18 konigsbergssiedgw ( ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ∈ Word V ∧ ⟨“ { 2 , 3 } ”⟩ ∈ Word V ∧ ⟨“ { 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 } ”⟩ ) ) → ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
20 5 14 15 19 mp3an ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
21 s5cli ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ∈ Word V
22 21 elexi ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ∈ V
23 4 22 opvtxfvi ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ⟩ ) = ( 0 ... 3 )
24 23 eqcomi ( 0 ... 3 ) = ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ⟩ )
25 4 22 opiedgfvi ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ⟩ ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩
26 25 eqcomi ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ = ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ⟩ )
27 s2cli ⟨“ { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V
28 s5s2 ⟨“ { 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 } ”⟩ )
29 16 17 18 konigsbergssiedgw ( ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ∈ Word V ∧ ⟨“ { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V ∧ ⟨“ { 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 } ”⟩ ) ) → ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
30 21 27 28 29 mp3an ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
31 s4cli ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ∈ Word V
32 31 elexi ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ∈ V
33 4 32 opvtxfvi ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ⟩ ) = ( 0 ... 3 )
34 33 eqcomi ( 0 ... 3 ) = ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ⟩ )
35 4 32 opiedgfvi ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ⟩ ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩
36 35 eqcomi ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ = ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ⟩ )
37 s3cli ⟨“ { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V
38 s4s3 ⟨“ { 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 } ”⟩ )
39 16 17 18 konigsbergssiedgw ( ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ∈ Word V ∧ ⟨“ { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V ∧ ⟨“ { 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 } ”⟩ ) ) → ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
40 31 37 38 39 mp3an ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
41 s3cli ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ∈ Word V
42 41 elexi ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ∈ V
43 4 42 opvtxfvi ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ⟩ ) = ( 0 ... 3 )
44 43 eqcomi ( 0 ... 3 ) = ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ⟩ )
45 4 42 opiedgfvi ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ⟩ ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩
46 45 eqcomi ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ = ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ⟩ )
47 s4cli ⟨“ { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V
48 s3s4 ⟨“ { 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 } ”⟩ )
49 16 17 18 konigsbergssiedgw ( ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ∈ Word V ∧ ⟨“ { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V ∧ ⟨“ { 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 } ”⟩ ) ) → ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
50 41 47 48 49 mp3an ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
51 s2cli ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ∈ Word V
52 51 elexi ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ∈ V
53 4 52 opvtxfvi ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ⟩ ) = ( 0 ... 3 )
54 53 eqcomi ( 0 ... 3 ) = ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ⟩ )
55 4 52 opiedgfvi ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ⟩ ) = ⟨“ { 0 , 1 } { 0 , 2 } ”⟩
56 55 eqcomi ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ = ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ⟩ )
57 s5cli ⟨“ { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V
58 s2s5 ⟨“ { 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 } ”⟩ )
59 16 17 18 konigsbergssiedgw ( ( ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ∈ Word V ∧ ⟨“ { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V ∧ ⟨“ { 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 } ”⟩ ) ) → ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
60 51 57 58 59 mp3an ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
61 s1cli ⟨“ { 0 , 1 } ”⟩ ∈ Word V
62 61 elexi ⟨“ { 0 , 1 } ”⟩ ∈ V
63 4 62 opvtxfvi ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } ”⟩ ⟩ ) = ( 0 ... 3 )
64 63 eqcomi ( 0 ... 3 ) = ( Vtx ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } ”⟩ ⟩ )
65 4 62 opiedgfvi ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } ”⟩ ⟩ ) = ⟨“ { 0 , 1 } ”⟩
66 65 eqcomi ⟨“ { 0 , 1 } ”⟩ = ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } ”⟩ ⟩ )
67 s6cli ⟨“ { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V
68 s1s6 ⟨“ { 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 } ”⟩ )
69 16 17 18 konigsbergssiedgw ( ( ⟨“ { 0 , 1 } ”⟩ ∈ Word V ∧ ⟨“ { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩ ∈ Word V ∧ ⟨“ { 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 } ”⟩ ) ) → ⟨“ { 0 , 1 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
70 61 67 68 69 mp3an ⟨“ { 0 , 1 } ”⟩ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
71 0ex ∅ ∈ V
72 4 71 opvtxfvi ( Vtx ‘ ⟨ ( 0 ... 3 ) , ∅ ⟩ ) = ( 0 ... 3 )
73 72 eqcomi ( 0 ... 3 ) = ( Vtx ‘ ⟨ ( 0 ... 3 ) , ∅ ⟩ )
74 4 71 opiedgfvi ( iEdg ‘ ⟨ ( 0 ... 3 ) , ∅ ⟩ ) = ∅
75 74 eqcomi ∅ = ( iEdg ‘ ⟨ ( 0 ... 3 ) , ∅ ⟩ )
76 wrd0 ∅ ∈ Word { 𝑥 ∈ ( 𝒫 ( 0 ... 3 ) ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 }
77 eqid ∅ = ∅
78 73 75 vtxdg0e ( ( 3 ∈ ( 0 ... 3 ) ∧ ∅ = ∅ ) → ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ∅ ⟩ ) ‘ 3 ) = 0 )
79 11 77 78 mp2an ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ∅ ⟩ ) ‘ 3 ) = 0
80 0elfz ( 3 ∈ ℕ0 → 0 ∈ ( 0 ... 3 ) )
81 9 80 ax-mp 0 ∈ ( 0 ... 3 )
82 3ne0 3 ≠ 0
83 82 necomi 0 ≠ 3
84 1nn0 1 ∈ ℕ0
85 1le3 1 ≤ 3
86 elfz2nn0 ( 1 ∈ ( 0 ... 3 ) ↔ ( 1 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 1 ≤ 3 ) )
87 84 9 85 86 mpbir3an 1 ∈ ( 0 ... 3 )
88 1re 1 ∈ ℝ
89 1lt3 1 < 3
90 88 89 ltneii 1 ≠ 3
91 s0s1 ⟨“ { 0 , 1 } ”⟩ = ( ∅ ++ ⟨“ { 0 , 1 } ”⟩ )
92 65 91 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } ”⟩ ⟩ ) = ( ∅ ++ ⟨“ { 0 , 1 } ”⟩ )
93 73 11 75 76 79 63 81 83 87 90 92 vdegp1ai ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } ”⟩ ⟩ ) ‘ 3 ) = 0
94 2nn0 2 ∈ ℕ0
95 2re 2 ∈ ℝ
96 3re 3 ∈ ℝ
97 2lt3 2 < 3
98 95 96 97 ltleii 2 ≤ 3
99 elfz2nn0 ( 2 ∈ ( 0 ... 3 ) ↔ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 2 ≤ 3 ) )
100 94 9 98 99 mpbir3an 2 ∈ ( 0 ... 3 )
101 95 97 ltneii 2 ≠ 3
102 df-s2 ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ = ( ⟨“ { 0 , 1 } ”⟩ ++ ⟨“ { 0 , 2 } ”⟩ )
103 55 102 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ⟩ ) = ( ⟨“ { 0 , 1 } ”⟩ ++ ⟨“ { 0 , 2 } ”⟩ )
104 64 11 66 70 93 53 81 83 100 101 103 vdegp1ai ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ⟩ ) ‘ 3 ) = 0
105 df-s3 ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ = ( ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ++ ⟨“ { 0 , 3 } ”⟩ )
106 45 105 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ⟩ ) = ( ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ++ ⟨“ { 0 , 3 } ”⟩ )
107 54 11 56 60 104 43 81 83 106 vdegp1ci ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ⟩ ) ‘ 3 ) = ( 0 + 1 )
108 0p1e1 ( 0 + 1 ) = 1
109 107 108 eqtri ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ⟩ ) ‘ 3 ) = 1
110 df-s4 ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ++ ⟨“ { 1 , 2 } ”⟩ )
111 35 110 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ⟩ ) = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ++ ⟨“ { 1 , 2 } ”⟩ )
112 44 11 46 50 109 33 87 90 100 101 111 vdegp1ai ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ⟩ ) ‘ 3 ) = 1
113 df-s5 ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ++ ⟨“ { 1 , 2 } ”⟩ )
114 25 113 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ⟩ ) = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ++ ⟨“ { 1 , 2 } ”⟩ )
115 34 11 36 40 112 23 87 90 100 101 114 vdegp1ai ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ⟩ ) ‘ 3 ) = 1
116 df-s6 ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ++ ⟨“ { 2 , 3 } ”⟩ )
117 12 116 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ⟩ ) = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ++ ⟨“ { 2 , 3 } ”⟩ )
118 24 11 26 30 115 7 100 101 117 vdegp1ci ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ⟩ ) ‘ 3 ) = ( 1 + 1 )
119 1p1e2 ( 1 + 1 ) = 2
120 118 119 eqtri ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ⟩ ) ‘ 3 ) = 2
121 1 2 3 konigsbergvtx ( Vtx ‘ 𝐺 ) = ( 0 ... 3 )
122 1 2 3 konigsbergiedg ( iEdg ‘ 𝐺 ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
123 122 15 eqtri ( iEdg ‘ 𝐺 ) = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ++ ⟨“ { 2 , 3 } ”⟩ )
124 8 11 13 20 120 121 100 101 123 vdegp1ci ( ( VtxDeg ‘ 𝐺 ) ‘ 3 ) = ( 2 + 1 )
125 2p1e3 ( 2 + 1 ) = 3
126 124 125 eqtri ( ( VtxDeg ‘ 𝐺 ) ‘ 3 ) = 3