Proof of Theorem oaord
Step | Hyp | Ref
| Expression |
1 | | oaordi 8274 |
. . 3
⊢ ((𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) |
2 | 1 | 3adant1 1132 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) |
3 | | oveq2 7221 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐶 +o 𝐴) = (𝐶 +o 𝐵)) |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 = 𝐵 → (𝐶 +o 𝐴) = (𝐶 +o 𝐵))) |
5 | | oaordi 8274 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐴 → (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴))) |
6 | 5 | 3adant2 1133 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐵 ∈ 𝐴 → (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴))) |
7 | 4, 6 | orim12d 965 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) → ((𝐶 +o 𝐴) = (𝐶 +o 𝐵) ∨ (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴)))) |
8 | 7 | con3d 155 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (¬
((𝐶 +o 𝐴) = (𝐶 +o 𝐵) ∨ (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴)) → ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
9 | | df-3an 1091 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ↔ ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On)) |
10 | | ancom 464 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) ↔ (𝐶 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On))) |
11 | | anandi 676 |
. . . . . 6
⊢ ((𝐶 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ↔ ((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐵 ∈ On))) |
12 | 9, 10, 11 | 3bitri 300 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ↔ ((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐵 ∈ On))) |
13 | | oacl 8262 |
. . . . . . 7
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 +o 𝐴) ∈ On) |
14 | | eloni 6223 |
. . . . . . 7
⊢ ((𝐶 +o 𝐴) ∈ On → Ord (𝐶 +o 𝐴)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → Ord (𝐶 +o 𝐴)) |
16 | | oacl 8262 |
. . . . . . 7
⊢ ((𝐶 ∈ On ∧ 𝐵 ∈ On) → (𝐶 +o 𝐵) ∈ On) |
17 | | eloni 6223 |
. . . . . . 7
⊢ ((𝐶 +o 𝐵) ∈ On → Ord (𝐶 +o 𝐵)) |
18 | 16, 17 | syl 17 |
. . . . . 6
⊢ ((𝐶 ∈ On ∧ 𝐵 ∈ On) → Ord (𝐶 +o 𝐵)) |
19 | 15, 18 | anim12i 616 |
. . . . 5
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐵 ∈ On)) → (Ord (𝐶 +o 𝐴) ∧ Ord (𝐶 +o 𝐵))) |
20 | 12, 19 | sylbi 220 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (Ord (𝐶 +o 𝐴) ∧ Ord (𝐶 +o 𝐵))) |
21 | | ordtri2 6248 |
. . . 4
⊢ ((Ord
(𝐶 +o 𝐴) ∧ Ord (𝐶 +o 𝐵)) → ((𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵) ↔ ¬ ((𝐶 +o 𝐴) = (𝐶 +o 𝐵) ∨ (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴)))) |
22 | 20, 21 | syl 17 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵) ↔ ¬ ((𝐶 +o 𝐴) = (𝐶 +o 𝐵) ∨ (𝐶 +o 𝐵) ∈ (𝐶 +o 𝐴)))) |
23 | | eloni 6223 |
. . . . . 6
⊢ (𝐴 ∈ On → Ord 𝐴) |
24 | | eloni 6223 |
. . . . . 6
⊢ (𝐵 ∈ On → Ord 𝐵) |
25 | 23, 24 | anim12i 616 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Ord 𝐴 ∧ Ord 𝐵)) |
26 | 25 | 3adant3 1134 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (Ord 𝐴 ∧ Ord 𝐵)) |
27 | | ordtri2 6248 |
. . . 4
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
28 | 26, 27 | syl 17 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
29 | 8, 22, 28 | 3imtr4d 297 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵) → 𝐴 ∈ 𝐵)) |
30 | 2, 29 | impbid 215 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) |