Proof of Theorem oecan
Step | Hyp | Ref
| Expression |
1 | | oeordi 7667 |
. . . . . . 7
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ (On ∖
2𝑜)) → (𝐵 ∈ 𝐶 → (𝐴 ↑𝑜 𝐵) ∈ (𝐴 ↑𝑜 𝐶))) |
2 | 1 | ancoms 469 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 → (𝐴 ↑𝑜 𝐵) ∈ (𝐴 ↑𝑜 𝐶))) |
3 | 2 | 3adant2 1080 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐶 → (𝐴 ↑𝑜 𝐵) ∈ (𝐴 ↑𝑜 𝐶))) |
4 | | oeordi 7667 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ (On ∖
2𝑜)) → (𝐶 ∈ 𝐵 → (𝐴 ↑𝑜 𝐶) ∈ (𝐴 ↑𝑜 𝐵))) |
5 | 4 | ancoms 469 |
. . . . . 6
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On) → (𝐶 ∈ 𝐵 → (𝐴 ↑𝑜 𝐶) ∈ (𝐴 ↑𝑜 𝐵))) |
6 | 5 | 3adant3 1081 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐶 ∈ 𝐵 → (𝐴 ↑𝑜 𝐶) ∈ (𝐴 ↑𝑜 𝐵))) |
7 | 3, 6 | orim12d 883 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵) → ((𝐴 ↑𝑜 𝐵) ∈ (𝐴 ↑𝑜 𝐶) ∨ (𝐴 ↑𝑜 𝐶) ∈ (𝐴 ↑𝑜 𝐵)))) |
8 | 7 | con3d 148 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (¬ ((𝐴 ↑𝑜
𝐵) ∈ (𝐴 ↑𝑜
𝐶) ∨ (𝐴 ↑𝑜 𝐶) ∈ (𝐴 ↑𝑜 𝐵)) → ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) |
9 | | eldifi 3732 |
. . . . . 6
⊢ (𝐴 ∈ (On ∖
2𝑜) → 𝐴 ∈ On) |
10 | 9 | 3ad2ant1 1082 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐴 ∈ On) |
11 | | simp2 1062 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐵 ∈ On) |
12 | | oecl 7617 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑𝑜
𝐵) ∈
On) |
13 | 10, 11, 12 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑𝑜 𝐵) ∈ On) |
14 | | simp3 1063 |
. . . . 5
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → 𝐶 ∈ On) |
15 | | oecl 7617 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑𝑜
𝐶) ∈
On) |
16 | 10, 14, 15 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ↑𝑜 𝐶) ∈ On) |
17 | | eloni 5733 |
. . . . 5
⊢ ((𝐴 ↑𝑜
𝐵) ∈ On → Ord
(𝐴
↑𝑜 𝐵)) |
18 | | eloni 5733 |
. . . . 5
⊢ ((𝐴 ↑𝑜
𝐶) ∈ On → Ord
(𝐴
↑𝑜 𝐶)) |
19 | | ordtri3 5759 |
. . . . 5
⊢ ((Ord
(𝐴
↑𝑜 𝐵) ∧ Ord (𝐴 ↑𝑜 𝐶)) → ((𝐴 ↑𝑜 𝐵) = (𝐴 ↑𝑜 𝐶) ↔ ¬ ((𝐴 ↑𝑜
𝐵) ∈ (𝐴 ↑𝑜
𝐶) ∨ (𝐴 ↑𝑜 𝐶) ∈ (𝐴 ↑𝑜 𝐵)))) |
20 | 17, 18, 19 | syl2an 494 |
. . . 4
⊢ (((𝐴 ↑𝑜
𝐵) ∈ On ∧ (𝐴 ↑𝑜
𝐶) ∈ On) →
((𝐴
↑𝑜 𝐵) = (𝐴 ↑𝑜 𝐶) ↔ ¬ ((𝐴 ↑𝑜
𝐵) ∈ (𝐴 ↑𝑜
𝐶) ∨ (𝐴 ↑𝑜 𝐶) ∈ (𝐴 ↑𝑜 𝐵)))) |
21 | 13, 16, 20 | syl2anc 693 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑𝑜 𝐵) = (𝐴 ↑𝑜 𝐶) ↔ ¬ ((𝐴 ↑𝑜
𝐵) ∈ (𝐴 ↑𝑜
𝐶) ∨ (𝐴 ↑𝑜 𝐶) ∈ (𝐴 ↑𝑜 𝐵)))) |
22 | | eloni 5733 |
. . . . 5
⊢ (𝐵 ∈ On → Ord 𝐵) |
23 | | eloni 5733 |
. . . . 5
⊢ (𝐶 ∈ On → Ord 𝐶) |
24 | | ordtri3 5759 |
. . . . 5
⊢ ((Ord
𝐵 ∧ Ord 𝐶) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) |
25 | 22, 23, 24 | syl2an 494 |
. . . 4
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) |
26 | 25 | 3adant1 1079 |
. . 3
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 = 𝐶 ↔ ¬ (𝐵 ∈ 𝐶 ∨ 𝐶 ∈ 𝐵))) |
27 | 8, 21, 26 | 3imtr4d 283 |
. 2
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑𝑜 𝐵) = (𝐴 ↑𝑜 𝐶) → 𝐵 = 𝐶)) |
28 | | oveq2 6658 |
. 2
⊢ (𝐵 = 𝐶 → (𝐴 ↑𝑜 𝐵) = (𝐴 ↑𝑜 𝐶)) |
29 | 27, 28 | impbid1 215 |
1
⊢ ((𝐴 ∈ (On ∖
2𝑜) ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 ↑𝑜 𝐵) = (𝐴 ↑𝑜 𝐶) ↔ 𝐵 = 𝐶)) |