Proof of Theorem oppcom
Step | Hyp | Ref
| Expression |
1 | | oppcom.o |
. . . . . 6
⊢ (𝜑 → 𝐴𝑂𝐵) |
2 | | hpg.p |
. . . . . . 7
⊢ 𝑃 = (Base‘𝐺) |
3 | | hpg.d |
. . . . . . 7
⊢ − =
(dist‘𝐺) |
4 | | hpg.i |
. . . . . . 7
⊢ 𝐼 = (Itv‘𝐺) |
5 | | hpg.o |
. . . . . . 7
⊢ 𝑂 = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (𝑃 ∖ 𝐷) ∧ 𝑏 ∈ (𝑃 ∖ 𝐷)) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝑎𝐼𝑏))} |
6 | | oppcom.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
7 | | oppcom.b |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
8 | 2, 3, 4, 5, 6, 7 | islnopp 26830 |
. . . . . 6
⊢ (𝜑 → (𝐴𝑂𝐵 ↔ ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵)))) |
9 | 1, 8 | mpbid 235 |
. . . . 5
⊢ (𝜑 → ((¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵))) |
10 | 9 | simpld 498 |
. . . 4
⊢ (𝜑 → (¬ 𝐴 ∈ 𝐷 ∧ ¬ 𝐵 ∈ 𝐷)) |
11 | 10 | simprd 499 |
. . 3
⊢ (𝜑 → ¬ 𝐵 ∈ 𝐷) |
12 | 10 | simpld 498 |
. . 3
⊢ (𝜑 → ¬ 𝐴 ∈ 𝐷) |
13 | 9 | simprd 499 |
. . . 4
⊢ (𝜑 → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵)) |
14 | | opphl.g |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
15 | 14 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG) |
16 | 6 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃) |
17 | | opphl.l |
. . . . . . . . 9
⊢ 𝐿 = (LineG‘𝐺) |
18 | 14 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝐺 ∈ TarskiG) |
19 | | opphl.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ran 𝐿) |
20 | 19 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝐷 ∈ ran 𝐿) |
21 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ 𝐷) |
22 | 2, 17, 4, 18, 20, 21 | tglnpt 26640 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → 𝑡 ∈ 𝑃) |
23 | 22 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝑡 ∈ 𝑃) |
24 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝐵 ∈ 𝑃) |
25 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝑡 ∈ (𝐴𝐼𝐵)) |
26 | 2, 3, 4, 15, 16, 23, 24, 25 | tgbtwncom 26579 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐴𝐼𝐵)) → 𝑡 ∈ (𝐵𝐼𝐴)) |
27 | 14 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐵𝐼𝐴)) → 𝐺 ∈ TarskiG) |
28 | 7 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐵𝐼𝐴)) → 𝐵 ∈ 𝑃) |
29 | 22 | adantr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐵𝐼𝐴)) → 𝑡 ∈ 𝑃) |
30 | 6 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐵𝐼𝐴)) → 𝐴 ∈ 𝑃) |
31 | | simpr 488 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐵𝐼𝐴)) → 𝑡 ∈ (𝐵𝐼𝐴)) |
32 | 2, 3, 4, 27, 28, 29, 30, 31 | tgbtwncom 26579 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ 𝐷) ∧ 𝑡 ∈ (𝐵𝐼𝐴)) → 𝑡 ∈ (𝐴𝐼𝐵)) |
33 | 26, 32 | impbida 801 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝐷) → (𝑡 ∈ (𝐴𝐼𝐵) ↔ 𝑡 ∈ (𝐵𝐼𝐴))) |
34 | 33 | rexbidva 3215 |
. . . 4
⊢ (𝜑 → (∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐴𝐼𝐵) ↔ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐴))) |
35 | 13, 34 | mpbid 235 |
. . 3
⊢ (𝜑 → ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐴)) |
36 | 11, 12, 35 | jca31 518 |
. 2
⊢ (𝜑 → ((¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐴))) |
37 | 2, 3, 4, 5, 7, 6 | islnopp 26830 |
. 2
⊢ (𝜑 → (𝐵𝑂𝐴 ↔ ((¬ 𝐵 ∈ 𝐷 ∧ ¬ 𝐴 ∈ 𝐷) ∧ ∃𝑡 ∈ 𝐷 𝑡 ∈ (𝐵𝐼𝐴)))) |
38 | 36, 37 | mpbird 260 |
1
⊢ (𝜑 → 𝐵𝑂𝐴) |