Proof of Theorem cgracol
| Step | Hyp | Ref
| Expression |
| 1 | | cgracol.p |
. . . . . . . . . 10
⊢ 𝑃 = (Base‘𝐺) |
| 2 | | cgracol.i |
. . . . . . . . . 10
⊢ 𝐼 = (Itv‘𝐺) |
| 3 | | cgracol.m |
. . . . . . . . . 10
⊢ − =
(dist‘𝐺) |
| 4 | | cgracol.g |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ TarskiG) |
| 5 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐺 ∈ TarskiG) |
| 6 | | cgracol.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝑃) |
| 7 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐴 ∈ 𝑃) |
| 8 | | cgracol.b |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ 𝑃) |
| 9 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐵 ∈ 𝑃) |
| 10 | | cgracol.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ 𝑃) |
| 11 | 10 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐶 ∈ 𝑃) |
| 12 | | cgracol.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ 𝑃) |
| 13 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐷 ∈ 𝑃) |
| 14 | | cgracol.e |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ 𝑃) |
| 15 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐸 ∈ 𝑃) |
| 16 | | cgracol.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ 𝑃) |
| 17 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐹 ∈ 𝑃) |
| 18 | | cgracol.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
| 19 | 18 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
| 20 | | eqid 2737 |
. . . . . . . . . 10
⊢
(hlG‘𝐺) =
(hlG‘𝐺) |
| 21 | 1, 2, 20, 4, 6, 8,
10, 12, 14, 16, 18 | cgrane2 28821 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 ≠ 𝐶) |
| 22 | 21 | necomd 2996 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ≠ 𝐵) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ≠ 𝐵) |
| 24 | 1, 2, 20, 4, 6, 8,
10, 12, 14, 16, 18 | cgrane1 28820 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ≠ 𝐵) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐴 ≠ 𝐵) |
| 26 | 4 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐺 ∈ TarskiG) |
| 27 | 6 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐴 ∈ 𝑃) |
| 28 | 10 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ 𝑃) |
| 29 | 8 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐵 ∈ 𝑃) |
| 30 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝐴𝐼𝐵)) |
| 31 | 1, 3, 2, 26, 27, 28, 29, 30 | tgbtwncom 28496 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → 𝐶 ∈ (𝐵𝐼𝐴)) |
| 32 | 31 | orcd 874 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))) |
| 33 | 23, 25, 32 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐶 ∈ (𝐴𝐼𝐵)) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))) |
| 34 | 22 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐶 ≠ 𝐵) |
| 35 | 24 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ≠ 𝐵) |
| 36 | 4 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐺 ∈ TarskiG) |
| 37 | 10 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐶 ∈ 𝑃) |
| 38 | 6 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ 𝑃) |
| 39 | 8 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐵 ∈ 𝑃) |
| 40 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐶𝐼𝐵)) |
| 41 | 1, 3, 2, 36, 37, 38, 39, 40 | tgbtwncom 28496 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → 𝐴 ∈ (𝐵𝐼𝐶)) |
| 42 | 41 | olcd 875 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))) |
| 43 | 34, 35, 42 | 3jca 1129 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 ∈ (𝐶𝐼𝐵)) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))) |
| 44 | 33, 43 | jaodan 960 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶)))) |
| 45 | 1, 2, 20, 10, 6, 8, 4 | ishlg 28610 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶((hlG‘𝐺)‘𝐵)𝐴 ↔ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))) |
| 46 | 45 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐶((hlG‘𝐺)‘𝐵)𝐴 ↔ (𝐶 ≠ 𝐵 ∧ 𝐴 ≠ 𝐵 ∧ (𝐶 ∈ (𝐵𝐼𝐴) ∨ 𝐴 ∈ (𝐵𝐼𝐶))))) |
| 47 | 44, 46 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐶((hlG‘𝐺)‘𝐵)𝐴) |
| 48 | 1, 2, 20, 11, 7, 9, 5, 47 | hlcomd 28612 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐴((hlG‘𝐺)‘𝐵)𝐶) |
| 49 | 1, 2, 3, 5, 7, 9, 11, 13, 15, 17, 19, 20, 48 | cgrahl 28835 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐷((hlG‘𝐺)‘𝐸)𝐹) |
| 50 | 1, 2, 20, 13, 17, 15, 5 | ishlg 28610 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷((hlG‘𝐺)‘𝐸)𝐹 ↔ (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷))))) |
| 51 | 49, 50 | mpbid 232 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷 ≠ 𝐸 ∧ 𝐹 ≠ 𝐸 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷)))) |
| 52 | 51 | simp3d 1145 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷))) |
| 53 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐺 ∈ TarskiG) |
| 54 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐸 ∈ 𝑃) |
| 55 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷 ∈ 𝑃) |
| 56 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐹 ∈ 𝑃) |
| 57 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷 ∈ (𝐸𝐼𝐹)) |
| 58 | 1, 3, 2, 53, 54, 55, 56, 57 | tgbtwncom 28496 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → 𝐷 ∈ (𝐹𝐼𝐸)) |
| 59 | 58 | olcd 875 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐷 ∈ (𝐸𝐼𝐹)) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸))) |
| 60 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐺 ∈ TarskiG) |
| 61 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐸 ∈ 𝑃) |
| 62 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹 ∈ 𝑃) |
| 63 | 12 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐷 ∈ 𝑃) |
| 64 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹 ∈ (𝐸𝐼𝐷)) |
| 65 | 1, 3, 2, 60, 61, 62, 63, 64 | tgbtwncom 28496 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → 𝐹 ∈ (𝐷𝐼𝐸)) |
| 66 | 65 | orcd 874 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ∈ (𝐸𝐼𝐷)) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸))) |
| 67 | 59, 66 | jaodan 960 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐷 ∈ (𝐸𝐼𝐹) ∨ 𝐹 ∈ (𝐸𝐼𝐷))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸))) |
| 68 | 52, 67 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸))) |
| 69 | 68 | orcd 874 |
. . . . 5
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)) ∨ 𝐸 ∈ (𝐷𝐼𝐹))) |
| 70 | | df-3or 1088 |
. . . . 5
⊢ ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹)) ↔ ((𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸)) ∨ 𝐸 ∈ (𝐷𝐼𝐹))) |
| 71 | 69, 70 | sylibr 234 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹))) |
| 72 | | cgracol.l |
. . . . . 6
⊢ 𝐿 = (LineG‘𝐺) |
| 73 | 1, 2, 4, 20, 6, 8,
10, 12, 14, 16, 18 | cgracom 28830 |
. . . . . . 7
⊢ (𝜑 → 〈“𝐷𝐸𝐹”〉(cgrA‘𝐺)〈“𝐴𝐵𝐶”〉) |
| 74 | 1, 2, 20, 4, 12, 14, 16, 6, 8, 10, 73 | cgrane1 28820 |
. . . . . 6
⊢ (𝜑 → 𝐷 ≠ 𝐸) |
| 75 | 1, 72, 2, 4, 12, 14, 74, 16 | tgellng 28561 |
. . . . 5
⊢ (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ↔ (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))) |
| 76 | 75 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐿𝐸) ↔ (𝐹 ∈ (𝐷𝐼𝐸) ∨ 𝐷 ∈ (𝐹𝐼𝐸) ∨ 𝐸 ∈ (𝐷𝐼𝐹)))) |
| 77 | 71, 76 | mpbird 257 |
. . 3
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → 𝐹 ∈ (𝐷𝐿𝐸)) |
| 78 | 77 | orcd 874 |
. 2
⊢ ((𝜑 ∧ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵))) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) |
| 79 | 4 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐺 ∈ TarskiG) |
| 80 | 12 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐷 ∈ 𝑃) |
| 81 | 14 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸 ∈ 𝑃) |
| 82 | 16 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐹 ∈ 𝑃) |
| 83 | 6 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐴 ∈ 𝑃) |
| 84 | 8 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵 ∈ 𝑃) |
| 85 | 10 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐶 ∈ 𝑃) |
| 86 | 18 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 〈“𝐴𝐵𝐶”〉(cgrA‘𝐺)〈“𝐷𝐸𝐹”〉) |
| 87 | | simpr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐵 ∈ (𝐴𝐼𝐶)) |
| 88 | 1, 2, 3, 79, 83, 84, 85, 80, 81, 82, 86, 87 | cgrabtwn 28834 |
. . 3
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → 𝐸 ∈ (𝐷𝐼𝐹)) |
| 89 | 1, 72, 2, 79, 80, 81, 82, 88 | btwncolg3 28565 |
. 2
⊢ ((𝜑 ∧ 𝐵 ∈ (𝐴𝐼𝐶)) → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) |
| 90 | 24 | neneqd 2945 |
. . . . 5
⊢ (𝜑 → ¬ 𝐴 = 𝐵) |
| 91 | | cgracol.2 |
. . . . . . 7
⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ∨ 𝐴 = 𝐵)) |
| 92 | 91 | orcomd 872 |
. . . . . 6
⊢ (𝜑 → (𝐴 = 𝐵 ∨ 𝐶 ∈ (𝐴𝐿𝐵))) |
| 93 | 92 | ord 865 |
. . . . 5
⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝐶 ∈ (𝐴𝐿𝐵))) |
| 94 | 90, 93 | mpd 15 |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐴𝐿𝐵)) |
| 95 | 1, 72, 2, 4, 6, 8, 24, 10 | tgellng 28561 |
. . . 4
⊢ (𝜑 → (𝐶 ∈ (𝐴𝐿𝐵) ↔ (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)))) |
| 96 | 94, 95 | mpbid 232 |
. . 3
⊢ (𝜑 → (𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶))) |
| 97 | | df-3or 1088 |
. . 3
⊢ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵) ∨ 𝐵 ∈ (𝐴𝐼𝐶)) ↔ ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶))) |
| 98 | 96, 97 | sylib 218 |
. 2
⊢ (𝜑 → ((𝐶 ∈ (𝐴𝐼𝐵) ∨ 𝐴 ∈ (𝐶𝐼𝐵)) ∨ 𝐵 ∈ (𝐴𝐼𝐶))) |
| 99 | 78, 89, 98 | mpjaodan 961 |
1
⊢ (𝜑 → (𝐹 ∈ (𝐷𝐿𝐸) ∨ 𝐷 = 𝐸)) |