Proof of Theorem ordtri3or
| Step | Hyp | Ref
| Expression |
| 1 | | ordin 6414 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵)) |
| 2 | | ordirr 6402 |
. . . . . 6
⊢ (Ord
(𝐴 ∩ 𝐵) → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵)) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵)) |
| 4 | | ianor 984 |
. . . . . 6
⊢ (¬
((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵) ↔ (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵)) |
| 5 | | elin 3967 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵)) |
| 6 | | incom 4209 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
| 7 | 6 | eleq1i 2832 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∈ 𝐵 ↔ (𝐵 ∩ 𝐴) ∈ 𝐵) |
| 8 | 7 | anbi2i 623 |
. . . . . . 7
⊢ (((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵)) |
| 9 | 5, 8 | bitri 275 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵)) |
| 10 | 4, 9 | xchnxbir 333 |
. . . . 5
⊢ (¬
(𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵)) |
| 11 | 3, 10 | sylib 218 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵)) |
| 12 | | inss1 4237 |
. . . . . . . . . 10
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
| 13 | | ordsseleq 6413 |
. . . . . . . . . 10
⊢ ((Ord
(𝐴 ∩ 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴))) |
| 14 | 12, 13 | mpbii 233 |
. . . . . . . . 9
⊢ ((Ord
(𝐴 ∩ 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴)) |
| 15 | 1, 14 | sylan 580 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ Ord 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴)) |
| 16 | 15 | anabss1 666 |
. . . . . . 7
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴)) |
| 17 | 16 | ord 865 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 → (𝐴 ∩ 𝐵) = 𝐴)) |
| 18 | | dfss2 3969 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) |
| 19 | 17, 18 | imbitrrdi 252 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 → 𝐴 ⊆ 𝐵)) |
| 20 | | ordin 6414 |
. . . . . . . . 9
⊢ ((Ord
𝐵 ∧ Ord 𝐴) → Ord (𝐵 ∩ 𝐴)) |
| 21 | | inss1 4237 |
. . . . . . . . . 10
⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵 |
| 22 | | ordsseleq 6413 |
. . . . . . . . . 10
⊢ ((Ord
(𝐵 ∩ 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ⊆ 𝐵 ↔ ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵))) |
| 23 | 21, 22 | mpbii 233 |
. . . . . . . . 9
⊢ ((Ord
(𝐵 ∩ 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵)) |
| 24 | 20, 23 | sylan 580 |
. . . . . . . 8
⊢ (((Ord
𝐵 ∧ Ord 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵)) |
| 25 | 24 | anabss4 667 |
. . . . . . 7
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵)) |
| 26 | 25 | ord 865 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ (𝐵 ∩ 𝐴) ∈ 𝐵 → (𝐵 ∩ 𝐴) = 𝐵)) |
| 27 | | dfss2 3969 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐵) |
| 28 | 26, 27 | imbitrrdi 252 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ (𝐵 ∩ 𝐴) ∈ 𝐵 → 𝐵 ⊆ 𝐴)) |
| 29 | 19, 28 | orim12d 967 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → ((¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))) |
| 30 | 11, 29 | mpd 15 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) |
| 31 | | sspsstri 4105 |
. . 3
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)) |
| 32 | 30, 31 | sylib 218 |
. 2
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)) |
| 33 | | ordelpss 6412 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵)) |
| 34 | | biidd 262 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ 𝐴 = 𝐵)) |
| 35 | | ordelpss 6412 |
. . . 4
⊢ ((Ord
𝐵 ∧ Ord 𝐴) → (𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴)) |
| 36 | 35 | ancoms 458 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴)) |
| 37 | 33, 34, 36 | 3orbi123d 1437 |
. 2
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))) |
| 38 | 32, 37 | mpbird 257 |
1
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |