Proof of Theorem 2pthlem2
Step | Hyp | Ref
| Expression |
1 | | 2pth.p |
. . . . . . 7
⊢ 𝑃 = {〈0, 𝐴〉, 〈1, 𝐵〉, 〈2, 𝐶〉} |
2 | 1 | 2trllemD 26087 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 𝑃 Fn {0, 1, 2}) |
3 | | 1ex 9914 |
. . . . . . 7
⊢ 1 ∈
V |
4 | 3 | tpid2 4247 |
. . . . . 6
⊢ 1 ∈
{0, 1, 2} |
5 | | fnsnfv 6168 |
. . . . . 6
⊢ ((𝑃 Fn {0, 1, 2} ∧ 1 ∈ {0,
1, 2}) → {(𝑃‘1)}
= (𝑃 “
{1})) |
6 | 2, 4, 5 | sylancl 693 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(𝑃‘1)} = (𝑃 “ {1})) |
7 | | fzo12sn 12418 |
. . . . . 6
⊢ (1..^2) =
{1} |
8 | 7 | imaeq2i 5383 |
. . . . 5
⊢ (𝑃 “ (1..^2)) = (𝑃 “ {1}) |
9 | 6, 8 | syl6reqr 2663 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃 “ (1..^2)) = {(𝑃‘1)}) |
10 | 9 | ineq2d 3776 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑃 “ {0, 2}) ∩ (𝑃 “ (1..^2))) = ((𝑃 “ {0, 2}) ∩ {(𝑃‘1)})) |
11 | 10 | adantr 480 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ((𝑃 “ {0, 2}) ∩ (𝑃 “ (1..^2))) = ((𝑃 “ {0, 2}) ∩ {(𝑃‘1)})) |
12 | | c0ex 9913 |
. . . . . . 7
⊢ 0 ∈
V |
13 | 12 | tpid1 4246 |
. . . . . 6
⊢ 0 ∈
{0, 1, 2} |
14 | 13 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 0 ∈ {0, 1,
2}) |
15 | | 2ex 10969 |
. . . . . . 7
⊢ 2 ∈
V |
16 | 15 | tpid3 4250 |
. . . . . 6
⊢ 2 ∈
{0, 1, 2} |
17 | 16 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → 2 ∈ {0, 1,
2}) |
18 | | fnimapr 6172 |
. . . . 5
⊢ ((𝑃 Fn {0, 1, 2} ∧ 0 ∈ {0,
1, 2} ∧ 2 ∈ {0, 1, 2}) → (𝑃 “ {0, 2}) = {(𝑃‘0), (𝑃‘2)}) |
19 | 2, 14, 17, 18 | syl3anc 1318 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃 “ {0, 2}) = {(𝑃‘0), (𝑃‘2)}) |
20 | 19 | ineq1d 3775 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ((𝑃 “ {0, 2}) ∩ {(𝑃‘1)}) = ({(𝑃‘0), (𝑃‘2)} ∩ {(𝑃‘1)})) |
21 | 20 | adantr 480 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ((𝑃 “ {0, 2}) ∩ {(𝑃‘1)}) = ({(𝑃‘0), (𝑃‘2)} ∩ {(𝑃‘1)})) |
22 | 1 | 2wlklemA 26084 |
. . . . . 6
⊢ (𝐴 ∈ 𝑉 → (𝑃‘0) = 𝐴) |
23 | 22 | 3ad2ant1 1075 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃‘0) = 𝐴) |
24 | 1 | 2wlklemC 26086 |
. . . . . 6
⊢ (𝐶 ∈ 𝑉 → (𝑃‘2) = 𝐶) |
25 | 24 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃‘2) = 𝐶) |
26 | 23, 25 | preq12d 4220 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(𝑃‘0), (𝑃‘2)} = {𝐴, 𝐶}) |
27 | 1 | 2wlklemB 26085 |
. . . . . 6
⊢ (𝐵 ∈ 𝑉 → (𝑃‘1) = 𝐵) |
28 | 27 | 3ad2ant2 1076 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝑃‘1) = 𝐵) |
29 | 28 | sneqd 4137 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → {(𝑃‘1)} = {𝐵}) |
30 | 26, 29 | ineq12d 3777 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → ({(𝑃‘0), (𝑃‘2)} ∩ {(𝑃‘1)}) = ({𝐴, 𝐶} ∩ {𝐵})) |
31 | | elpri 4145 |
. . . . . . 7
⊢ (𝐵 ∈ {𝐴, 𝐶} → (𝐵 = 𝐴 ∨ 𝐵 = 𝐶)) |
32 | | nne 2786 |
. . . . . . . . . 10
⊢ (¬
𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵) |
33 | 32 | biimpri 217 |
. . . . . . . . 9
⊢ (𝐴 = 𝐵 → ¬ 𝐴 ≠ 𝐵) |
34 | 33 | eqcoms 2618 |
. . . . . . . 8
⊢ (𝐵 = 𝐴 → ¬ 𝐴 ≠ 𝐵) |
35 | | nne 2786 |
. . . . . . . . 9
⊢ (¬
𝐵 ≠ 𝐶 ↔ 𝐵 = 𝐶) |
36 | 35 | biimpri 217 |
. . . . . . . 8
⊢ (𝐵 = 𝐶 → ¬ 𝐵 ≠ 𝐶) |
37 | 34, 36 | orim12i 537 |
. . . . . . 7
⊢ ((𝐵 = 𝐴 ∨ 𝐵 = 𝐶) → (¬ 𝐴 ≠ 𝐵 ∨ ¬ 𝐵 ≠ 𝐶)) |
38 | 31, 37 | syl 17 |
. . . . . 6
⊢ (𝐵 ∈ {𝐴, 𝐶} → (¬ 𝐴 ≠ 𝐵 ∨ ¬ 𝐵 ≠ 𝐶)) |
39 | | ianor 508 |
. . . . . 6
⊢ (¬
(𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) ↔ (¬ 𝐴 ≠ 𝐵 ∨ ¬ 𝐵 ≠ 𝐶)) |
40 | 38, 39 | sylibr 223 |
. . . . 5
⊢ (𝐵 ∈ {𝐴, 𝐶} → ¬ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) |
41 | 40 | con2i 133 |
. . . 4
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ¬ 𝐵 ∈ {𝐴, 𝐶}) |
42 | | disjsn 4192 |
. . . 4
⊢ (({𝐴, 𝐶} ∩ {𝐵}) = ∅ ↔ ¬ 𝐵 ∈ {𝐴, 𝐶}) |
43 | 41, 42 | sylibr 223 |
. . 3
⊢ ((𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶) → ({𝐴, 𝐶} ∩ {𝐵}) = ∅) |
44 | 30, 43 | sylan9eq 2664 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ({(𝑃‘0), (𝑃‘2)} ∩ {(𝑃‘1)}) = ∅) |
45 | 11, 21, 44 | 3eqtrd 2648 |
1
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) ∧ (𝐴 ≠ 𝐵 ∧ 𝐵 ≠ 𝐶)) → ((𝑃 “ {0, 2}) ∩ (𝑃 “ (1..^2))) =
∅) |