Proof of Theorem oeord
Step | Hyp | Ref
| Expression |
1 | | oeordi 7667 |
. . 3
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐴 ∈ 𝐵 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵))) |
2 | 1 | 3adant1 1079 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐴 ∈ 𝐵 → (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵))) |
3 | | oveq2 6658 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐶 ↑𝑜 𝐴) = (𝐶 ↑𝑜 𝐵)) |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐴 = 𝐵 → (𝐶 ↑𝑜 𝐴) = (𝐶 ↑𝑜 𝐵))) |
5 | | oeordi 7667 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐵 ∈ 𝐴 → (𝐶 ↑𝑜 𝐵) ∈ (𝐶 ↑𝑜 𝐴))) |
6 | 5 | 3adant2 1080 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐵 ∈ 𝐴 → (𝐶 ↑𝑜 𝐵) ∈ (𝐶 ↑𝑜 𝐴))) |
7 | 4, 6 | orim12d 883 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → ((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) → ((𝐶 ↑𝑜 𝐴) = (𝐶 ↑𝑜 𝐵) ∨ (𝐶 ↑𝑜 𝐵) ∈ (𝐶 ↑𝑜 𝐴)))) |
8 | 7 | con3d 148 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (¬ ((𝐶 ↑𝑜 𝐴) = (𝐶 ↑𝑜 𝐵) ∨ (𝐶 ↑𝑜 𝐵) ∈ (𝐶 ↑𝑜 𝐴)) → ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
9 | | eldifi 3732 |
. . . . . 6
⊢ (𝐶 ∈ (On ∖
2𝑜) → 𝐶 ∈ On) |
10 | 9 | 3ad2ant3 1084 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → 𝐶 ∈ On) |
11 | | simp1 1061 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → 𝐴 ∈ On) |
12 | | oecl 7617 |
. . . . 5
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 ↑𝑜
𝐴) ∈
On) |
13 | 10, 11, 12 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐶 ↑𝑜 𝐴) ∈ On) |
14 | | simp2 1062 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → 𝐵 ∈ On) |
15 | | oecl 7617 |
. . . . 5
⊢ ((𝐶 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ↑𝑜
𝐵) ∈
On) |
16 | 10, 14, 15 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐶 ↑𝑜 𝐵) ∈ On) |
17 | | eloni 5733 |
. . . . 5
⊢ ((𝐶 ↑𝑜
𝐴) ∈ On → Ord
(𝐶
↑𝑜 𝐴)) |
18 | | eloni 5733 |
. . . . 5
⊢ ((𝐶 ↑𝑜
𝐵) ∈ On → Ord
(𝐶
↑𝑜 𝐵)) |
19 | | ordtri2 5758 |
. . . . 5
⊢ ((Ord
(𝐶
↑𝑜 𝐴) ∧ Ord (𝐶 ↑𝑜 𝐵)) → ((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵) ↔ ¬ ((𝐶 ↑𝑜
𝐴) = (𝐶 ↑𝑜 𝐵) ∨ (𝐶 ↑𝑜 𝐵) ∈ (𝐶 ↑𝑜 𝐴)))) |
20 | 17, 18, 19 | syl2an 494 |
. . . 4
⊢ (((𝐶 ↑𝑜
𝐴) ∈ On ∧ (𝐶 ↑𝑜
𝐵) ∈ On) →
((𝐶
↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵) ↔ ¬ ((𝐶 ↑𝑜
𝐴) = (𝐶 ↑𝑜 𝐵) ∨ (𝐶 ↑𝑜 𝐵) ∈ (𝐶 ↑𝑜 𝐴)))) |
21 | 13, 16, 20 | syl2anc 693 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → ((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵) ↔ ¬ ((𝐶 ↑𝑜
𝐴) = (𝐶 ↑𝑜 𝐵) ∨ (𝐶 ↑𝑜 𝐵) ∈ (𝐶 ↑𝑜 𝐴)))) |
22 | | eloni 5733 |
. . . . 5
⊢ (𝐴 ∈ On → Ord 𝐴) |
23 | | eloni 5733 |
. . . . 5
⊢ (𝐵 ∈ On → Ord 𝐵) |
24 | | ordtri2 5758 |
. . . . 5
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
25 | 22, 23, 24 | syl2an 494 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
26 | 25 | 3adant3 1081 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
27 | 8, 21, 26 | 3imtr4d 283 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → ((𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵) → 𝐴 ∈ 𝐵)) |
28 | 2, 27 | impbid 202 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ (On ∖
2𝑜)) → (𝐴 ∈ 𝐵 ↔ (𝐶 ↑𝑜 𝐴) ∈ (𝐶 ↑𝑜 𝐵))) |