Proof of Theorem constr3trllem3
Step | Hyp | Ref
| Expression |
1 | | 0z 11265 |
. . . . . 6
⊢ 0 ∈
ℤ |
2 | | 1z 11284 |
. . . . . 6
⊢ 1 ∈
ℤ |
3 | 1, 2 | pm3.2i 470 |
. . . . 5
⊢ (0 ∈
ℤ ∧ 1 ∈ ℤ) |
4 | 3 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (0 ∈ ℤ ∧ 1 ∈
ℤ)) |
5 | | 3simpa 1051 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉)) |
6 | | 0ne1 10965 |
. . . . 5
⊢ 0 ≠
1 |
7 | 6 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 0 ≠ 1) |
8 | | fprg 6327 |
. . . . 5
⊢ (((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 0 ≠ 1) → {〈0, 𝐴〉, 〈1, 𝐵〉}:{0, 1}⟶{𝐴, 𝐵}) |
9 | | 0p1e1 11009 |
. . . . . . . . 9
⊢ (0 + 1) =
1 |
10 | 9 | eqcomi 2619 |
. . . . . . . 8
⊢ 1 = (0 +
1) |
11 | 10 | oveq2i 6560 |
. . . . . . 7
⊢ (0...1) =
(0...(0 + 1)) |
12 | | fzpr 12266 |
. . . . . . . 8
⊢ (0 ∈
ℤ → (0...(0 + 1)) = {0, (0 + 1)}) |
13 | 1, 12 | ax-mp 5 |
. . . . . . 7
⊢ (0...(0 +
1)) = {0, (0 + 1)} |
14 | 9 | preq2i 4216 |
. . . . . . 7
⊢ {0, (0 +
1)} = {0, 1} |
15 | 11, 13, 14 | 3eqtri 2636 |
. . . . . 6
⊢ (0...1) =
{0, 1} |
16 | 15 | feq2i 5950 |
. . . . 5
⊢
({〈0, 𝐴〉,
〈1, 𝐵〉}:(0...1)⟶{𝐴, 𝐵} ↔ {〈0, 𝐴〉, 〈1, 𝐵〉}:{0, 1}⟶{𝐴, 𝐵}) |
17 | 8, 16 | sylibr 223 |
. . . 4
⊢ (((0
∈ ℤ ∧ 1 ∈ ℤ) ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 0 ≠ 1) → {〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶{𝐴, 𝐵}) |
18 | 4, 5, 7, 17 | syl3anc 1318 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶{𝐴, 𝐵}) |
19 | | prssi 4293 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → {𝐴, 𝐵} ⊆ 𝑉) |
20 | 19 | 3adant3 1074 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {𝐴, 𝐵} ⊆ 𝑉) |
21 | 18, 20 | fssd 5970 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉) |
22 | | 2nn0 11186 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
23 | | 3nn0 11187 |
. . . . . 6
⊢ 3 ∈
ℕ0 |
24 | 22, 23 | pm3.2i 470 |
. . . . 5
⊢ (2 ∈
ℕ0 ∧ 3 ∈ ℕ0) |
25 | 24 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (2 ∈ ℕ0 ∧
3 ∈ ℕ0)) |
26 | | pm3.22 464 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
27 | 26 | 3adant2 1073 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉)) |
28 | | 2re 10967 |
. . . . . 6
⊢ 2 ∈
ℝ |
29 | | 2lt3 11072 |
. . . . . 6
⊢ 2 <
3 |
30 | 28, 29 | ltneii 10029 |
. . . . 5
⊢ 2 ≠
3 |
31 | 30 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 2 ≠ 3) |
32 | | fprg 6327 |
. . . . 5
⊢ (((2
∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ 2 ≠ 3) → {〈2, 𝐶〉, 〈3, 𝐴〉}:{2, 3}⟶{𝐶, 𝐴}) |
33 | | constr3cycl.f |
. . . . . . . . . 10
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉} |
34 | | constr3cycl.p |
. . . . . . . . . 10
⊢ 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) |
35 | 33, 34 | constr3lem2 26174 |
. . . . . . . . 9
⊢
(#‘𝐹) =
3 |
36 | | df-3 10957 |
. . . . . . . . 9
⊢ 3 = (2 +
1) |
37 | 35, 36 | eqtri 2632 |
. . . . . . . 8
⊢
(#‘𝐹) = (2 +
1) |
38 | 37 | oveq2i 6560 |
. . . . . . 7
⊢
(2...(#‘𝐹)) =
(2...(2 + 1)) |
39 | | 2z 11286 |
. . . . . . . 8
⊢ 2 ∈
ℤ |
40 | | fzpr 12266 |
. . . . . . . 8
⊢ (2 ∈
ℤ → (2...(2 + 1)) = {2, (2 + 1)}) |
41 | 39, 40 | ax-mp 5 |
. . . . . . 7
⊢ (2...(2 +
1)) = {2, (2 + 1)} |
42 | 36 | eqcomi 2619 |
. . . . . . . 8
⊢ (2 + 1) =
3 |
43 | 42 | preq2i 4216 |
. . . . . . 7
⊢ {2, (2 +
1)} = {2, 3} |
44 | 38, 41, 43 | 3eqtri 2636 |
. . . . . 6
⊢
(2...(#‘𝐹)) =
{2, 3} |
45 | 44 | feq2i 5950 |
. . . . 5
⊢
({〈2, 𝐶〉,
〈3, 𝐴〉}:(2...(#‘𝐹))⟶{𝐶, 𝐴} ↔ {〈2, 𝐶〉, 〈3, 𝐴〉}:{2, 3}⟶{𝐶, 𝐴}) |
46 | 32, 45 | sylibr 223 |
. . . 4
⊢ (((2
∈ ℕ0 ∧ 3 ∈ ℕ0) ∧ (𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) ∧ 2 ≠ 3) → {〈2, 𝐶〉, 〈3, 𝐴〉}:(2...(#‘𝐹))⟶{𝐶, 𝐴}) |
47 | 25, 27, 31, 46 | syl3anc 1318 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {〈2, 𝐶〉, 〈3, 𝐴〉}:(2...(#‘𝐹))⟶{𝐶, 𝐴}) |
48 | | prssi 4293 |
. . . . 5
⊢ ((𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉) → {𝐶, 𝐴} ⊆ 𝑉) |
49 | 48 | ancoms 468 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {𝐶, 𝐴} ⊆ 𝑉) |
50 | 49 | 3adant2 1073 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {𝐶, 𝐴} ⊆ 𝑉) |
51 | 47, 50 | fssd 5970 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {〈2, 𝐶〉, 〈3, 𝐴〉}:(2...(#‘𝐹))⟶𝑉) |
52 | | 1lt2 11071 |
. . 3
⊢ 1 <
2 |
53 | | fzdisj 12239 |
. . 3
⊢ (1 < 2
→ ((0...1) ∩ (2...(#‘𝐹))) = ∅) |
54 | 52, 53 | mp1i 13 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((0...1) ∩ (2...(#‘𝐹))) = ∅) |
55 | | fun 5979 |
. . 3
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉 ∧ {〈2, 𝐶〉, 〈3, 𝐴〉}:(2...(#‘𝐹))⟶𝑉) ∧ ((0...1) ∩ (2...(#‘𝐹))) = ∅) → ({〈0,
𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}):((0...1) ∪
(2...(#‘𝐹)))⟶(𝑉 ∪ 𝑉)) |
56 | 34 | a1i 11 |
. . . 4
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉 ∧ {〈2, 𝐶〉, 〈3, 𝐴〉}:(2...(#‘𝐹))⟶𝑉) ∧ ((0...1) ∩ (2...(#‘𝐹))) = ∅) → 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉})) |
57 | | 3nn 11063 |
. . . . . . 7
⊢ 3 ∈
ℕ |
58 | 35, 57 | eqeltri 2684 |
. . . . . 6
⊢
(#‘𝐹) ∈
ℕ |
59 | | elnnuz 11600 |
. . . . . 6
⊢
((#‘𝐹) ∈
ℕ ↔ (#‘𝐹)
∈ (ℤ≥‘1)) |
60 | 58, 59 | mpbi 219 |
. . . . 5
⊢
(#‘𝐹) ∈
(ℤ≥‘1) |
61 | | 0le1 10430 |
. . . . . . . . 9
⊢ 0 ≤
1 |
62 | 61 | a1i 11 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
(ℤ≥‘1) → 0 ≤ 1) |
63 | | eluzle 11576 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
(ℤ≥‘1) → 1 ≤ (#‘𝐹)) |
64 | | eluzelz 11573 |
. . . . . . . . 9
⊢
((#‘𝐹) ∈
(ℤ≥‘1) → (#‘𝐹) ∈ ℤ) |
65 | | elfz 12203 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ 0 ∈ ℤ ∧ (#‘𝐹) ∈ ℤ) → (1 ∈
(0...(#‘𝐹)) ↔ (0
≤ 1 ∧ 1 ≤ (#‘𝐹)))) |
66 | 2, 1, 65 | mp3an12 1406 |
. . . . . . . . 9
⊢
((#‘𝐹) ∈
ℤ → (1 ∈ (0...(#‘𝐹)) ↔ (0 ≤ 1 ∧ 1 ≤
(#‘𝐹)))) |
67 | 64, 66 | syl 17 |
. . . . . . . 8
⊢
((#‘𝐹) ∈
(ℤ≥‘1) → (1 ∈ (0...(#‘𝐹)) ↔ (0 ≤ 1 ∧ 1 ≤
(#‘𝐹)))) |
68 | 62, 63, 67 | mpbir2and 959 |
. . . . . . 7
⊢
((#‘𝐹) ∈
(ℤ≥‘1) → 1 ∈ (0...(#‘𝐹))) |
69 | | fzsplit 12238 |
. . . . . . 7
⊢ (1 ∈
(0...(#‘𝐹)) →
(0...(#‘𝐹)) =
((0...1) ∪ ((1 + 1)...(#‘𝐹)))) |
70 | 68, 69 | syl 17 |
. . . . . 6
⊢
((#‘𝐹) ∈
(ℤ≥‘1) → (0...(#‘𝐹)) = ((0...1) ∪ ((1 +
1)...(#‘𝐹)))) |
71 | | df-2 10956 |
. . . . . . . 8
⊢ 2 = (1 +
1) |
72 | 71 | oveq1i 6559 |
. . . . . . 7
⊢
(2...(#‘𝐹)) =
((1 + 1)...(#‘𝐹)) |
73 | 72 | uneq2i 3726 |
. . . . . 6
⊢ ((0...1)
∪ (2...(#‘𝐹))) =
((0...1) ∪ ((1 + 1)...(#‘𝐹))) |
74 | 70, 73 | syl6eqr 2662 |
. . . . 5
⊢
((#‘𝐹) ∈
(ℤ≥‘1) → (0...(#‘𝐹)) = ((0...1) ∪ (2...(#‘𝐹)))) |
75 | 60, 74 | mp1i 13 |
. . . 4
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉 ∧ {〈2, 𝐶〉, 〈3, 𝐴〉}:(2...(#‘𝐹))⟶𝑉) ∧ ((0...1) ∩ (2...(#‘𝐹))) = ∅) →
(0...(#‘𝐹)) =
((0...1) ∪ (2...(#‘𝐹)))) |
76 | | unidm 3718 |
. . . . . 6
⊢ (𝑉 ∪ 𝑉) = 𝑉 |
77 | 76 | eqcomi 2619 |
. . . . 5
⊢ 𝑉 = (𝑉 ∪ 𝑉) |
78 | 77 | a1i 11 |
. . . 4
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉 ∧ {〈2, 𝐶〉, 〈3, 𝐴〉}:(2...(#‘𝐹))⟶𝑉) ∧ ((0...1) ∩ (2...(#‘𝐹))) = ∅) → 𝑉 = (𝑉 ∪ 𝑉)) |
79 | 56, 75, 78 | feq123d 5947 |
. . 3
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉 ∧ {〈2, 𝐶〉, 〈3, 𝐴〉}:(2...(#‘𝐹))⟶𝑉) ∧ ((0...1) ∩ (2...(#‘𝐹))) = ∅) → (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}):((0...1) ∪ (2...(#‘𝐹)))⟶(𝑉 ∪ 𝑉))) |
80 | 55, 79 | mpbird 246 |
. 2
⊢
((({〈0, 𝐴〉, 〈1, 𝐵〉}:(0...1)⟶𝑉 ∧ {〈2, 𝐶〉, 〈3, 𝐴〉}:(2...(#‘𝐹))⟶𝑉) ∧ ((0...1) ∩ (2...(#‘𝐹))) = ∅) → 𝑃:(0...(#‘𝐹))⟶𝑉) |
81 | 21, 51, 54, 80 | syl21anc 1317 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝑃:(0...(#‘𝐹))⟶𝑉) |