Metamath Proof Explorer


Theorem konigsberglem1

Description: Lemma 1 for konigsberg : Vertex 0 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 konigsberglem1 ( ( VtxDeg ‘ 𝐺 ) ‘ 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 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 0elfz ( 3 ∈ ℕ0 → 0 ∈ ( 0 ... 3 ) )
11 9 10 ax-mp 0 ∈ ( 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 ( ( 0 ∈ ( 0 ... 3 ) ∧ ∅ = ∅ ) → ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ∅ ⟩ ) ‘ 0 ) = 0 )
79 11 77 78 mp2an ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ∅ ⟩ ) ‘ 0 ) = 0
80 1nn0 1 ∈ ℕ0
81 1le3 1 ≤ 3
82 elfz2nn0 ( 1 ∈ ( 0 ... 3 ) ↔ ( 1 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 1 ≤ 3 ) )
83 80 9 81 82 mpbir3an 1 ∈ ( 0 ... 3 )
84 ax-1ne0 1 ≠ 0
85 s0s1 ⟨“ { 0 , 1 } ”⟩ = ( ∅ ++ ⟨“ { 0 , 1 } ”⟩ )
86 65 85 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } ”⟩ ⟩ ) = ( ∅ ++ ⟨“ { 0 , 1 } ”⟩ )
87 73 11 75 76 79 63 83 84 86 vdegp1bi ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } ”⟩ ⟩ ) ‘ 0 ) = ( 0 + 1 )
88 0p1e1 ( 0 + 1 ) = 1
89 87 88 eqtri ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } ”⟩ ⟩ ) ‘ 0 ) = 1
90 2nn0 2 ∈ ℕ0
91 2re 2 ∈ ℝ
92 3re 3 ∈ ℝ
93 2lt3 2 < 3
94 91 92 93 ltleii 2 ≤ 3
95 elfz2nn0 ( 2 ∈ ( 0 ... 3 ) ↔ ( 2 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 2 ≤ 3 ) )
96 90 9 94 95 mpbir3an 2 ∈ ( 0 ... 3 )
97 2ne0 2 ≠ 0
98 df-s2 ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ = ( ⟨“ { 0 , 1 } ”⟩ ++ ⟨“ { 0 , 2 } ”⟩ )
99 55 98 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ⟩ ) = ( ⟨“ { 0 , 1 } ”⟩ ++ ⟨“ { 0 , 2 } ”⟩ )
100 64 11 66 70 89 53 96 97 99 vdegp1bi ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ⟩ ) ‘ 0 ) = ( 1 + 1 )
101 1p1e2 ( 1 + 1 ) = 2
102 100 101 eqtri ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ⟩ ) ‘ 0 ) = 2
103 nn0fz0 ( 3 ∈ ℕ0 ↔ 3 ∈ ( 0 ... 3 ) )
104 9 103 mpbi 3 ∈ ( 0 ... 3 )
105 3ne0 3 ≠ 0
106 df-s3 ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ = ( ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ++ ⟨“ { 0 , 3 } ”⟩ )
107 45 106 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ⟩ ) = ( ⟨“ { 0 , 1 } { 0 , 2 } ”⟩ ++ ⟨“ { 0 , 3 } ”⟩ )
108 54 11 56 60 102 43 104 105 107 vdegp1bi ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ⟩ ) ‘ 0 ) = ( 2 + 1 )
109 2p1e3 ( 2 + 1 ) = 3
110 108 109 eqtri ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ⟩ ) ‘ 0 ) = 3
111 df-s4 ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ++ ⟨“ { 1 , 2 } ”⟩ )
112 35 111 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ⟩ ) = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } ”⟩ ++ ⟨“ { 1 , 2 } ”⟩ )
113 44 11 46 50 110 33 83 84 96 97 112 vdegp1ai ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ⟩ ) ‘ 0 ) = 3
114 df-s5 ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ++ ⟨“ { 1 , 2 } ”⟩ )
115 25 114 eqtri ( iEdg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ⟩ ) = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } ”⟩ ++ ⟨“ { 1 , 2 } ”⟩ )
116 34 11 36 40 113 23 83 84 96 97 115 vdegp1ai ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } ”⟩ ⟩ ) ‘ 0 ) = 3
117 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 } ”⟩ )
118 12 117 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 } ”⟩ )
119 24 11 26 30 116 7 96 97 104 105 118 vdegp1ai ( ( VtxDeg ‘ ⟨ ( 0 ... 3 ) , ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ⟩ ) ‘ 0 ) = 3
120 1 2 3 konigsbergvtx ( Vtx ‘ 𝐺 ) = ( 0 ... 3 )
121 1 2 3 konigsbergiedg ( iEdg ‘ 𝐺 ) = ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ”⟩
122 121 15 eqtri ( iEdg ‘ 𝐺 ) = ( ⟨“ { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } ”⟩ ++ ⟨“ { 2 , 3 } ”⟩ )
123 8 11 13 20 119 120 96 97 104 105 122 vdegp1ai ( ( VtxDeg ‘ 𝐺 ) ‘ 0 ) = 3