Proof of Theorem nnmord
Step | Hyp | Ref
| Expression |
1 | | nnmordi 6466 |
. . . . . 6
⊢ (((𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) |
2 | 1 | ex 114 |
. . . . 5
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (∅
∈ 𝐶 → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))) |
3 | 2 | com23 78 |
. . . 4
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 → (∅ ∈ 𝐶 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵)))) |
4 | 3 | impd 252 |
. . 3
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶) → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) |
5 | 4 | 3adant1 1000 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶) → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) |
6 | | ne0i 3401 |
. . . . . . . 8
⊢ ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) → (𝐶 ·o 𝐵) ≠ ∅) |
7 | | nnm0r 6429 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ω → (∅
·o 𝐵) =
∅) |
8 | | oveq1 5834 |
. . . . . . . . . . 11
⊢ (𝐶 = ∅ → (𝐶 ·o 𝐵) = (∅
·o 𝐵)) |
9 | 8 | eqeq1d 2166 |
. . . . . . . . . 10
⊢ (𝐶 = ∅ → ((𝐶 ·o 𝐵) = ∅ ↔ (∅
·o 𝐵) =
∅)) |
10 | 7, 9 | syl5ibrcom 156 |
. . . . . . . . 9
⊢ (𝐵 ∈ ω → (𝐶 = ∅ → (𝐶 ·o 𝐵) = ∅)) |
11 | 10 | necon3d 2371 |
. . . . . . . 8
⊢ (𝐵 ∈ ω → ((𝐶 ·o 𝐵) ≠ ∅ → 𝐶 ≠ ∅)) |
12 | 6, 11 | syl5 32 |
. . . . . . 7
⊢ (𝐵 ∈ ω → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) → 𝐶 ≠ ∅)) |
13 | 12 | adantr 274 |
. . . . . 6
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) → 𝐶 ≠ ∅)) |
14 | | nn0eln0 4582 |
. . . . . . 7
⊢ (𝐶 ∈ ω → (∅
∈ 𝐶 ↔ 𝐶 ≠ ∅)) |
15 | 14 | adantl 275 |
. . . . . 6
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (∅
∈ 𝐶 ↔ 𝐶 ≠ ∅)) |
16 | 13, 15 | sylibrd 168 |
. . . . 5
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) → ∅ ∈ 𝐶)) |
17 | 16 | 3adant1 1000 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) → ∅ ∈ 𝐶)) |
18 | | oveq2 5835 |
. . . . . . . . . 10
⊢ (𝐴 = 𝐵 → (𝐶 ·o 𝐴) = (𝐶 ·o 𝐵)) |
19 | 18 | a1i 9 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 = 𝐵 → (𝐶 ·o 𝐴) = (𝐶 ·o 𝐵))) |
20 | | nnmordi 6466 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐵 ∈ 𝐴 → (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴))) |
21 | 20 | 3adantl2 1139 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐵 ∈ 𝐴 → (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴))) |
22 | 19, 21 | orim12d 776 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → ((𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴) → ((𝐶 ·o 𝐴) = (𝐶 ·o 𝐵) ∨ (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴)))) |
23 | 22 | con3d 621 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (¬
((𝐶 ·o
𝐴) = (𝐶 ·o 𝐵) ∨ (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴)) → ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
24 | | simpl3 987 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐶 ∈
ω) |
25 | | simpl1 985 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐴 ∈
ω) |
26 | | nnmcl 6431 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ω ∧ 𝐴 ∈ ω) → (𝐶 ·o 𝐴) ∈
ω) |
27 | 24, 25, 26 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐶 ·o 𝐴) ∈
ω) |
28 | | simpl2 986 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → 𝐵 ∈
ω) |
29 | | nnmcl 6431 |
. . . . . . . . 9
⊢ ((𝐶 ∈ ω ∧ 𝐵 ∈ ω) → (𝐶 ·o 𝐵) ∈
ω) |
30 | 24, 28, 29 | syl2anc 409 |
. . . . . . . 8
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐶 ·o 𝐵) ∈
ω) |
31 | | nntri2 6444 |
. . . . . . . 8
⊢ (((𝐶 ·o 𝐴) ∈ ω ∧ (𝐶 ·o 𝐵) ∈ ω) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) ↔ ¬ ((𝐶 ·o 𝐴) = (𝐶 ·o 𝐵) ∨ (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴)))) |
32 | 27, 30, 31 | syl2anc 409 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) ↔ ¬ ((𝐶 ·o 𝐴) = (𝐶 ·o 𝐵) ∨ (𝐶 ·o 𝐵) ∈ (𝐶 ·o 𝐴)))) |
33 | | nntri2 6444 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
34 | 25, 28, 33 | syl2anc 409 |
. . . . . . 7
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
35 | 23, 32, 34 | 3imtr4d 202 |
. . . . . 6
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅
∈ 𝐶) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) → 𝐴 ∈ 𝐵)) |
36 | 35 | ex 114 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (∅
∈ 𝐶 → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) → 𝐴 ∈ 𝐵))) |
37 | 36 | com23 78 |
. . . 4
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) → (∅ ∈ 𝐶 → 𝐴 ∈ 𝐵))) |
38 | 17, 37 | mpdd 41 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) → 𝐴 ∈ 𝐵)) |
39 | 38, 17 | jcad 305 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵) → (𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶))) |
40 | 5, 39 | impbid 128 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) |