Proof of Theorem nnm00
Step | Hyp | Ref
| Expression |
1 | | simpl 102 |
. . . . . . 7
⊢
((A = ∅ ∧ B = ∅)
→ A = ∅) |
2 | | simpl 102 |
. . . . . . 7
⊢
((A = ∅ ∧ ∅ ∈
B) → A = ∅) |
3 | 1, 2 | jaoi 635 |
. . . . . 6
⊢
(((A = ∅ ∧ B = ∅)
∨ (A =
∅ ∧ ∅ ∈ B)) →
A = ∅) |
4 | 3 | orcd 651 |
. . . . 5
⊢
(((A = ∅ ∧ B = ∅)
∨ (A =
∅ ∧ ∅ ∈ B)) →
(A = ∅
∨ B = ∅)) |
5 | 4 | a1i 9 |
. . . 4
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) → (((A = ∅ ∧
B = ∅)
∨ (A = ∅ ∧ ∅ ∈
B)) → (A = ∅ ∨
B = ∅))) |
6 | | simpr 103 |
. . . . . . 7
⊢ ((∅
∈ A ∧ B = ∅)
→ B = ∅) |
7 | 6 | olcd 652 |
. . . . . 6
⊢ ((∅
∈ A ∧ B = ∅)
→ (A = ∅
∨ B = ∅)) |
8 | 7 | a1i 9 |
. . . . 5
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) → ((∅ ∈ A ∧ B = ∅)
→ (A = ∅
∨ B = ∅))) |
9 | | simplr 482 |
. . . . . . 7
⊢
((((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) ∧
(∅ ∈ A ∧ ∅ ∈ B)) →
(A ·𝑜 B) = ∅) |
10 | | nnmordi 6025 |
. . . . . . . . . . . . 13
⊢
(((B ∈ 𝜔 ∧
A ∈
𝜔) ∧ ∅ ∈ A) →
(∅ ∈ B → (A
·𝑜 ∅) ∈
(A ·𝑜 B))) |
11 | 10 | expimpd 345 |
. . . . . . . . . . . 12
⊢
((B ∈ 𝜔 ∧
A ∈
𝜔) → ((∅ ∈ A ∧ ∅ ∈ B) →
(A ·𝑜 ∅)
∈ (A
·𝑜 B))) |
12 | 11 | ancoms 255 |
. . . . . . . . . . 11
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → ((∅ ∈ A ∧ ∅ ∈ B) →
(A ·𝑜 ∅)
∈ (A
·𝑜 B))) |
13 | | nnm0 5993 |
. . . . . . . . . . . . 13
⊢ (A ∈ 𝜔
→ (A ·𝑜
∅) = ∅) |
14 | 13 | adantr 261 |
. . . . . . . . . . . 12
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → (A
·𝑜 ∅) = ∅) |
15 | 14 | eleq1d 2103 |
. . . . . . . . . . 11
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → ((A
·𝑜 ∅) ∈
(A ·𝑜 B) ↔ ∅ ∈ (A
·𝑜 B))) |
16 | 12, 15 | sylibd 138 |
. . . . . . . . . 10
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → ((∅ ∈ A ∧ ∅ ∈ B) →
∅ ∈ (A ·𝑜 B))) |
17 | 16 | adantr 261 |
. . . . . . . . 9
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) → ((∅ ∈ A ∧ ∅ ∈
B) → ∅ ∈ (A
·𝑜 B))) |
18 | 17 | imp 115 |
. . . . . . . 8
⊢
((((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) ∧
(∅ ∈ A ∧ ∅ ∈ B)) →
∅ ∈ (A ·𝑜 B)) |
19 | | n0i 3223 |
. . . . . . . 8
⊢ (∅
∈ (A
·𝑜 B) →
¬ (A ·𝑜
B) = ∅) |
20 | 18, 19 | syl 14 |
. . . . . . 7
⊢
((((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) ∧
(∅ ∈ A ∧ ∅ ∈ B)) →
¬ (A ·𝑜
B) = ∅) |
21 | 9, 20 | pm2.21dd 550 |
. . . . . 6
⊢
((((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) ∧
(∅ ∈ A ∧ ∅ ∈ B)) →
(A = ∅
∨ B = ∅)) |
22 | 21 | ex 108 |
. . . . 5
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) → ((∅ ∈ A ∧ ∅ ∈
B) → (A = ∅ ∨
B = ∅))) |
23 | 8, 22 | jaod 636 |
. . . 4
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) → (((∅ ∈ A ∧ B = ∅)
∨ (∅ ∈
A ∧
∅ ∈ B)) → (A =
∅ ∨ B = ∅))) |
24 | | 0elnn 4283 |
. . . . . . 7
⊢ (A ∈ 𝜔
→ (A = ∅
∨ ∅ ∈ A)) |
25 | | 0elnn 4283 |
. . . . . . 7
⊢ (B ∈ 𝜔
→ (B = ∅
∨ ∅ ∈ B)) |
26 | 24, 25 | anim12i 321 |
. . . . . 6
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → ((A = ∅ ∨ ∅ ∈
A) ∧
(B = ∅
∨ ∅ ∈ B))) |
27 | | anddi 733 |
. . . . . 6
⊢
(((A = ∅ ∨ ∅ ∈
A) ∧
(B = ∅
∨ ∅ ∈ B)) ↔ (((A
= ∅ ∧ B = ∅) ∨
(A = ∅ ∧ ∅ ∈
B)) ∨
((∅ ∈ A ∧ B = ∅) ∨
(∅ ∈ A ∧ ∅ ∈ B)))) |
28 | 26, 27 | sylib 127 |
. . . . 5
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → (((A = ∅ ∧ B = ∅)
∨ (A =
∅ ∧ ∅ ∈ B)) ∨ ((∅ ∈
A ∧
B = ∅)
∨ (∅ ∈ A ∧ ∅ ∈ B)))) |
29 | 28 | adantr 261 |
. . . 4
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) → (((A = ∅ ∧
B = ∅)
∨ (A = ∅ ∧ ∅ ∈
B)) ∨
((∅ ∈ A ∧ B = ∅) ∨
(∅ ∈ A ∧ ∅ ∈ B)))) |
30 | 5, 23, 29 | mpjaod 637 |
. . 3
⊢
(((A ∈ 𝜔 ∧
B ∈
𝜔) ∧ (A ·𝑜 B) = ∅) → (A = ∅ ∨
B = ∅)) |
31 | 30 | ex 108 |
. 2
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → ((A
·𝑜 B) = ∅
→ (A = ∅
∨ B = ∅))) |
32 | | oveq1 5462 |
. . . . . 6
⊢ (A = ∅ → (A ·𝑜 B) = (∅ ·𝑜 B)) |
33 | | nnm0r 5997 |
. . . . . 6
⊢ (B ∈ 𝜔
→ (∅ ·𝑜 B) = ∅) |
34 | 32, 33 | sylan9eqr 2091 |
. . . . 5
⊢
((B ∈ 𝜔 ∧
A = ∅) → (A ·𝑜 B) = ∅) |
35 | 34 | ex 108 |
. . . 4
⊢ (B ∈ 𝜔
→ (A = ∅ → (A ·𝑜 B) = ∅)) |
36 | 35 | adantl 262 |
. . 3
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → (A = ∅ →
(A ·𝑜 B) = ∅)) |
37 | | oveq2 5463 |
. . . . . 6
⊢ (B = ∅ → (A ·𝑜 B) = (A
·𝑜 ∅)) |
38 | 37, 13 | sylan9eqr 2091 |
. . . . 5
⊢
((A ∈ 𝜔 ∧
B = ∅) → (A ·𝑜 B) = ∅) |
39 | 38 | ex 108 |
. . . 4
⊢ (A ∈ 𝜔
→ (B = ∅ → (A ·𝑜 B) = ∅)) |
40 | 39 | adantr 261 |
. . 3
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → (B = ∅ →
(A ·𝑜 B) = ∅)) |
41 | 36, 40 | jaod 636 |
. 2
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → ((A = ∅ ∨ B = ∅)
→ (A ·𝑜
B) = ∅)) |
42 | 31, 41 | impbid 120 |
1
⊢
((A ∈ 𝜔 ∧
B ∈
𝜔) → ((A
·𝑜 B) = ∅
↔ (A = ∅
∨ B = ∅))) |