Proof of Theorem nnmord
Step | Hyp | Ref
| Expression |
1 | | nnmordi 6025 |
. . . . . 6
⊢
(((B ∈ 𝜔 ∧
𝐶 ∈ 𝜔) ∧
∅ ∈ 𝐶) → (A ∈ B → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |
2 | 1 | ex 108 |
. . . . 5
⊢
((B ∈ 𝜔 ∧
𝐶 ∈ 𝜔) → (∅ ∈ 𝐶 → (A ∈ B → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B)))) |
3 | 2 | com23 72 |
. . . 4
⊢
((B ∈ 𝜔 ∧
𝐶 ∈ 𝜔) → (A ∈ B → (∅ ∈ 𝐶 → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B)))) |
4 | 3 | impd 242 |
. . 3
⊢
((B ∈ 𝜔 ∧
𝐶 ∈ 𝜔) → ((A ∈ B ∧ ∅ ∈ 𝐶) → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |
5 | 4 | 3adant1 921 |
. 2
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) → ((A ∈ B ∧ ∅ ∈ 𝐶) → (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |
6 | | ne0i 3224 |
. . . . . . . 8
⊢ ((𝐶 ·𝑜
A) ∈
(𝐶
·𝑜 B) →
(𝐶
·𝑜 B) ≠
∅) |
7 | | nnm0r 5997 |
. . . . . . . . . 10
⊢ (B ∈ 𝜔
→ (∅ ·𝑜 B) = ∅) |
8 | | oveq1 5462 |
. . . . . . . . . . 11
⊢ (𝐶 = ∅ → (𝐶 ·𝑜
B) = (∅ ·𝑜
B)) |
9 | 8 | eqeq1d 2045 |
. . . . . . . . . 10
⊢ (𝐶 = ∅ → ((𝐶 ·𝑜
B) = ∅ ↔ (∅
·𝑜 B) =
∅)) |
10 | 7, 9 | syl5ibrcom 146 |
. . . . . . . . 9
⊢ (B ∈ 𝜔
→ (𝐶 = ∅ →
(𝐶
·𝑜 B) =
∅)) |
11 | 10 | necon3d 2243 |
. . . . . . . 8
⊢ (B ∈ 𝜔
→ ((𝐶
·𝑜 B) ≠
∅ → 𝐶 ≠
∅)) |
12 | 6, 11 | syl5 28 |
. . . . . . 7
⊢ (B ∈ 𝜔
→ ((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 B) → 𝐶 ≠ ∅)) |
13 | 12 | adantr 261 |
. . . . . 6
⊢
((B ∈ 𝜔 ∧
𝐶 ∈ 𝜔) → ((𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B) → 𝐶 ≠ ∅)) |
14 | | nn0eln0 4284 |
. . . . . . 7
⊢ (𝐶 ∈ 𝜔 → (∅ ∈ 𝐶 ↔ 𝐶 ≠ ∅)) |
15 | 14 | adantl 262 |
. . . . . 6
⊢
((B ∈ 𝜔 ∧
𝐶 ∈ 𝜔) → (∅ ∈ 𝐶 ↔ 𝐶 ≠ ∅)) |
16 | 13, 15 | sylibrd 158 |
. . . . 5
⊢
((B ∈ 𝜔 ∧
𝐶 ∈ 𝜔) → ((𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B) → ∅ ∈ 𝐶)) |
17 | 16 | 3adant1 921 |
. . . 4
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) → ((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 B) → ∅ ∈ 𝐶)) |
18 | | oveq2 5463 |
. . . . . . . . . 10
⊢ (A = B →
(𝐶
·𝑜 A) = (𝐶 ·𝑜
B)) |
19 | 18 | a1i 9 |
. . . . . . . . 9
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (A = B →
(𝐶
·𝑜 A) = (𝐶 ·𝑜
B))) |
20 | | nnmordi 6025 |
. . . . . . . . . 10
⊢
(((A ∈ 𝜔 ∧
𝐶 ∈ 𝜔) ∧
∅ ∈ 𝐶) → (B ∈ A → (𝐶 ·𝑜 B) ∈ (𝐶 ·𝑜
A))) |
21 | 20 | 3adantl2 1060 |
. . . . . . . . 9
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (B ∈ A → (𝐶 ·𝑜 B) ∈ (𝐶 ·𝑜
A))) |
22 | 19, 21 | orim12d 699 |
. . . . . . . 8
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → ((A = B ∨ B ∈ A) →
((𝐶
·𝑜 A) = (𝐶 ·𝑜
B) ∨
(𝐶
·𝑜 B) ∈ (𝐶 ·𝑜 A)))) |
23 | 22 | con3d 560 |
. . . . . . 7
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (¬ ((𝐶 ·𝑜 A) = (𝐶 ·𝑜 B) ∨ (𝐶 ·𝑜
B) ∈
(𝐶
·𝑜 A)) →
¬ (A = B ∨ B ∈ A))) |
24 | | simpl3 908 |
. . . . . . . . 9
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → 𝐶 ∈
𝜔) |
25 | | simpl1 906 |
. . . . . . . . 9
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → A ∈
𝜔) |
26 | | nnmcl 5999 |
. . . . . . . . 9
⊢ ((𝐶 ∈ 𝜔 ∧
A ∈
𝜔) → (𝐶
·𝑜 A) ∈ 𝜔) |
27 | 24, 25, 26 | syl2anc 391 |
. . . . . . . 8
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (𝐶 ·𝑜 A) ∈
𝜔) |
28 | | simpl2 907 |
. . . . . . . . 9
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → B ∈
𝜔) |
29 | | nnmcl 5999 |
. . . . . . . . 9
⊢ ((𝐶 ∈ 𝜔 ∧
B ∈
𝜔) → (𝐶
·𝑜 B) ∈ 𝜔) |
30 | 24, 28, 29 | syl2anc 391 |
. . . . . . . 8
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (𝐶 ·𝑜 B) ∈
𝜔) |
31 | | nntri2 6012 |
. . . . . . . 8
⊢ (((𝐶 ·𝑜
A) ∈
𝜔 ∧ (𝐶 ·𝑜 B) ∈ 𝜔)
→ ((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 B) ↔ ¬ ((𝐶 ·𝑜 A) = (𝐶 ·𝑜 B) ∨ (𝐶 ·𝑜
B) ∈
(𝐶
·𝑜 A)))) |
32 | 27, 30, 31 | syl2anc 391 |
. . . . . . 7
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → ((𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B) ↔ ¬ ((𝐶 ·𝑜 A) = (𝐶 ·𝑜 B) ∨ (𝐶 ·𝑜
B) ∈
(𝐶
·𝑜 A)))) |
33 | | nntri2 6012 |
. . . . . . . 8
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → (A ∈ B ↔
¬ (A = B ∨ B ∈ A))) |
34 | 25, 28, 33 | syl2anc 391 |
. . . . . . 7
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → (A ∈ B ↔ ¬ (A = B ∨ B ∈ A))) |
35 | 23, 32, 34 | 3imtr4d 192 |
. . . . . 6
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) ∧ ∅ ∈ 𝐶) → ((𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B) → A ∈ B)) |
36 | 35 | ex 108 |
. . . . 5
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) → (∅ ∈ 𝐶 → ((𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B) → A ∈ B))) |
37 | 36 | com23 72 |
. . . 4
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) → ((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 B) → (∅ ∈ 𝐶 → A ∈ B))) |
38 | 17, 37 | mpdd 36 |
. . 3
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) → ((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 B) → A
∈ B)) |
39 | 38, 17 | jcad 291 |
. 2
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) → ((𝐶
·𝑜 A) ∈ (𝐶 ·𝑜 B) → (A
∈ B ∧ ∅ ∈ 𝐶))) |
40 | 5, 39 | impbid 120 |
1
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔 ∧ 𝐶 ∈
𝜔) → ((A ∈ B ∧ ∅ ∈ 𝐶) ↔ (𝐶 ·𝑜 A) ∈ (𝐶 ·𝑜
B))) |