Proof of Theorem oeord
Step | Hyp | Ref
| Expression |
1 | | oeordi 8401 |
. . 3
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐴
∈ 𝐵 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝐵))) |
2 | 1 | 3adant1 1129 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐴
∈ 𝐵 → (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝐵))) |
3 | | oveq2 7277 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐶 ↑o 𝐴) = (𝐶 ↑o 𝐵)) |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐴 =
𝐵 → (𝐶 ↑o 𝐴) = (𝐶 ↑o 𝐵))) |
5 | | oeordi 8401 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐵
∈ 𝐴 → (𝐶 ↑o 𝐵) ∈ (𝐶 ↑o 𝐴))) |
6 | 5 | 3adant2 1130 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐵
∈ 𝐴 → (𝐶 ↑o 𝐵) ∈ (𝐶 ↑o 𝐴))) |
7 | 4, 6 | orim12d 962 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → ((𝐴
= 𝐵 ∨ 𝐵 ∈ 𝐴) → ((𝐶 ↑o 𝐴) = (𝐶 ↑o 𝐵) ∨ (𝐶 ↑o 𝐵) ∈ (𝐶 ↑o 𝐴)))) |
8 | 7 | con3d 152 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (¬ ((𝐶 ↑o 𝐴) = (𝐶 ↑o 𝐵) ∨ (𝐶 ↑o 𝐵) ∈ (𝐶 ↑o 𝐴)) → ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
9 | | eldifi 4066 |
. . . . . 6
⊢ (𝐶 ∈ (On ∖
2o) → 𝐶
∈ On) |
10 | 9 | 3ad2ant3 1134 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → 𝐶
∈ On) |
11 | | simp1 1135 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → 𝐴
∈ On) |
12 | | oecl 8350 |
. . . . 5
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 ↑o 𝐴) ∈ On) |
13 | 10, 11, 12 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐶
↑o 𝐴)
∈ On) |
14 | | simp2 1136 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → 𝐵
∈ On) |
15 | | oecl 8350 |
. . . . 5
⊢ ((𝐶 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ↑o 𝐵) ∈ On) |
16 | 10, 14, 15 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐶
↑o 𝐵)
∈ On) |
17 | | eloni 6274 |
. . . . 5
⊢ ((𝐶 ↑o 𝐴) ∈ On → Ord (𝐶 ↑o 𝐴)) |
18 | | eloni 6274 |
. . . . 5
⊢ ((𝐶 ↑o 𝐵) ∈ On → Ord (𝐶 ↑o 𝐵)) |
19 | | ordtri2 6299 |
. . . . 5
⊢ ((Ord
(𝐶 ↑o 𝐴) ∧ Ord (𝐶 ↑o 𝐵)) → ((𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝐵) ↔ ¬ ((𝐶 ↑o 𝐴) = (𝐶 ↑o 𝐵) ∨ (𝐶 ↑o 𝐵) ∈ (𝐶 ↑o 𝐴)))) |
20 | 17, 18, 19 | syl2an 596 |
. . . 4
⊢ (((𝐶 ↑o 𝐴) ∈ On ∧ (𝐶 ↑o 𝐵) ∈ On) → ((𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝐵) ↔ ¬ ((𝐶 ↑o 𝐴) = (𝐶 ↑o 𝐵) ∨ (𝐶 ↑o 𝐵) ∈ (𝐶 ↑o 𝐴)))) |
21 | 13, 16, 20 | syl2anc 584 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → ((𝐶
↑o 𝐴)
∈ (𝐶
↑o 𝐵)
↔ ¬ ((𝐶
↑o 𝐴) =
(𝐶 ↑o 𝐵) ∨ (𝐶 ↑o 𝐵) ∈ (𝐶 ↑o 𝐴)))) |
22 | | eloni 6274 |
. . . . 5
⊢ (𝐴 ∈ On → Ord 𝐴) |
23 | | eloni 6274 |
. . . . 5
⊢ (𝐵 ∈ On → Ord 𝐵) |
24 | | ordtri2 6299 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
25 | 22, 23, 24 | syl2an 596 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
26 | 25 | 3adant3 1131 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐴
∈ 𝐵 ↔ ¬
(𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
27 | 8, 21, 26 | 3imtr4d 294 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → ((𝐶
↑o 𝐴)
∈ (𝐶
↑o 𝐵)
→ 𝐴 ∈ 𝐵)) |
28 | 2, 27 | impbid 211 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2o)) → (𝐴
∈ 𝐵 ↔ (𝐶 ↑o 𝐴) ∈ (𝐶 ↑o 𝐵))) |