Step | Hyp | Ref
| Expression |
1 | | prhash2ex 13048 |
. . . . . 6
⊢
(#‘{0, 1}) = 2 |
2 | 1 | oveq1i 6559 |
. . . . 5
⊢
((#‘{0, 1}) + 1) = (2 + 1) |
3 | | prfi 8120 |
. . . . . 6
⊢ {0, 1}
∈ Fin |
4 | | 3ne0 10992 |
. . . . . . 7
⊢ 3 ≠
0 |
5 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
6 | | 1lt3 11073 |
. . . . . . . 8
⊢ 1 <
3 |
7 | 5, 6 | gtneii 10028 |
. . . . . . 7
⊢ 3 ≠
1 |
8 | 4, 7 | nelpri 4149 |
. . . . . 6
⊢ ¬ 3
∈ {0, 1} |
9 | | 3nn0 11187 |
. . . . . . 7
⊢ 3 ∈
ℕ0 |
10 | | hashunsng 13042 |
. . . . . . 7
⊢ (3 ∈
ℕ0 → (({0, 1} ∈ Fin ∧ ¬ 3 ∈ {0, 1})
→ (#‘({0, 1} ∪ {3})) = ((#‘{0, 1}) + 1))) |
11 | 9, 10 | ax-mp 5 |
. . . . . 6
⊢ (({0, 1}
∈ Fin ∧ ¬ 3 ∈ {0, 1}) → (#‘({0, 1} ∪ {3})) =
((#‘{0, 1}) + 1)) |
12 | 3, 8, 11 | mp2an 704 |
. . . . 5
⊢
(#‘({0, 1} ∪ {3})) = ((#‘{0, 1}) + 1) |
13 | | df-3 10957 |
. . . . 5
⊢ 3 = (2 +
1) |
14 | 2, 12, 13 | 3eqtr4i 2642 |
. . . 4
⊢
(#‘({0, 1} ∪ {3})) = 3 |
15 | | konigsberg.v |
. . . . . . . 8
⊢ 𝑉 = (0...3) |
16 | | fzfi 12633 |
. . . . . . . 8
⊢ (0...3)
∈ Fin |
17 | 15, 16 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑉 ∈ Fin |
18 | | ssrab2 3650 |
. . . . . . 7
⊢ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ⊆ 𝑉 |
19 | | ssfi 8065 |
. . . . . . 7
⊢ ((𝑉 ∈ Fin ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ⊆ 𝑉) → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ∈ Fin) |
20 | 17, 18, 19 | mp2an 704 |
. . . . . 6
⊢ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ∈ Fin |
21 | | nn0uz 11598 |
. . . . . . . . . . . 12
⊢
ℕ0 = (ℤ≥‘0) |
22 | 9, 21 | eleqtri 2686 |
. . . . . . . . . . 11
⊢ 3 ∈
(ℤ≥‘0) |
23 | | eluzfz1 12219 |
. . . . . . . . . . 11
⊢ (3 ∈
(ℤ≥‘0) → 0 ∈ (0...3)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . 10
⊢ 0 ∈
(0...3) |
25 | 24, 15 | eleqtrri 2687 |
. . . . . . . . 9
⊢ 0 ∈
𝑉 |
26 | | n2dvds3 14945 |
. . . . . . . . 9
⊢ ¬ 2
∥ 3 |
27 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 0 → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘0)) |
28 | 15 | ovexi 6578 |
. . . . . . . . . . . . . 14
⊢ 𝑉 ∈ V |
29 | | df-s6 13448 |
. . . . . . . . . . . . . . 15
⊢
〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}”〉 =
(〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}”〉 ++
〈“{2, 3}”〉) |
30 | | df-s5 13447 |
. . . . . . . . . . . . . . . 16
⊢
〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}”〉 =
(〈“{0, 1} {0, 2} {0, 3} {1, 2}”〉 ++ 〈“{1,
2}”〉) |
31 | | df-s4 13446 |
. . . . . . . . . . . . . . . . 17
⊢
〈“{0, 1} {0, 2} {0, 3} {1, 2}”〉 =
(〈“{0, 1} {0, 2} {0, 3}”〉 ++ 〈“{1,
2}”〉) |
32 | | df-s3 13445 |
. . . . . . . . . . . . . . . . . 18
⊢
〈“{0, 1} {0, 2} {0, 3}”〉 = (〈“{0, 1}
{0, 2}”〉 ++ 〈“{0, 3}”〉) |
33 | | df-s2 13444 |
. . . . . . . . . . . . . . . . . . 19
⊢
〈“{0, 1} {0, 2}”〉 = (〈“{0,
1}”〉 ++ 〈“{0, 2}”〉) |
34 | | 1le3 11121 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ≤
3 |
35 | | 1eluzge0 11608 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
(ℤ≥‘0) |
36 | | 3z 11287 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 3 ∈
ℤ |
37 | | elfz5 12205 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((1
∈ (ℤ≥‘0) ∧ 3 ∈ ℤ) → (1
∈ (0...3) ↔ 1 ≤ 3)) |
38 | 35, 36, 37 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (1 ∈
(0...3) ↔ 1 ≤ 3) |
39 | 34, 38 | mpbir 220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
(0...3) |
40 | 39, 15 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
𝑉 |
41 | 28, 25, 40 | umgrabi 26510 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ {0, 1} ∈ {𝑥
∈ (𝒫 𝑉 ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
42 | 41 | s1cld 13236 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⊤
→ 〈“{0, 1}”〉 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
43 | | 2re 10967 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
ℝ |
44 | | 3re 10971 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 3 ∈
ℝ |
45 | | 2lt3 11072 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 <
3 |
46 | 43, 44, 45 | ltleii 10039 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ≤
3 |
47 | | 2eluzge0 11609 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 2 ∈
(ℤ≥‘0) |
48 | | elfz5 12205 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((2
∈ (ℤ≥‘0) ∧ 3 ∈ ℤ) → (2
∈ (0...3) ↔ 2 ≤ 3)) |
49 | 47, 36, 48 | mp2an 704 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2 ∈
(0...3) ↔ 2 ≤ 3) |
50 | 46, 49 | mpbir 220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 2 ∈
(0...3) |
51 | 50, 15 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ∈
𝑉 |
52 | 28, 25, 51 | umgrabi 26510 |
. . . . . . . . . . . . . . . . . . 19
⊢ (⊤
→ {0, 2} ∈ {𝑥
∈ (𝒫 𝑉 ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
53 | 33, 42, 52 | cats1cld 13451 |
. . . . . . . . . . . . . . . . . 18
⊢ (⊤
→ 〈“{0, 1} {0, 2}”〉 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
54 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (3 ∈
(ℤ≥‘0) → 3 ∈ (0...3)) |
55 | 22, 54 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 3 ∈
(0...3) |
56 | 55, 15 | eleqtrri 2687 |
. . . . . . . . . . . . . . . . . . 19
⊢ 3 ∈
𝑉 |
57 | 28, 25, 56 | umgrabi 26510 |
. . . . . . . . . . . . . . . . . 18
⊢ (⊤
→ {0, 3} ∈ {𝑥
∈ (𝒫 𝑉 ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
58 | 32, 53, 57 | cats1cld 13451 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ 〈“{0, 1} {0, 2} {0, 3}”〉 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
59 | 28, 40, 51 | umgrabi 26510 |
. . . . . . . . . . . . . . . . 17
⊢ (⊤
→ {1, 2} ∈ {𝑥
∈ (𝒫 𝑉 ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
60 | 31, 58, 59 | cats1cld 13451 |
. . . . . . . . . . . . . . . 16
⊢ (⊤
→ 〈“{0, 1} {0, 2} {0, 3} {1, 2}”〉 ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
61 | 30, 60, 59 | cats1cld 13451 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2}”〉 ∈ Word
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
62 | 28, 51, 56 | umgrabi 26510 |
. . . . . . . . . . . . . . 15
⊢ (⊤
→ {2, 3} ∈ {𝑥
∈ (𝒫 𝑉 ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
63 | 29, 61, 62 | cats1cld 13451 |
. . . . . . . . . . . . . 14
⊢ (⊤
→ 〈“{0, 1} {0, 2} {0, 3} {1, 2} {1, 2} {2, 3}”〉
∈ Word {𝑥 ∈
(𝒫 𝑉 ∖
{∅}) ∣ (#‘𝑥) ≤ 2}) |
64 | | wrd0 13185 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ∅
∈ Word {𝑥 ∈
(𝒫 𝑉 ∖
{∅}) ∣ (#‘𝑥) ≤ 2} |
65 | 64 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (⊤
→ ∅ ∈ Word {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
66 | 28, 25 | vdeg0i 26509 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 VDeg ∅)‘0) =
0 |
67 | | 1e0p1 11428 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 = (0 +
1) |
68 | | ax-1ne0 9884 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ≠
0 |
69 | | s0s1 13517 |
. . . . . . . . . . . . . . . . . . . 20
⊢
〈“{0, 1}”〉 = (∅ ++ 〈“{0,
1}”〉) |
70 | 28, 65, 25, 66, 67, 40, 68, 69 | vdegp1bi 26512 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 VDeg 〈“{0,
1}”〉)‘0) = 1 |
71 | | df-2 10956 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 = (1 +
1) |
72 | | 2ne0 10990 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≠
0 |
73 | 28, 42, 25, 70, 71, 51, 72, 33 | vdegp1bi 26512 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 VDeg 〈“{0, 1} {0,
2}”〉)‘0) = 2 |
74 | 28, 53, 25, 73, 13, 56, 4, 32 | vdegp1bi 26512 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3}”〉)‘0) = 3 |
75 | 28, 58, 25, 74, 40, 68, 51, 72, 31 | vdegp1ai 26511 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3} {1, 2}”〉)‘0) = 3 |
76 | 28, 60, 25, 75, 40, 68, 51, 72, 30 | vdegp1ai 26511 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3} {1, 2} {1, 2}”〉)‘0) = 3 |
77 | 28, 61, 25, 76, 51, 72, 56, 4, 29 | vdegp1ai 26511 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3} {1, 2} {1, 2} {2, 3}”〉)‘0) = 3 |
78 | | konigsberg.e |
. . . . . . . . . . . . . . 15
⊢ 𝐸 = 〈“{0, 1} {0, 2}
{0, 3} {1, 2} {1, 2} {2, 3} {2, 3}”〉 |
79 | | df-s7 13449 |
. . . . . . . . . . . . . . 15
⊢
〈“{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}”〉) |
80 | 78, 79 | eqtri 2632 |
. . . . . . . . . . . . . 14
⊢ 𝐸 = (〈“{0, 1} {0, 2}
{0, 3} {1, 2} {1, 2} {2, 3}”〉 ++ 〈“{2,
3}”〉) |
81 | 28, 63, 25, 77, 51, 72, 56, 4, 80 | vdegp1ai 26511 |
. . . . . . . . . . . . 13
⊢ ((𝑉 VDeg 𝐸)‘0) = 3 |
82 | 27, 81 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑥 = 0 → ((𝑉 VDeg 𝐸)‘𝑥) = 3) |
83 | 82 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑥 = 0 → (2 ∥ ((𝑉 VDeg 𝐸)‘𝑥) ↔ 2 ∥ 3)) |
84 | 83 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑥 = 0 → (¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥) ↔ ¬ 2 ∥ 3)) |
85 | 84 | elrab 3331 |
. . . . . . . . 9
⊢ (0 ∈
{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ↔ (0 ∈ 𝑉 ∧ ¬ 2 ∥ 3)) |
86 | 25, 26, 85 | mpbir2an 957 |
. . . . . . . 8
⊢ 0 ∈
{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} |
87 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 1 → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘1)) |
88 | 28, 40 | vdeg0i 26509 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 VDeg ∅)‘1) =
0 |
89 | | 0ne1 10965 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≠
1 |
90 | 28, 65, 40, 88, 67, 25, 89, 69 | vdegp1ci 26513 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 VDeg 〈“{0,
1}”〉)‘1) = 1 |
91 | | 1lt2 11071 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 <
2 |
92 | 5, 91 | gtneii 10028 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≠
1 |
93 | 28, 42, 40, 90, 25, 89, 51, 92, 33 | vdegp1ai 26511 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 VDeg 〈“{0, 1} {0,
2}”〉)‘1) = 1 |
94 | 28, 53, 40, 93, 25, 89, 56, 7, 32 | vdegp1ai 26511 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3}”〉)‘1) = 1 |
95 | 28, 58, 40, 94, 71, 51, 92, 31 | vdegp1bi 26512 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3} {1, 2}”〉)‘1) = 2 |
96 | 28, 60, 40, 95, 13, 51, 92, 30 | vdegp1bi 26512 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3} {1, 2} {1, 2}”〉)‘1) = 3 |
97 | 28, 61, 40, 96, 51, 92, 56, 7, 29 | vdegp1ai 26511 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3} {1, 2} {1, 2} {2, 3}”〉)‘1) = 3 |
98 | 28, 63, 40, 97, 51, 92, 56, 7, 80 | vdegp1ai 26511 |
. . . . . . . . . . . . 13
⊢ ((𝑉 VDeg 𝐸)‘1) = 3 |
99 | 87, 98 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑥 = 1 → ((𝑉 VDeg 𝐸)‘𝑥) = 3) |
100 | 99 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑥 = 1 → (2 ∥ ((𝑉 VDeg 𝐸)‘𝑥) ↔ 2 ∥ 3)) |
101 | 100 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑥 = 1 → (¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥) ↔ ¬ 2 ∥ 3)) |
102 | 101 | elrab 3331 |
. . . . . . . . 9
⊢ (1 ∈
{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ↔ (1 ∈ 𝑉 ∧ ¬ 2 ∥ 3)) |
103 | 40, 26, 102 | mpbir2an 957 |
. . . . . . . 8
⊢ 1 ∈
{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} |
104 | | prssi 4293 |
. . . . . . . 8
⊢ ((0
∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ∧ 1 ∈ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) → {0, 1} ⊆ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) |
105 | 86, 103, 104 | mp2an 704 |
. . . . . . 7
⊢ {0, 1}
⊆ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} |
106 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 3 → ((𝑉 VDeg 𝐸)‘𝑥) = ((𝑉 VDeg 𝐸)‘3)) |
107 | 28, 56 | vdeg0i 26509 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 VDeg ∅)‘3) =
0 |
108 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℝ |
109 | | 3pos 10991 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 <
3 |
110 | 108, 109 | ltneii 10029 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 ≠
3 |
111 | 5, 6 | ltneii 10029 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ≠
3 |
112 | 28, 65, 56, 107, 25, 110, 40, 111, 69 | vdegp1ai 26511 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑉 VDeg 〈“{0,
1}”〉)‘3) = 0 |
113 | 43, 45 | ltneii 10029 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≠
3 |
114 | 28, 42, 56, 112, 25, 110, 51, 113, 33 | vdegp1ai 26511 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑉 VDeg 〈“{0, 1} {0,
2}”〉)‘3) = 0 |
115 | 28, 53, 56, 114, 67, 25, 110, 32 | vdegp1ci 26513 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3}”〉)‘3) = 1 |
116 | 28, 58, 56, 115, 40, 111, 51, 113, 31 | vdegp1ai 26511 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3} {1, 2}”〉)‘3) = 1 |
117 | 28, 60, 56, 116, 40, 111, 51, 113, 30 | vdegp1ai 26511 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3} {1, 2} {1, 2}”〉)‘3) = 1 |
118 | 28, 61, 56, 117, 71, 51, 113, 29 | vdegp1ci 26513 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 VDeg 〈“{0, 1} {0, 2}
{0, 3} {1, 2} {1, 2} {2, 3}”〉)‘3) = 2 |
119 | 28, 63, 56, 118, 13, 51, 113, 80 | vdegp1ci 26513 |
. . . . . . . . . . . . 13
⊢ ((𝑉 VDeg 𝐸)‘3) = 3 |
120 | 106, 119 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (𝑥 = 3 → ((𝑉 VDeg 𝐸)‘𝑥) = 3) |
121 | 120 | breq2d 4595 |
. . . . . . . . . . 11
⊢ (𝑥 = 3 → (2 ∥ ((𝑉 VDeg 𝐸)‘𝑥) ↔ 2 ∥ 3)) |
122 | 121 | notbid 307 |
. . . . . . . . . 10
⊢ (𝑥 = 3 → (¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥) ↔ ¬ 2 ∥ 3)) |
123 | 122 | elrab 3331 |
. . . . . . . . 9
⊢ (3 ∈
{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ↔ (3 ∈ 𝑉 ∧ ¬ 2 ∥ 3)) |
124 | 56, 26, 123 | mpbir2an 957 |
. . . . . . . 8
⊢ 3 ∈
{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} |
125 | | snssi 4280 |
. . . . . . . 8
⊢ (3 ∈
{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} → {3} ⊆ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) |
126 | 124, 125 | ax-mp 5 |
. . . . . . 7
⊢ {3}
⊆ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} |
127 | 105, 126 | unssi 3750 |
. . . . . 6
⊢ ({0, 1}
∪ {3}) ⊆ {𝑥
∈ 𝑉 ∣ ¬ 2
∥ ((𝑉 VDeg 𝐸)‘𝑥)} |
128 | | ssdomg 7887 |
. . . . . 6
⊢ ({𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ∈ Fin → (({0, 1} ∪ {3})
⊆ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} → ({0, 1} ∪ {3}) ≼ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)})) |
129 | 20, 127, 128 | mp2 9 |
. . . . 5
⊢ ({0, 1}
∪ {3}) ≼ {𝑥
∈ 𝑉 ∣ ¬ 2
∥ ((𝑉 VDeg 𝐸)‘𝑥)} |
130 | | snfi 7923 |
. . . . . . 7
⊢ {3}
∈ Fin |
131 | | unfi 8112 |
. . . . . . 7
⊢ (({0, 1}
∈ Fin ∧ {3} ∈ Fin) → ({0, 1} ∪ {3}) ∈
Fin) |
132 | 3, 130, 131 | mp2an 704 |
. . . . . 6
⊢ ({0, 1}
∪ {3}) ∈ Fin |
133 | | hashdom 13029 |
. . . . . 6
⊢ ((({0, 1}
∪ {3}) ∈ Fin ∧ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ∈ Fin) → ((#‘({0, 1} ∪
{3})) ≤ (#‘{𝑥
∈ 𝑉 ∣ ¬ 2
∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ↔ ({0, 1} ∪ {3}) ≼ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)})) |
134 | 132, 20, 133 | mp2an 704 |
. . . . 5
⊢
((#‘({0, 1} ∪ {3})) ≤ (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ↔ ({0, 1} ∪ {3}) ≼ {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) |
135 | 129, 134 | mpbir 220 |
. . . 4
⊢
(#‘({0, 1} ∪ {3})) ≤ (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) |
136 | 14, 135 | eqbrtrri 4606 |
. . 3
⊢ 3 ≤
(#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) |
137 | | hashcl 13009 |
. . . . . 6
⊢ ({𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} ∈ Fin → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ∈
ℕ0) |
138 | 20, 137 | ax-mp 5 |
. . . . 5
⊢
(#‘{𝑥 ∈
𝑉 ∣ ¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥)}) ∈
ℕ0 |
139 | 138 | nn0rei 11180 |
. . . 4
⊢
(#‘{𝑥 ∈
𝑉 ∣ ¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥)}) ∈ ℝ |
140 | 44, 139 | lenlti 10036 |
. . 3
⊢ (3 ≤
(#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ↔ ¬ (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) < 3) |
141 | 136, 140 | mpbi 219 |
. 2
⊢ ¬
(#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) < 3 |
142 | | eupath 26508 |
. . . 4
⊢ ((𝑉 EulPaths 𝐸) ≠ ∅ → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ∈ {0, 2}) |
143 | | elpri 4145 |
. . . 4
⊢
((#‘{𝑥 ∈
𝑉 ∣ ¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥)}) ∈ {0, 2} → ((#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) = 0 ∨ (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) = 2)) |
144 | | id 22 |
. . . . . 6
⊢
((#‘{𝑥 ∈
𝑉 ∣ ¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥)}) = 0 → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) = 0) |
145 | 144, 109 | syl6eqbr 4622 |
. . . . 5
⊢
((#‘{𝑥 ∈
𝑉 ∣ ¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥)}) = 0 → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) < 3) |
146 | | id 22 |
. . . . . 6
⊢
((#‘{𝑥 ∈
𝑉 ∣ ¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥)}) = 2 → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) = 2) |
147 | 146, 45 | syl6eqbr 4622 |
. . . . 5
⊢
((#‘{𝑥 ∈
𝑉 ∣ ¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥)}) = 2 → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) < 3) |
148 | 145, 147 | jaoi 393 |
. . . 4
⊢
(((#‘{𝑥 ∈
𝑉 ∣ ¬ 2 ∥
((𝑉 VDeg 𝐸)‘𝑥)}) = 0 ∨ (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) = 2) → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) < 3) |
149 | 142, 143,
148 | 3syl 18 |
. . 3
⊢ ((𝑉 EulPaths 𝐸) ≠ ∅ → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) < 3) |
150 | 149 | necon1bi 2810 |
. 2
⊢ (¬
(#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) < 3 → (𝑉 EulPaths 𝐸) = ∅) |
151 | 141, 150 | ax-mp 5 |
1
⊢ (𝑉 EulPaths 𝐸) = ∅ |