Proof of Theorem nnmord
Step | Hyp | Ref
| Expression |
1 | | nnmordi 7711 |
. . . . . 6
⊢ (((𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵))) |
2 | 1 | ex 450 |
. . . . 5
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (∅
∈ 𝐶 → (𝐴 ∈ 𝐵 → (𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵)))) |
3 | 2 | com23 86 |
. . . 4
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 → (∅ ∈ 𝐶 → (𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵)))) |
4 | 3 | impd 447 |
. . 3
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶) → (𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵))) |
5 | 4 | 3adant1 1079 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶) → (𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵))) |
6 | | ne0i 3921 |
. . . . . . . 8
⊢ ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → (𝐶 ·𝑜
𝐵) ≠
∅) |
7 | | nnm0r 7690 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ω → (∅
·𝑜 𝐵) = ∅) |
8 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝐶 = ∅ → (𝐶 ·𝑜
𝐵) = (∅
·𝑜 𝐵)) |
9 | 8 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝐶 = ∅ → ((𝐶 ·𝑜
𝐵) = ∅ ↔
(∅ ·𝑜 𝐵) = ∅)) |
10 | 7, 9 | syl5ibrcom 237 |
. . . . . . . . 9
⊢ (𝐵 ∈ ω → (𝐶 = ∅ → (𝐶 ·𝑜
𝐵) =
∅)) |
11 | 10 | necon3d 2815 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → ((𝐶 ·𝑜
𝐵) ≠ ∅ →
𝐶 ≠
∅)) |
12 | 6, 11 | syl5 34 |
. . . . . . 7
⊢ (𝐵 ∈ ω → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → 𝐶 ≠ ∅)) |
13 | 12 | adantr 481 |
. . . . . 6
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → 𝐶 ≠ ∅)) |
14 | | nnord 7073 |
. . . . . . . 8
⊢ (𝐶 ∈ ω → Ord 𝐶) |
15 | | ord0eln0 5779 |
. . . . . . . 8
⊢ (Ord
𝐶 → (∅ ∈
𝐶 ↔ 𝐶 ≠ ∅)) |
16 | 14, 15 | syl 17 |
. . . . . . 7
⊢ (𝐶 ∈ ω → (∅
∈ 𝐶 ↔ 𝐶 ≠ ∅)) |
17 | 16 | adantl 482 |
. . . . . 6
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (∅
∈ 𝐶 ↔ 𝐶 ≠ ∅)) |
18 | 13, 17 | sylibrd 249 |
. . . . 5
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → ∅ ∈
𝐶)) |
19 | 18 | 3adant1 1079 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → ∅ ∈
𝐶)) |
20 | | oveq2 6658 |
. . . . . . . . . 10
⊢ (𝐴 = 𝐵 → (𝐶 ·𝑜 𝐴) = (𝐶 ·𝑜 𝐵)) |
21 | 20 | a1i 11 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 = 𝐵 → (𝐶 ·𝑜 𝐴) = (𝐶 ·𝑜 𝐵))) |
22 | | nnmordi 7711 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐵 ∈ 𝐴 → (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴))) |
23 | 22 | 3adantl2 1218 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐵 ∈ 𝐴 → (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴))) |
24 | 21, 23 | orim12d 883 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → ((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) → ((𝐶 ·𝑜 𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
25 | 24 | con3d 148 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (¬
((𝐶
·𝑜 𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)) → ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
26 | | simpl3 1066 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐶 ∈
ω) |
27 | | simpl1 1064 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐴 ∈
ω) |
28 | | nnmcl 7692 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) → (𝐶 ·𝑜
𝐴) ∈
ω) |
29 | 26, 27, 28 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐶 ·𝑜
𝐴) ∈
ω) |
30 | | simpl2 1065 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐵 ∈
ω) |
31 | | nnmcl 7692 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ω ∧ 𝐵 ∈ ω) → (𝐶 ·𝑜
𝐵) ∈
ω) |
32 | 26, 30, 31 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐶 ·𝑜
𝐵) ∈
ω) |
33 | | nnord 7073 |
. . . . . . . . 9
⊢ ((𝐶 ·𝑜
𝐴) ∈ ω →
Ord (𝐶
·𝑜 𝐴)) |
34 | | nnord 7073 |
. . . . . . . . 9
⊢ ((𝐶 ·𝑜
𝐵) ∈ ω →
Ord (𝐶
·𝑜 𝐵)) |
35 | | ordtri2 5758 |
. . . . . . . . 9
⊢ ((Ord
(𝐶
·𝑜 𝐴) ∧ Ord (𝐶 ·𝑜 𝐵)) → ((𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵) ↔ ¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
36 | 33, 34, 35 | syl2an 494 |
. . . . . . . 8
⊢ (((𝐶 ·𝑜
𝐴) ∈ ω ∧
(𝐶
·𝑜 𝐵) ∈ ω) → ((𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵) ↔ ¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
37 | 29, 32, 36 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) ↔ ¬ ((𝐶 ·𝑜
𝐴) = (𝐶 ·𝑜 𝐵) ∨ (𝐶 ·𝑜 𝐵) ∈ (𝐶 ·𝑜 𝐴)))) |
38 | | nnord 7073 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → Ord 𝐴) |
39 | | nnord 7073 |
. . . . . . . . 9
⊢ (𝐵 ∈ ω → Ord 𝐵) |
40 | | ordtri2 5758 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ Ord 𝐵) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
41 | 38, 39, 40 | syl2an 494 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
42 | 27, 30, 41 | syl2anc 693 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
43 | 25, 37, 42 | 3imtr4d 283 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → 𝐴 ∈ 𝐵)) |
44 | 43 | ex 450 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (∅
∈ 𝐶 → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → 𝐴 ∈ 𝐵))) |
45 | 44 | com23 86 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → (∅ ∈
𝐶 → 𝐴 ∈ 𝐵))) |
46 | 19, 45 | mpdd 43 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → 𝐴 ∈ 𝐵)) |
47 | 46, 19 | jcad 555 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·𝑜
𝐴) ∈ (𝐶 ·𝑜
𝐵) → (𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶))) |
48 | 5, 47 | impbid 202 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶) ↔ (𝐶 ·𝑜 𝐴) ∈ (𝐶 ·𝑜 𝐵))) |