Step | Hyp | Ref
| Expression |
1 | | elif 4128 |
. . . . . 6
⊢ (𝑥 ∈ if((𝑠 ∪ 𝑡) = {∅}, {∅,
1𝑜}, (𝑠
∪ 𝑡)) ↔ (((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)))) |
2 | | uneq12 3762 |
. . . . . . . . . . 11
⊢ ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠 ∪ 𝑡) = ({∅} ∪
{∅})) |
3 | | unidm 3756 |
. . . . . . . . . . 11
⊢
({∅} ∪ {∅}) = {∅} |
4 | 2, 3 | syl6eq 2672 |
. . . . . . . . . 10
⊢ ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠 ∪ 𝑡) = {∅}) |
5 | | an3 868 |
. . . . . . . . . . . . . 14
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))
→ (𝑠 = {∅} ∧
𝑥 ∈ {∅,
1𝑜})) |
6 | 5 | orcd 407 |
. . . . . . . . . . . . 13
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))
→ ((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠))) |
7 | 6 | orcd 407 |
. . . . . . . . . . . 12
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
8 | 7 | ex 450 |
. . . . . . . . . . 11
⊢ ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))))) |
9 | | pm2.24 121 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∪ 𝑡) = {∅} → (¬ (𝑠 ∪ 𝑡) = {∅} → (𝑥 ∈ (𝑠 ∪ 𝑡) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
10 | 9 | impd 447 |
. . . . . . . . . . 11
⊢ ((𝑠 ∪ 𝑡) = {∅} → ((¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))))) |
11 | 8, 10 | jaao 531 |
. . . . . . . . . 10
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ (𝑠 ∪ 𝑡) = {∅}) → ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))))) |
12 | 4, 11 | mpdan 702 |
. . . . . . . . 9
⊢ ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))))) |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ ((𝑠 = {∅}
∧ 𝑡 = {∅}) →
((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
14 | | uneqsn 38321 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∪ 𝑡) = {∅} ↔ ((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅}))) |
15 | | df-3or 1038 |
. . . . . . . . . . . . 13
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅}))) |
16 | 14, 15 | bitri 264 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∪ 𝑡) = {∅} ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅}))) |
17 | | pm2.21 120 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑠 = {∅} → (𝑠 = {∅} → (𝑥 ∈ {∅,
1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
18 | 17 | adantrd 484 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑠 = {∅} →
((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅,
1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
19 | 17 | adantrd 484 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑠 = {∅} →
((𝑠 = {∅} ∧ 𝑡 = ∅) → (𝑥 ∈ {∅,
1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
20 | 18, 19 | jaod 395 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑠 = {∅} →
(((𝑠 = {∅} ∧
𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅,
1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
21 | 20 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
(((𝑠 = {∅} ∧
𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅,
1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
22 | | pm2.21 120 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑡 = {∅} → (𝑡 = {∅} → (𝑥 ∈ {∅,
1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
(𝑡 = {∅} →
(𝑥 ∈ {∅,
1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
24 | 23 | adantld 483 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((𝑠 = ∅ ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅,
1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
25 | 21, 24 | jaod 395 |
. . . . . . . . . . . 12
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((((𝑠 = {∅} ∧
𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) → (𝑥 ∈ {∅,
1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
26 | 16, 25 | syl5bi 232 |
. . . . . . . . . . 11
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((𝑠 ∪ 𝑡) = {∅} → (𝑥 ∈ {∅,
1𝑜} → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
27 | 26 | impd 447 |
. . . . . . . . . 10
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
(((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))))) |
28 | | elun 3753 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑠 ∪ 𝑡) ↔ (𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡)) |
29 | 28 | biimpi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑠 ∪ 𝑡) → (𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡)) |
30 | 29 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)) → (𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡)) |
31 | | andi 911 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ (𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡)) ↔ (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥 ∈ 𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥 ∈ 𝑡))) |
32 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) → ¬
𝑠 =
{∅}) |
33 | 32 | anim1i 592 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ 𝑥 ∈ 𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) |
34 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) → ¬
𝑡 =
{∅}) |
35 | 34 | anim1i 592 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ 𝑥 ∈ 𝑡) → (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)) |
36 | 33, 35 | orim12i 538 |
. . . . . . . . . . . . . . 15
⊢ ((((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ 𝑥 ∈ 𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥 ∈ 𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
37 | 31, 36 | sylbi 207 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ (𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
38 | 30, 37 | sylan2 491 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
39 | 38 | olcd 408 |
. . . . . . . . . . . 12
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (𝑡 = {∅} ∧
𝑥 ∈ {∅,
1𝑜})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
40 | | or4 550 |
. . . . . . . . . . . 12
⊢ ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜}))
∨ ((¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
41 | 39, 40 | sylib 208 |
. . . . . . . . . . 11
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
42 | 41 | ex 450 |
. . . . . . . . . 10
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))))) |
43 | 27, 42 | jaod 395 |
. . . . . . . . 9
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))))) |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ ((¬ 𝑠 =
{∅} ∧ ¬ 𝑡 =
{∅}) → ((((𝑠
∪ 𝑡) = {∅} ∧
𝑥 ∈ {∅,
1𝑜}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
45 | 13, 44 | jaod 395 |
. . . . . . 7
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (((𝑠 = {∅}
∧ 𝑡 = {∅}) ∨
(¬ 𝑠 = {∅} ∧
¬ 𝑡 = {∅}))
→ ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
46 | | orc 400 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))) |
47 | 46 | expcom 451 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {∅,
1𝑜} → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
48 | 47 | adantrd 484 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {∅,
1𝑜} → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
49 | 48 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
→ ((𝑠 = {∅}
∧ ¬ 𝑡 = {∅})
→ ((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
50 | | simpr 477 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 = {∅}) → 𝑠 = {∅}) |
51 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = {∅} → 𝑠 = {∅}) |
52 | | snsspr1 4345 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {∅}
⊆ {∅, 1𝑜} |
53 | 51, 52 | syl6eqss 3655 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = {∅} → 𝑠 ⊆ {∅,
1𝑜}) |
54 | 53 | sseld 3602 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = {∅} → (𝑥 ∈ 𝑠 → 𝑥 ∈ {∅,
1𝑜})) |
55 | 54 | impcom 446 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 = {∅}) → 𝑥 ∈ {∅,
1𝑜}) |
56 | 50, 55 | jca 554 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 = {∅}) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜})) |
57 | 56 | orcd 407 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))) |
58 | 57 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑠 → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
59 | | olc 399 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))) |
60 | 59 | expcom 451 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑡 → (¬ 𝑡 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
61 | 58, 60 | jaoa 532 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
62 | 28, 61 | sylbi 207 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑠 ∪ 𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
63 | 62 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
64 | 49, 63 | jaoi 394 |
. . . . . . . . . . 11
⊢ ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
65 | | olc 399 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}))) |
66 | 65 | expcom 451 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {∅,
1𝑜} → (𝑡 = {∅} → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜})))) |
67 | 66 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
→ (𝑡 = {∅}
→ ((¬ 𝑠 =
{∅} ∧ 𝑥 ∈
𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜})))) |
68 | 67 | adantrd 484 |
. . . . . . . . . . . 12
⊢ (((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
→ ((𝑡 = {∅}
∧ ¬ 𝑠 = {∅})
→ ((¬ 𝑠 =
{∅} ∧ 𝑥 ∈
𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜})))) |
69 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ ((¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) |
70 | 69 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑠 = {∅} → (𝑥 ∈ 𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠))) |
71 | 70 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥 ∈ 𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠))) |
72 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = {∅} → 𝑡 = {∅}) |
73 | 72, 52 | syl6eqss 3655 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = {∅} → 𝑡 ⊆ {∅,
1𝑜}) |
74 | 73 | sseld 3602 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = {∅} → (𝑥 ∈ 𝑡 → 𝑥 ∈ {∅,
1𝑜})) |
75 | 74 | anc2li 580 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = {∅} → (𝑥 ∈ 𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}))) |
76 | 75 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥 ∈ 𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}))) |
77 | 71, 76 | orim12d 883 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜})))) |
78 | 77 | com12 32 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜})))) |
79 | 28, 78 | sylbi 207 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑠 ∪ 𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜})))) |
80 | 79 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜})))) |
81 | 68, 80 | jaoi 394 |
. . . . . . . . . . 11
⊢ ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜})))) |
82 | 64, 81 | orim12d 883 |
. . . . . . . . . 10
⊢ ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}))))) |
83 | 82 | com12 32 |
. . . . . . . . 9
⊢ (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}))))) |
84 | | or42 551 |
. . . . . . . . 9
⊢ ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})))
↔ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
85 | 83, 84 | syl6ib 241 |
. . . . . . . 8
⊢ (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))))) |
86 | 85 | a1i 11 |
. . . . . . 7
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (((𝑠 = {∅}
∧ ¬ 𝑡 = {∅})
∨ (𝑡 = {∅} ∧
¬ 𝑠 = {∅}))
→ ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))))) |
87 | | 4exmid 997 |
. . . . . . . 8
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅}))) |
88 | 87 | a1i 11 |
. . . . . . 7
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (((𝑠 = {∅}
∧ 𝑡 = {∅}) ∨
(¬ 𝑠 = {∅} ∧
¬ 𝑡 = {∅})) ∨
((𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 =
{∅})))) |
89 | 45, 86, 88 | mpjaod 396 |
. . . . . 6
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))))) |
90 | 1, 89 | syl5bi 232 |
. . . . 5
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (𝑥 ∈ if((𝑠 ∪ 𝑡) = {∅}, {∅,
1𝑜}, (𝑠
∪ 𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))))) |
91 | | elun 3753 |
. . . . . 6
⊢ (𝑥 ∈ (if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∪ if(𝑡 = {∅},
{∅, 1𝑜}, 𝑡)) ↔ (𝑥 ∈ if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∨ 𝑥 ∈ if(𝑡 = {∅}, {∅,
1𝑜}, 𝑡))) |
92 | | elif 4128 |
. . . . . . 7
⊢ (𝑥 ∈ if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
↔ ((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠))) |
93 | | elif 4128 |
. . . . . . 7
⊢ (𝑥 ∈ if(𝑡 = {∅}, {∅,
1𝑜}, 𝑡)
↔ ((𝑡 = {∅}
∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
94 | 92, 93 | orbi12i 543 |
. . . . . 6
⊢ ((𝑥 ∈ if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∨ 𝑥 ∈ if(𝑡 = {∅}, {∅,
1𝑜}, 𝑡))
↔ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡)))) |
95 | 91, 94 | sylbbr 226 |
. . . . 5
⊢ ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1𝑜})
∨ (¬ 𝑡 = {∅}
∧ 𝑥 ∈ 𝑡))) → 𝑥 ∈ (if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∪ if(𝑡 = {∅},
{∅, 1𝑜}, 𝑡))) |
96 | 90, 95 | syl6 35 |
. . . 4
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (𝑥 ∈ if((𝑠 ∪ 𝑡) = {∅}, {∅,
1𝑜}, (𝑠
∪ 𝑡)) → 𝑥 ∈ (if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∪ if(𝑡 = {∅},
{∅, 1𝑜}, 𝑡)))) |
97 | 96 | ssrdv 3609 |
. . 3
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ if((𝑠 ∪ 𝑡) = {∅}, {∅,
1𝑜}, (𝑠
∪ 𝑡)) ⊆ (if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∪ if(𝑡 = {∅},
{∅, 1𝑜}, 𝑡))) |
98 | | 3on 7570 |
. . . . . 6
⊢
3𝑜 ∈ On |
99 | 98 | a1i 11 |
. . . . 5
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ 3𝑜 ∈ On) |
100 | | elpwi 4168 |
. . . . . 6
⊢ (𝑠 ∈ 𝒫
3𝑜 → 𝑠 ⊆
3𝑜) |
101 | | elpwi 4168 |
. . . . . 6
⊢ (𝑡 ∈ 𝒫
3𝑜 → 𝑡 ⊆
3𝑜) |
102 | | unss 3787 |
. . . . . . 7
⊢ ((𝑠 ⊆ 3𝑜
∧ 𝑡 ⊆
3𝑜) ↔ (𝑠 ∪ 𝑡) ⊆
3𝑜) |
103 | 102 | biimpi 206 |
. . . . . 6
⊢ ((𝑠 ⊆ 3𝑜
∧ 𝑡 ⊆
3𝑜) → (𝑠 ∪ 𝑡) ⊆
3𝑜) |
104 | 100, 101,
103 | syl2an 494 |
. . . . 5
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (𝑠 ∪ 𝑡) ⊆
3𝑜) |
105 | 99, 104 | sselpwd 4807 |
. . . 4
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (𝑠 ∪ 𝑡) ∈ 𝒫
3𝑜) |
106 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑟 = (𝑠 ∪ 𝑡) → (𝑟 = {∅} ↔ (𝑠 ∪ 𝑡) = {∅})) |
107 | | id 22 |
. . . . . 6
⊢ (𝑟 = (𝑠 ∪ 𝑡) → 𝑟 = (𝑠 ∪ 𝑡)) |
108 | 106, 107 | ifbieq2d 4111 |
. . . . 5
⊢ (𝑟 = (𝑠 ∪ 𝑡) → if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)
= if((𝑠 ∪ 𝑡) = {∅}, {∅,
1𝑜}, (𝑠
∪ 𝑡))) |
109 | | clsk1indlem.k |
. . . . 5
⊢ 𝐾 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) |
110 | | prex 4909 |
. . . . . 6
⊢ {∅,
1𝑜} ∈ V |
111 | | vex 3203 |
. . . . . . 7
⊢ 𝑠 ∈ V |
112 | | vex 3203 |
. . . . . . 7
⊢ 𝑡 ∈ V |
113 | 111, 112 | unex 6956 |
. . . . . 6
⊢ (𝑠 ∪ 𝑡) ∈ V |
114 | 110, 113 | ifex 4156 |
. . . . 5
⊢ if((𝑠 ∪ 𝑡) = {∅}, {∅,
1𝑜}, (𝑠
∪ 𝑡)) ∈
V |
115 | 108, 109,
114 | fvmpt 6282 |
. . . 4
⊢ ((𝑠 ∪ 𝑡) ∈ 𝒫 3𝑜
→ (𝐾‘(𝑠 ∪ 𝑡)) = if((𝑠 ∪ 𝑡) = {∅}, {∅,
1𝑜}, (𝑠
∪ 𝑡))) |
116 | 105, 115 | syl 17 |
. . 3
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (𝐾‘(𝑠 ∪ 𝑡)) = if((𝑠 ∪ 𝑡) = {∅}, {∅,
1𝑜}, (𝑠
∪ 𝑡))) |
117 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → (𝑟 = {∅} ↔ 𝑠 = {∅})) |
118 | | id 22 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → 𝑟 = 𝑠) |
119 | 117, 118 | ifbieq2d 4111 |
. . . . . 6
⊢ (𝑟 = 𝑠 → if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)
= if(𝑠 = {∅},
{∅, 1𝑜}, 𝑠)) |
120 | 110, 111 | ifex 4156 |
. . . . . 6
⊢ if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∈ V |
121 | 119, 109,
120 | fvmpt 6282 |
. . . . 5
⊢ (𝑠 ∈ 𝒫
3𝑜 → (𝐾‘𝑠) = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)) |
122 | 121 | adantr 481 |
. . . 4
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (𝐾‘𝑠) = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)) |
123 | | eqeq1 2626 |
. . . . . . 7
⊢ (𝑟 = 𝑡 → (𝑟 = {∅} ↔ 𝑡 = {∅})) |
124 | | id 22 |
. . . . . . 7
⊢ (𝑟 = 𝑡 → 𝑟 = 𝑡) |
125 | 123, 124 | ifbieq2d 4111 |
. . . . . 6
⊢ (𝑟 = 𝑡 → if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)
= if(𝑡 = {∅},
{∅, 1𝑜}, 𝑡)) |
126 | 110, 112 | ifex 4156 |
. . . . . 6
⊢ if(𝑡 = {∅}, {∅,
1𝑜}, 𝑡)
∈ V |
127 | 125, 109,
126 | fvmpt 6282 |
. . . . 5
⊢ (𝑡 ∈ 𝒫
3𝑜 → (𝐾‘𝑡) = if(𝑡 = {∅}, {∅,
1𝑜}, 𝑡)) |
128 | 127 | adantl 482 |
. . . 4
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (𝐾‘𝑡) = if(𝑡 = {∅}, {∅,
1𝑜}, 𝑡)) |
129 | 122, 128 | uneq12d 3768 |
. . 3
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = (if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∪ if(𝑡 = {∅},
{∅, 1𝑜}, 𝑡))) |
130 | 97, 116, 129 | 3sstr4d 3648 |
. 2
⊢ ((𝑠 ∈ 𝒫
3𝑜 ∧ 𝑡 ∈ 𝒫 3𝑜)
→ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))) |
131 | 130 | rgen2a 2977 |
1
⊢
∀𝑠 ∈
𝒫 3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) |