Metamath Proof Explorer

Theorem konigsberglem2

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