Proof of Theorem ordtri3or
Step | Hyp | Ref
| Expression |
1 | | ordin 6289 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵)) |
2 | | ordirr 6277 |
. . . . . 6
⊢ (Ord
(𝐴 ∩ 𝐵) → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵)) |
3 | 1, 2 | syl 17 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → ¬ (𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵)) |
4 | | ianor 979 |
. . . . . 6
⊢ (¬
((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵) ↔ (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵)) |
5 | | elin 3902 |
. . . . . . 7
⊢ ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵)) |
6 | | incom 4134 |
. . . . . . . . 9
⊢ (𝐴 ∩ 𝐵) = (𝐵 ∩ 𝐴) |
7 | 6 | eleq1i 2829 |
. . . . . . . 8
⊢ ((𝐴 ∩ 𝐵) ∈ 𝐵 ↔ (𝐵 ∩ 𝐴) ∈ 𝐵) |
8 | 7 | anbi2i 623 |
. . . . . . 7
⊢ (((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐴 ∩ 𝐵) ∈ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵)) |
9 | 5, 8 | bitri 274 |
. . . . . 6
⊢ ((𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∧ (𝐵 ∩ 𝐴) ∈ 𝐵)) |
10 | 4, 9 | xchnxbir 333 |
. . . . 5
⊢ (¬
(𝐴 ∩ 𝐵) ∈ (𝐴 ∩ 𝐵) ↔ (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵)) |
11 | 3, 10 | sylib 217 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵)) |
12 | | inss1 4162 |
. . . . . . . . . 10
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
13 | | ordsseleq 6288 |
. . . . . . . . . 10
⊢ ((Ord
(𝐴 ∩ 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ⊆ 𝐴 ↔ ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴))) |
14 | 12, 13 | mpbii 232 |
. . . . . . . . 9
⊢ ((Ord
(𝐴 ∩ 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴)) |
15 | 1, 14 | sylan 580 |
. . . . . . . 8
⊢ (((Ord
𝐴 ∧ Ord 𝐵) ∧ Ord 𝐴) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴)) |
16 | 15 | anabss1 663 |
. . . . . . 7
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → ((𝐴 ∩ 𝐵) ∈ 𝐴 ∨ (𝐴 ∩ 𝐵) = 𝐴)) |
17 | 16 | ord 861 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 → (𝐴 ∩ 𝐵) = 𝐴)) |
18 | | df-ss 3903 |
. . . . . 6
⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∩ 𝐵) = 𝐴) |
19 | 17, 18 | syl6ibr 251 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ (𝐴 ∩ 𝐵) ∈ 𝐴 → 𝐴 ⊆ 𝐵)) |
20 | | ordin 6289 |
. . . . . . . . 9
⊢ ((Ord
𝐵 ∧ Ord 𝐴) → Ord (𝐵 ∩ 𝐴)) |
21 | | inss1 4162 |
. . . . . . . . . 10
⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵 |
22 | | ordsseleq 6288 |
. . . . . . . . . 10
⊢ ((Ord
(𝐵 ∩ 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ⊆ 𝐵 ↔ ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵))) |
23 | 21, 22 | mpbii 232 |
. . . . . . . . 9
⊢ ((Ord
(𝐵 ∩ 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵)) |
24 | 20, 23 | sylan 580 |
. . . . . . . 8
⊢ (((Ord
𝐵 ∧ Ord 𝐴) ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵)) |
25 | 24 | anabss4 664 |
. . . . . . 7
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → ((𝐵 ∩ 𝐴) ∈ 𝐵 ∨ (𝐵 ∩ 𝐴) = 𝐵)) |
26 | 25 | ord 861 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ (𝐵 ∩ 𝐴) ∈ 𝐵 → (𝐵 ∩ 𝐴) = 𝐵)) |
27 | | df-ss 3903 |
. . . . . 6
⊢ (𝐵 ⊆ 𝐴 ↔ (𝐵 ∩ 𝐴) = 𝐵) |
28 | 26, 27 | syl6ibr 251 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (¬ (𝐵 ∩ 𝐴) ∈ 𝐵 → 𝐵 ⊆ 𝐴)) |
29 | 19, 28 | orim12d 962 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → ((¬ (𝐴 ∩ 𝐵) ∈ 𝐴 ∨ ¬ (𝐵 ∩ 𝐴) ∈ 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴))) |
30 | 11, 29 | mpd 15 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) |
31 | | sspsstri 4036 |
. . 3
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)) |
32 | 30, 31 | sylib 217 |
. 2
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴)) |
33 | | ordelpss 6287 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ 𝐴 ⊊ 𝐵)) |
34 | | biidd 261 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 = 𝐵 ↔ 𝐴 = 𝐵)) |
35 | | ordelpss 6287 |
. . . 4
⊢ ((Ord
𝐵 ∧ Ord 𝐴) → (𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴)) |
36 | 35 | ancoms 459 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐵 ∈ 𝐴 ↔ 𝐵 ⊊ 𝐴)) |
37 | 33, 34, 36 | 3orbi123d 1434 |
. 2
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → ((𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) ↔ (𝐴 ⊊ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ⊊ 𝐴))) |
38 | 32, 37 | mpbird 256 |
1
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |