Proof of Theorem omord2
Step | Hyp | Ref
| Expression |
1 | | omordi 7533 |
. . 3
⊢ (((𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵))) |
2 | 1 | 3adantl1 1210 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵))) |
3 | | oveq2 6557 |
. . . . . 6
⊢ (𝐴 = 𝐵 → (𝐶 ·𝑜 𝐴) = (𝐶 ·𝑜 𝐵)) |
4 | 3 | a1i 11 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 = 𝐵 → (𝐶 ·𝑜 𝐴) = (𝐶 ·𝑜 𝐵))) |
5 | | omordi 7533 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐵 ∈ 𝐴 → (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴))) |
6 | 5 | 3adantl2 1211 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐵 ∈ 𝐴 → (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴))) |
7 | 4, 6 | orim12d 879 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → ((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) → ((𝐶 ·𝑜 𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
8 | 7 | con3d 147 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)) → ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
9 | | omcl 7503 |
. . . . . . . 8
⊢ ((𝐶 ∈ On ∧ 𝐴 ∈ On) → (𝐶 ·𝑜
𝐴) ∈
On) |
10 | | omcl 7503 |
. . . . . . . 8
⊢ ((𝐶 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ·𝑜
𝐵) ∈
On) |
11 | | eloni 5650 |
. . . . . . . . 9
⊢ ((𝐶 ·𝑜
𝐴) ∈ On → Ord
(𝐶
·𝑜 𝐴)) |
12 | | eloni 5650 |
. . . . . . . . 9
⊢ ((𝐶 ·𝑜
𝐵) ∈ On → Ord
(𝐶
·𝑜 𝐵)) |
13 | | ordtri2 5675 |
. . . . . . . . 9
⊢ ((Ord
(𝐶
·𝑜 𝐴) ∧ Ord (𝐶 ·𝑜 𝐵)) → ((𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵) ↔ ¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
14 | 11, 12, 13 | syl2an 493 |
. . . . . . . 8
⊢ (((𝐶 ·𝑜
𝐴) ∈ On ∧ (𝐶 ·𝑜
𝐵) ∈ On) →
((𝐶
·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵) ↔ ¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
15 | 9, 10, 14 | syl2an 493 |
. . . . . . 7
⊢ (((𝐶 ∈ On ∧ 𝐴 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐵 ∈ On)) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) ↔ ¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
16 | 15 | anandis 869 |
. . . . . 6
⊢ ((𝐶 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) ↔ ¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
17 | 16 | ancoms 468 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝐶 ∈ On) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) ↔ ¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
18 | 17 | 3impa 1251 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) ↔ ¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
19 | 18 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) ↔ ¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
20 | | eloni 5650 |
. . . . . 6
⊢ (𝐴 ∈ On → Ord 𝐴) |
21 | | eloni 5650 |
. . . . . 6
⊢ (𝐵 ∈ On → Ord 𝐵) |
22 | | ordtri2 5675 |
. . . . . 6
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
23 | 20, 21, 22 | syl2an 493 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
24 | 23 | 3adant3 1074 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
25 | 24 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
26 | 8, 19, 25 | 3imtr4d 282 |
. 2
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → 𝐴 ∈ 𝐵)) |
27 | 2, 26 | impbid 201 |
1
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) ∧ ∅ ∈
𝐶) → (𝐴 ∈ 𝐵 ↔ (𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵))) |