Proof of Theorem ordelinelOLD
Step | Hyp | Ref
| Expression |
1 | | ordtri2or3 5824 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 = (𝐴 ∩ 𝐵) ∨ 𝐵 = (𝐴 ∩ 𝐵))) |
2 | 1 | 3adant3 1081 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → (𝐴 = (𝐴 ∩ 𝐵) ∨ 𝐵 = (𝐴 ∩ 𝐵))) |
3 | | eleq1 2689 |
. . . . 5
⊢ (𝐴 = (𝐴 ∩ 𝐵) → (𝐴 ∈ 𝐶 ↔ (𝐴 ∩ 𝐵) ∈ 𝐶)) |
4 | | orc 400 |
. . . . 5
⊢ (𝐴 ∈ 𝐶 → (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶)) |
5 | 3, 4 | syl6bir 244 |
. . . 4
⊢ (𝐴 = (𝐴 ∩ 𝐵) → ((𝐴 ∩ 𝐵) ∈ 𝐶 → (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶))) |
6 | | eleq1 2689 |
. . . . 5
⊢ (𝐵 = (𝐴 ∩ 𝐵) → (𝐵 ∈ 𝐶 ↔ (𝐴 ∩ 𝐵) ∈ 𝐶)) |
7 | | olc 399 |
. . . . 5
⊢ (𝐵 ∈ 𝐶 → (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶)) |
8 | 6, 7 | syl6bir 244 |
. . . 4
⊢ (𝐵 = (𝐴 ∩ 𝐵) → ((𝐴 ∩ 𝐵) ∈ 𝐶 → (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶))) |
9 | 5, 8 | jaoi 394 |
. . 3
⊢ ((𝐴 = (𝐴 ∩ 𝐵) ∨ 𝐵 = (𝐴 ∩ 𝐵)) → ((𝐴 ∩ 𝐵) ∈ 𝐶 → (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶))) |
10 | 2, 9 | syl 17 |
. 2
⊢ ((Ord
𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → ((𝐴 ∩ 𝐵) ∈ 𝐶 → (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶))) |
11 | | inss1 3833 |
. . . 4
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
12 | | ordin 5753 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵)) |
13 | | ordtr2 5768 |
. . . . 5
⊢ ((Ord
(𝐴 ∩ 𝐵) ∧ Ord 𝐶) → (((𝐴 ∩ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶)) |
14 | 12, 13 | stoic3 1701 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → (((𝐴 ∩ 𝐵) ⊆ 𝐴 ∧ 𝐴 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶)) |
15 | 11, 14 | mpani 712 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → (𝐴 ∈ 𝐶 → (𝐴 ∩ 𝐵) ∈ 𝐶)) |
16 | | inss2 3834 |
. . . 4
⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
17 | | ordtr2 5768 |
. . . . 5
⊢ ((Ord
(𝐴 ∩ 𝐵) ∧ Ord 𝐶) → (((𝐴 ∩ 𝐵) ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶)) |
18 | 12, 17 | stoic3 1701 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → (((𝐴 ∩ 𝐵) ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶)) |
19 | 16, 18 | mpani 712 |
. . 3
⊢ ((Ord
𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → (𝐵 ∈ 𝐶 → (𝐴 ∩ 𝐵) ∈ 𝐶)) |
20 | 15, 19 | jaod 395 |
. 2
⊢ ((Ord
𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → ((𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶) → (𝐴 ∩ 𝐵) ∈ 𝐶)) |
21 | 10, 20 | impbid 202 |
1
⊢ ((Ord
𝐴 ∧ Ord 𝐵 ∧ Ord 𝐶) → ((𝐴 ∩ 𝐵) ∈ 𝐶 ↔ (𝐴 ∈ 𝐶 ∨ 𝐵 ∈ 𝐶))) |