Proof of Theorem constr3pthlem3
Step | Hyp | Ref
| Expression |
1 | | constr3cycl.f |
. . 3
⊢ 𝐹 = {〈0, (◡𝐸‘{𝐴, 𝐵})〉, 〈1, (◡𝐸‘{𝐵, 𝐶})〉, 〈2, (◡𝐸‘{𝐶, 𝐴})〉} |
2 | | constr3cycl.p |
. . 3
⊢ 𝑃 = ({〈0, 𝐴〉, 〈1, 𝐵〉} ∪ {〈2, 𝐶〉, 〈3, 𝐴〉}) |
3 | 1, 2 | constr3lem2 26174 |
. 2
⊢
(#‘𝐹) =
3 |
4 | | preq2 4213 |
. . . . 5
⊢
((#‘𝐹) = 3
→ {0, (#‘𝐹)} =
{0, 3}) |
5 | 4 | imaeq2d 5385 |
. . . 4
⊢
((#‘𝐹) = 3
→ (𝑃 “ {0,
(#‘𝐹)}) = (𝑃 “ {0,
3})) |
6 | | oveq2 6557 |
. . . . 5
⊢
((#‘𝐹) = 3
→ (1..^(#‘𝐹)) =
(1..^3)) |
7 | 6 | imaeq2d 5385 |
. . . 4
⊢
((#‘𝐹) = 3
→ (𝑃 “
(1..^(#‘𝐹))) = (𝑃 “
(1..^3))) |
8 | 5, 7 | ineq12d 3777 |
. . 3
⊢
((#‘𝐹) = 3
→ ((𝑃 “ {0,
(#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ((𝑃 “ {0, 3}) ∩ (𝑃 “ (1..^3)))) |
9 | 1, 2 | constr3lem6 26177 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ({(𝑃‘0), (𝑃‘3)} ∩ {(𝑃‘1), (𝑃‘2)}) = ∅) |
10 | 1, 2 | constr3trllem4 26181 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝑃:(0...3)⟶𝑉) |
11 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝑃:(0...3)⟶𝑉 → 𝑃 Fn (0...3)) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝑃 Fn (0...3)) |
13 | | 3nn0 11187 |
. . . . . . . . . 10
⊢ 3 ∈
ℕ0 |
14 | | elnn0uz 11601 |
. . . . . . . . . 10
⊢ (3 ∈
ℕ0 ↔ 3 ∈
(ℤ≥‘0)) |
15 | 13, 14 | mpbi 219 |
. . . . . . . . 9
⊢ 3 ∈
(ℤ≥‘0) |
16 | | eluzfz1 12219 |
. . . . . . . . 9
⊢ (3 ∈
(ℤ≥‘0) → 0 ∈ (0...3)) |
17 | 15, 16 | mp1i 13 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 0 ∈ (0...3)) |
18 | | eluzfz2 12220 |
. . . . . . . . 9
⊢ (3 ∈
(ℤ≥‘0) → 3 ∈ (0...3)) |
19 | 15, 18 | mp1i 13 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 3 ∈ (0...3)) |
20 | | fnimapr 6172 |
. . . . . . . 8
⊢ ((𝑃 Fn (0...3) ∧ 0 ∈
(0...3) ∧ 3 ∈ (0...3)) → (𝑃 “ {0, 3}) = {(𝑃‘0), (𝑃‘3)}) |
21 | 12, 17, 19, 20 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃 “ {0, 3}) = {(𝑃‘0), (𝑃‘3)}) |
22 | | 3z 11287 |
. . . . . . . . . . 11
⊢ 3 ∈
ℤ |
23 | | fzoval 12340 |
. . . . . . . . . . 11
⊢ (3 ∈
ℤ → (1..^3) = (1...(3 − 1))) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . 10
⊢ (1..^3) =
(1...(3 − 1)) |
25 | | 3m1e2 11014 |
. . . . . . . . . . 11
⊢ (3
− 1) = 2 |
26 | 25 | oveq2i 6560 |
. . . . . . . . . 10
⊢ (1...(3
− 1)) = (1...2) |
27 | 24, 26 | eqtri 2632 |
. . . . . . . . 9
⊢ (1..^3) =
(1...2) |
28 | 27 | imaeq2i 5383 |
. . . . . . . 8
⊢ (𝑃 “ (1..^3)) = (𝑃 “
(1...2)) |
29 | | df-2 10956 |
. . . . . . . . . . . 12
⊢ 2 = (1 +
1) |
30 | 29 | oveq2i 6560 |
. . . . . . . . . . 11
⊢ (1...2) =
(1...(1 + 1)) |
31 | | 1z 11284 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
32 | | fzpr 12266 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → (1...(1 + 1)) = {1, (1 + 1)}) |
33 | 31, 32 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (1...(1 +
1)) = {1, (1 + 1)} |
34 | | 1p1e2 11011 |
. . . . . . . . . . . 12
⊢ (1 + 1) =
2 |
35 | 34 | preq2i 4216 |
. . . . . . . . . . 11
⊢ {1, (1 +
1)} = {1, 2} |
36 | 30, 33, 35 | 3eqtri 2636 |
. . . . . . . . . 10
⊢ (1...2) =
{1, 2} |
37 | 36 | imaeq2i 5383 |
. . . . . . . . 9
⊢ (𝑃 “ (1...2)) = (𝑃 “ {1,
2}) |
38 | | 1eluzge0 11608 |
. . . . . . . . . . . 12
⊢ 1 ∈
(ℤ≥‘0) |
39 | | 1le3 11121 |
. . . . . . . . . . . . 13
⊢ 1 ≤
3 |
40 | | elfz5 12205 |
. . . . . . . . . . . . 13
⊢ ((1
∈ (ℤ≥‘0) ∧ 3 ∈ ℤ) → (1
∈ (0...3) ↔ 1 ≤ 3)) |
41 | 39, 40 | mpbiri 247 |
. . . . . . . . . . . 12
⊢ ((1
∈ (ℤ≥‘0) ∧ 3 ∈ ℤ) → 1 ∈
(0...3)) |
42 | 38, 22, 41 | mp2an 704 |
. . . . . . . . . . 11
⊢ 1 ∈
(0...3) |
43 | 42 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 1 ∈ (0...3)) |
44 | | 2eluzge0 11609 |
. . . . . . . . . . . 12
⊢ 2 ∈
(ℤ≥‘0) |
45 | | 2re 10967 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
46 | | 3re 10971 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℝ |
47 | | 2lt3 11072 |
. . . . . . . . . . . . . 14
⊢ 2 <
3 |
48 | 45, 46, 47 | ltleii 10039 |
. . . . . . . . . . . . 13
⊢ 2 ≤
3 |
49 | | elfz5 12205 |
. . . . . . . . . . . . 13
⊢ ((2
∈ (ℤ≥‘0) ∧ 3 ∈ ℤ) → (2
∈ (0...3) ↔ 2 ≤ 3)) |
50 | 48, 49 | mpbiri 247 |
. . . . . . . . . . . 12
⊢ ((2
∈ (ℤ≥‘0) ∧ 3 ∈ ℤ) → 2 ∈
(0...3)) |
51 | 44, 22, 50 | mp2an 704 |
. . . . . . . . . . 11
⊢ 2 ∈
(0...3) |
52 | 51 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 2 ∈ (0...3)) |
53 | | fnimapr 6172 |
. . . . . . . . . 10
⊢ ((𝑃 Fn (0...3) ∧ 1 ∈
(0...3) ∧ 2 ∈ (0...3)) → (𝑃 “ {1, 2}) = {(𝑃‘1), (𝑃‘2)}) |
54 | 12, 43, 52, 53 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃 “ {1, 2}) = {(𝑃‘1), (𝑃‘2)}) |
55 | 37, 54 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃 “ (1...2)) = {(𝑃‘1), (𝑃‘2)}) |
56 | 28, 55 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃 “ (1..^3)) = {(𝑃‘1), (𝑃‘2)}) |
57 | 21, 56 | ineq12d 3777 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑃 “ {0, 3}) ∩ (𝑃 “ (1..^3))) = ({(𝑃‘0), (𝑃‘3)} ∩ {(𝑃‘1), (𝑃‘2)})) |
58 | 57 | eqeq1d 2612 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (((𝑃 “ {0, 3}) ∩ (𝑃 “ (1..^3))) = ∅ ↔ ({(𝑃‘0), (𝑃‘3)} ∩ {(𝑃‘1), (𝑃‘2)}) = ∅)) |
59 | 58 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → (((𝑃 “ {0, 3}) ∩ (𝑃 “ (1..^3))) = ∅ ↔ ({(𝑃‘0), (𝑃‘3)} ∩ {(𝑃‘1), (𝑃‘2)}) = ∅)) |
60 | 9, 59 | mpbird 246 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ((𝑃 “ {0, 3}) ∩ (𝑃 “ (1..^3))) =
∅) |
61 | 8, 60 | sylan9eq 2664 |
. 2
⊢
(((#‘𝐹) = 3
∧ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴))) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |
62 | 3, 61 | mpan 702 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴)) → ((𝑃 “ {0, (#‘𝐹)}) ∩ (𝑃 “ (1..^(#‘𝐹)))) = ∅) |