Proof of Theorem nnm00
Step | Hyp | Ref
| Expression |
1 | | simpl 102 |
. . . . . . 7
⊢ ((𝐴 = ∅ ∧ 𝐵 = ∅) → 𝐴 = ∅) |
2 | | simpl 102 |
. . . . . . 7
⊢ ((𝐴 = ∅ ∧ ∅ ∈
𝐵) → 𝐴 = ∅) |
3 | 1, 2 | jaoi 636 |
. . . . . 6
⊢ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ ∅ ∈
𝐵)) → 𝐴 = ∅) |
4 | 3 | orcd 652 |
. . . . 5
⊢ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ ∅ ∈
𝐵)) → (𝐴 = ∅ ∨ 𝐵 = ∅)) |
5 | 4 | a1i 9 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) →
(((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ ∅ ∈
𝐵)) → (𝐴 = ∅ ∨ 𝐵 = ∅))) |
6 | | simpr 103 |
. . . . . . 7
⊢ ((∅
∈ 𝐴 ∧ 𝐵 = ∅) → 𝐵 = ∅) |
7 | 6 | olcd 653 |
. . . . . 6
⊢ ((∅
∈ 𝐴 ∧ 𝐵 = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅)) |
8 | 7 | a1i 9 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) →
((∅ ∈ 𝐴 ∧
𝐵 = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅))) |
9 | | simplr 482 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) ∧
(∅ ∈ 𝐴 ∧
∅ ∈ 𝐵)) →
(𝐴
·𝑜 𝐵) = ∅) |
10 | | nnmordi 6089 |
. . . . . . . . . . . . 13
⊢ (((𝐵 ∈ ω ∧ 𝐴 ∈ ω) ∧ ∅
∈ 𝐴) → (∅
∈ 𝐵 → (𝐴 ·𝑜
∅) ∈ (𝐴
·𝑜 𝐵))) |
11 | 10 | expimpd 345 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ ω ∧ 𝐴 ∈ ω) →
((∅ ∈ 𝐴 ∧
∅ ∈ 𝐵) →
(𝐴
·𝑜 ∅) ∈ (𝐴 ·𝑜 𝐵))) |
12 | 11 | ancoms 255 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
((∅ ∈ 𝐴 ∧
∅ ∈ 𝐵) →
(𝐴
·𝑜 ∅) ∈ (𝐴 ·𝑜 𝐵))) |
13 | | nnm0 6054 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ω → (𝐴 ·𝑜
∅) = ∅) |
14 | 13 | adantr 261 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·𝑜
∅) = ∅) |
15 | 14 | eleq1d 2106 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜
∅) ∈ (𝐴
·𝑜 𝐵) ↔ ∅ ∈ (𝐴 ·𝑜 𝐵))) |
16 | 12, 15 | sylibd 138 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
((∅ ∈ 𝐴 ∧
∅ ∈ 𝐵) →
∅ ∈ (𝐴
·𝑜 𝐵))) |
17 | 16 | adantr 261 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) →
((∅ ∈ 𝐴 ∧
∅ ∈ 𝐵) →
∅ ∈ (𝐴
·𝑜 𝐵))) |
18 | 17 | imp 115 |
. . . . . . . 8
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) ∧
(∅ ∈ 𝐴 ∧
∅ ∈ 𝐵)) →
∅ ∈ (𝐴
·𝑜 𝐵)) |
19 | | n0i 3229 |
. . . . . . . 8
⊢ (∅
∈ (𝐴
·𝑜 𝐵) → ¬ (𝐴 ·𝑜 𝐵) = ∅) |
20 | 18, 19 | syl 14 |
. . . . . . 7
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) ∧
(∅ ∈ 𝐴 ∧
∅ ∈ 𝐵)) →
¬ (𝐴
·𝑜 𝐵) = ∅) |
21 | 9, 20 | pm2.21dd 550 |
. . . . . 6
⊢ ((((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) ∧
(∅ ∈ 𝐴 ∧
∅ ∈ 𝐵)) →
(𝐴 = ∅ ∨ 𝐵 = ∅)) |
22 | 21 | ex 108 |
. . . . 5
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) →
((∅ ∈ 𝐴 ∧
∅ ∈ 𝐵) →
(𝐴 = ∅ ∨ 𝐵 = ∅))) |
23 | 8, 22 | jaod 637 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) →
(((∅ ∈ 𝐴 ∧
𝐵 = ∅) ∨ (∅
∈ 𝐴 ∧ ∅
∈ 𝐵)) → (𝐴 = ∅ ∨ 𝐵 = ∅))) |
24 | | 0elnn 4340 |
. . . . . . 7
⊢ (𝐴 ∈ ω → (𝐴 = ∅ ∨ ∅ ∈
𝐴)) |
25 | | 0elnn 4340 |
. . . . . . 7
⊢ (𝐵 ∈ ω → (𝐵 = ∅ ∨ ∅ ∈
𝐵)) |
26 | 24, 25 | anim12i 321 |
. . . . . 6
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 = ∅ ∨ ∅ ∈
𝐴) ∧ (𝐵 = ∅ ∨ ∅ ∈ 𝐵))) |
27 | | anddi 734 |
. . . . . 6
⊢ (((𝐴 = ∅ ∨ ∅ ∈
𝐴) ∧ (𝐵 = ∅ ∨ ∅ ∈ 𝐵)) ↔ (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ ∅ ∈ 𝐵)) ∨ ((∅ ∈ 𝐴 ∧ 𝐵 = ∅) ∨ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵)))) |
28 | 26, 27 | sylib 127 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ ∅ ∈
𝐵)) ∨ ((∅ ∈
𝐴 ∧ 𝐵 = ∅) ∨ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵)))) |
29 | 28 | adantr 261 |
. . . 4
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) →
(((𝐴 = ∅ ∧ 𝐵 = ∅) ∨ (𝐴 = ∅ ∧ ∅ ∈
𝐵)) ∨ ((∅ ∈
𝐴 ∧ 𝐵 = ∅) ∨ (∅ ∈ 𝐴 ∧ ∅ ∈ 𝐵)))) |
30 | 5, 23, 29 | mpjaod 638 |
. . 3
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω) ∧ (𝐴 ·𝑜
𝐵) = ∅) → (𝐴 = ∅ ∨ 𝐵 = ∅)) |
31 | 30 | ex 108 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜
𝐵) = ∅ → (𝐴 = ∅ ∨ 𝐵 = ∅))) |
32 | | oveq1 5519 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐴 ·𝑜
𝐵) = (∅
·𝑜 𝐵)) |
33 | | nnm0r 6058 |
. . . . . 6
⊢ (𝐵 ∈ ω → (∅
·𝑜 𝐵) = ∅) |
34 | 32, 33 | sylan9eqr 2094 |
. . . . 5
⊢ ((𝐵 ∈ ω ∧ 𝐴 = ∅) → (𝐴 ·𝑜
𝐵) =
∅) |
35 | 34 | ex 108 |
. . . 4
⊢ (𝐵 ∈ ω → (𝐴 = ∅ → (𝐴 ·𝑜
𝐵) =
∅)) |
36 | 35 | adantl 262 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 = ∅ → (𝐴 ·𝑜
𝐵) =
∅)) |
37 | | oveq2 5520 |
. . . . . 6
⊢ (𝐵 = ∅ → (𝐴 ·𝑜
𝐵) = (𝐴 ·𝑜
∅)) |
38 | 37, 13 | sylan9eqr 2094 |
. . . . 5
⊢ ((𝐴 ∈ ω ∧ 𝐵 = ∅) → (𝐴 ·𝑜
𝐵) =
∅) |
39 | 38 | ex 108 |
. . . 4
⊢ (𝐴 ∈ ω → (𝐵 = ∅ → (𝐴 ·𝑜
𝐵) =
∅)) |
40 | 39 | adantr 261 |
. . 3
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐵 = ∅ → (𝐴 ·𝑜
𝐵) =
∅)) |
41 | 36, 40 | jaod 637 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 = ∅ ∨ 𝐵 = ∅) → (𝐴 ·𝑜
𝐵) =
∅)) |
42 | 31, 41 | impbid 120 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·𝑜
𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))) |