Step | Hyp | Ref
| Expression |
1 | | elif 4508 |
. . . . . 6
⊢ (𝑥 ∈ if((𝑠 ∪ 𝑡) = {∅}, {∅, 1o},
(𝑠 ∪ 𝑡)) ↔ (((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)))) |
2 | | uneq12 4097 |
. . . . . . . . . . 11
⊢ ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠 ∪ 𝑡) = ({∅} ∪
{∅})) |
3 | | unidm 4091 |
. . . . . . . . . . 11
⊢
({∅} ∪ {∅}) = {∅} |
4 | 2, 3 | eqtrdi 2796 |
. . . . . . . . . 10
⊢ ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑠 ∪ 𝑡) = {∅}) |
5 | | an3 656 |
. . . . . . . . . . . . . 14
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o})) →
(𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1o})) |
6 | 5 | orcd 870 |
. . . . . . . . . . . . 13
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o})) →
((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠))) |
7 | 6 | orcd 870 |
. . . . . . . . . . . 12
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ ((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o})) →
(((𝑠 = {∅} ∧
𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
8 | 7 | ex 413 |
. . . . . . . . . . 11
⊢ ((𝑠 = {∅} ∧ 𝑡 = {∅}) → (((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) →
(((𝑠 = {∅} ∧
𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))))) |
9 | | pm2.24 124 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∪ 𝑡) = {∅} → (¬ (𝑠 ∪ 𝑡) = {∅} → (𝑥 ∈ (𝑠 ∪ 𝑡) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
10 | 9 | impd 411 |
. . . . . . . . . . 11
⊢ ((𝑠 ∪ 𝑡) = {∅} → ((¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))))) |
11 | 8, 10 | jaao 952 |
. . . . . . . . . 10
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∧ (𝑠 ∪ 𝑡) = {∅}) → ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))))) |
12 | 4, 11 | mpdan 684 |
. . . . . . . . 9
⊢ ((𝑠 = {∅} ∧ 𝑡 = {∅}) → ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))))) |
13 | 12 | a1i 11 |
. . . . . . . 8
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → ((𝑠 =
{∅} ∧ 𝑡 =
{∅}) → ((((𝑠
∪ 𝑡) = {∅} ∧
𝑥 ∈ {∅,
1o}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
14 | | uneqsn 41615 |
. . . . . . . . . . . . 13
⊢ ((𝑠 ∪ 𝑡) = {∅} ↔ ((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅}))) |
15 | | df-3or 1087 |
. . . . . . . . . . . . 13
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅}))) |
16 | 14, 15 | bitri 274 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∪ 𝑡) = {∅} ↔ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅}))) |
17 | | pm2.21 123 |
. . . . . . . . . . . . . . . 16
⊢ (¬
𝑠 = {∅} → (𝑠 = {∅} → (𝑥 ∈ {∅, 1o}
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
18 | 17 | adantrd 492 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑠 = {∅} →
((𝑠 = {∅} ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1o}
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
19 | 17 | adantrd 492 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑠 = {∅} →
((𝑠 = {∅} ∧ 𝑡 = ∅) → (𝑥 ∈ {∅, 1o}
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
20 | 18, 19 | jaod 856 |
. . . . . . . . . . . . . 14
⊢ (¬
𝑠 = {∅} →
(((𝑠 = {∅} ∧
𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1o}
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
21 | 20 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
(((𝑠 = {∅} ∧
𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) → (𝑥 ∈ {∅, 1o}
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
22 | | pm2.21 123 |
. . . . . . . . . . . . . . 15
⊢ (¬
𝑡 = {∅} → (𝑡 = {∅} → (𝑥 ∈ {∅, 1o}
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
(𝑡 = {∅} →
(𝑥 ∈ {∅,
1o} → (((𝑠
= {∅} ∧ 𝑥 ∈
{∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
24 | 23 | adantld 491 |
. . . . . . . . . . . . 13
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((𝑠 = ∅ ∧ 𝑡 = {∅}) → (𝑥 ∈ {∅, 1o}
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
25 | 21, 24 | jaod 856 |
. . . . . . . . . . . 12
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((((𝑠 = {∅} ∧
𝑡 = {∅}) ∨ (𝑠 = {∅} ∧ 𝑡 = ∅)) ∨ (𝑠 = ∅ ∧ 𝑡 = {∅})) → (𝑥 ∈ {∅, 1o}
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
26 | 16, 25 | syl5bi 241 |
. . . . . . . . . . 11
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((𝑠 ∪ 𝑡) = {∅} → (𝑥 ∈ {∅, 1o}
→ (((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
27 | 26 | impd 411 |
. . . . . . . . . 10
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
(((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅,
1o}) → (((𝑠
= {∅} ∧ 𝑥 ∈
{∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))))) |
28 | | elun 4088 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑠 ∪ 𝑡) ↔ (𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡)) |
29 | 28 | biimpi 215 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝑠 ∪ 𝑡) → (𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡)) |
30 | 29 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)) → (𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡)) |
31 | | andi 1005 |
. . . . . . . . . . . . . . 15
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ (𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡)) ↔ (((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥 ∈ 𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥 ∈ 𝑡))) |
32 | | simpl 483 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) → ¬
𝑠 =
{∅}) |
33 | 32 | anim1i 615 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ 𝑥 ∈ 𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) |
34 | | simpr 485 |
. . . . . . . . . . . . . . . . 17
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) → ¬
𝑡 =
{∅}) |
35 | 34 | anim1i 615 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ 𝑥 ∈ 𝑡) → (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)) |
36 | 33, 35 | orim12i 906 |
. . . . . . . . . . . . . . 15
⊢ ((((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ 𝑥 ∈ 𝑠) ∨ ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∧ 𝑥 ∈ 𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
37 | 31, 36 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ (𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡)) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
38 | 30, 37 | sylan2 593 |
. . . . . . . . . . . . 13
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
39 | 38 | olcd 871 |
. . . . . . . . . . . 12
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
40 | | or4 924 |
. . . . . . . . . . . 12
⊢ ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1o}) ∨ (𝑡 =
{∅} ∧ 𝑥 ∈
{∅, 1o})) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
41 | 39, 40 | sylib 217 |
. . . . . . . . . . 11
⊢ (((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) ∧ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
42 | 41 | ex 413 |
. . . . . . . . . 10
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))))) |
43 | 27, 42 | jaod 856 |
. . . . . . . . 9
⊢ ((¬
𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))))) |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → ((¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
45 | 13, 44 | jaod 856 |
. . . . . . 7
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → (((𝑠
= {∅} ∧ 𝑡 =
{∅}) ∨ (¬ 𝑠 =
{∅} ∧ ¬ 𝑡 =
{∅})) → ((((𝑠
∪ 𝑡) = {∅} ∧
𝑥 ∈ {∅,
1o}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
46 | | orc 864 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1o}) → ((𝑠
= {∅} ∧ 𝑥 ∈
{∅, 1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
47 | 46 | expcom 414 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {∅, 1o}
→ (𝑠 = {∅}
→ ((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
48 | 47 | adantrd 492 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ {∅, 1o}
→ ((𝑠 = {∅}
∧ ¬ 𝑡 = {∅})
→ ((𝑠 = {∅}
∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
49 | 48 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) →
((𝑠 = {∅} ∧ ¬
𝑡 = {∅}) →
((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
50 | | simpr 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 = {∅}) → 𝑠 = {∅}) |
51 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = {∅} → 𝑠 = {∅}) |
52 | | snsspr1 4753 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ {∅}
⊆ {∅, 1o} |
53 | 51, 52 | eqsstrdi 3980 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = {∅} → 𝑠 ⊆ {∅,
1o}) |
54 | 53 | sseld 3925 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = {∅} → (𝑥 ∈ 𝑠 → 𝑥 ∈ {∅,
1o})) |
55 | 54 | impcom 408 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 = {∅}) → 𝑥 ∈ {∅,
1o}) |
56 | 50, 55 | jca 512 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 = {∅}) → (𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1o})) |
57 | 56 | orcd 870 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝑠 ∧ 𝑠 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
58 | 57 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑠 → (𝑠 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
59 | | olc 865 |
. . . . . . . . . . . . . . . 16
⊢ ((¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
60 | 59 | expcom 414 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ 𝑡 → (¬ 𝑡 = {∅} → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
61 | 58, 60 | jaoa 953 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
62 | 28, 61 | sylbi 216 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑠 ∪ 𝑡) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
63 | 62 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
64 | 49, 63 | jaoi 854 |
. . . . . . . . . . 11
⊢ ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) → ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
65 | | olc 865 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o}) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o}))) |
66 | 65 | expcom 414 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {∅, 1o}
→ (𝑡 = {∅}
→ ((¬ 𝑠 =
{∅} ∧ 𝑥 ∈
𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o})))) |
67 | 66 | adantl 482 |
. . . . . . . . . . . . 13
⊢ (((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) →
(𝑡 = {∅} →
((¬ 𝑠 = {∅} ∧
𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o})))) |
68 | 67 | adantrd 492 |
. . . . . . . . . . . 12
⊢ (((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) →
((𝑡 = {∅} ∧ ¬
𝑠 = {∅}) →
((¬ 𝑠 = {∅} ∧
𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o})))) |
69 | | id 22 |
. . . . . . . . . . . . . . . . . 18
⊢ ((¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) → (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) |
70 | 69 | ex 413 |
. . . . . . . . . . . . . . . . 17
⊢ (¬
𝑠 = {∅} → (𝑥 ∈ 𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠))) |
71 | 70 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥 ∈ 𝑠 → (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠))) |
72 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑡 = {∅} → 𝑡 = {∅}) |
73 | 72, 52 | eqsstrdi 3980 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑡 = {∅} → 𝑡 ⊆ {∅,
1o}) |
74 | 73 | sseld 3925 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 = {∅} → (𝑥 ∈ 𝑡 → 𝑥 ∈ {∅,
1o})) |
75 | 74 | anc2li 556 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = {∅} → (𝑥 ∈ 𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o}))) |
76 | 75 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → (𝑥 ∈ 𝑡 → (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o}))) |
77 | 71, 76 | orim12d 962 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o})))) |
78 | 77 | com12 32 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝑠 ∨ 𝑥 ∈ 𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o})))) |
79 | 28, 78 | sylbi 216 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (𝑠 ∪ 𝑡) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o})))) |
80 | 79 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡)) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o})))) |
81 | 68, 80 | jaoi 854 |
. . . . . . . . . . 11
⊢ ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → ((𝑡 = {∅} ∧ ¬ 𝑠 = {∅}) → ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o})))) |
82 | 64, 81 | orim12d 962 |
. . . . . . . . . 10
⊢ ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o}))))) |
83 | 82 | com12 32 |
. . . . . . . . 9
⊢ (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅,
1o}))))) |
84 | | or42 925 |
. . . . . . . . 9
⊢ ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)) ∨ ((¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠) ∨ (𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}))) ↔
(((𝑠 = {∅} ∧
𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
85 | 83, 84 | syl6ib 250 |
. . . . . . . 8
⊢ (((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅})) → ((((𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
(𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))))) |
86 | 85 | a1i 11 |
. . . . . . 7
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → (((𝑠
= {∅} ∧ ¬ 𝑡 =
{∅}) ∨ (𝑡 =
{∅} ∧ ¬ 𝑠 =
{∅})) → ((((𝑠
∪ 𝑡) = {∅} ∧
𝑥 ∈ {∅,
1o}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))))) |
87 | | 4exmid 1049 |
. . . . . . . 8
⊢ (((𝑠 = {∅} ∧ 𝑡 = {∅}) ∨ (¬ 𝑠 = {∅} ∧ ¬ 𝑡 = {∅})) ∨ ((𝑠 = {∅} ∧ ¬ 𝑡 = {∅}) ∨ (𝑡 = {∅} ∧ ¬ 𝑠 = {∅}))) |
88 | 87 | a1i 11 |
. . . . . . 7
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → (((𝑠
= {∅} ∧ 𝑡 =
{∅}) ∨ (¬ 𝑠 =
{∅} ∧ ¬ 𝑡 =
{∅})) ∨ ((𝑠 =
{∅} ∧ ¬ 𝑡 =
{∅}) ∨ (𝑡 =
{∅} ∧ ¬ 𝑠 =
{∅})))) |
89 | 45, 86, 88 | mpjaod 857 |
. . . . . 6
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → ((((𝑠
∪ 𝑡) = {∅} ∧
𝑥 ∈ {∅,
1o}) ∨ (¬ (𝑠 ∪ 𝑡) = {∅} ∧ 𝑥 ∈ (𝑠 ∪ 𝑡))) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))))) |
90 | 1, 89 | syl5bi 241 |
. . . . 5
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → (𝑥
∈ if((𝑠 ∪ 𝑡) = {∅}, {∅,
1o}, (𝑠 ∪
𝑡)) → (((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))))) |
91 | | elun 4088 |
. . . . . 6
⊢ (𝑥 ∈ (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡)) ↔ (𝑥 ∈ if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1o}, 𝑡))) |
92 | | elif 4508 |
. . . . . . 7
⊢ (𝑥 ∈ if(𝑠 = {∅}, {∅, 1o}, 𝑠) ↔ ((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠))) |
93 | | elif 4508 |
. . . . . . 7
⊢ (𝑥 ∈ if(𝑡 = {∅}, {∅, 1o}, 𝑡) ↔ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) |
94 | 92, 93 | orbi12i 912 |
. . . . . 6
⊢ ((𝑥 ∈ if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∨ 𝑥 ∈ if(𝑡 = {∅}, {∅, 1o}, 𝑡)) ↔ (((𝑠 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡)))) |
95 | 91, 94 | sylbbr 235 |
. . . . 5
⊢ ((((𝑠 = {∅} ∧ 𝑥 ∈ {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ 𝑥 ∈ 𝑠)) ∨ ((𝑡 = {∅} ∧ 𝑥 ∈ {∅, 1o}) ∨ (¬
𝑡 = {∅} ∧ 𝑥 ∈ 𝑡))) → 𝑥 ∈ (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡))) |
96 | 90, 95 | syl6 35 |
. . . 4
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → (𝑥
∈ if((𝑠 ∪ 𝑡) = {∅}, {∅,
1o}, (𝑠 ∪
𝑡)) → 𝑥 ∈ (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡)))) |
97 | 96 | ssrdv 3932 |
. . 3
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → if((𝑠
∪ 𝑡) = {∅},
{∅, 1o}, (𝑠 ∪ 𝑡)) ⊆ (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡))) |
98 | | pwuncl 7615 |
. . . 4
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → (𝑠
∪ 𝑡) ∈ 𝒫
3o) |
99 | | eqeq1 2744 |
. . . . . 6
⊢ (𝑟 = (𝑠 ∪ 𝑡) → (𝑟 = {∅} ↔ (𝑠 ∪ 𝑡) = {∅})) |
100 | | id 22 |
. . . . . 6
⊢ (𝑟 = (𝑠 ∪ 𝑡) → 𝑟 = (𝑠 ∪ 𝑡)) |
101 | 99, 100 | ifbieq2d 4491 |
. . . . 5
⊢ (𝑟 = (𝑠 ∪ 𝑡) → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if((𝑠 ∪ 𝑡) = {∅}, {∅, 1o},
(𝑠 ∪ 𝑡))) |
102 | | clsk1indlem.k |
. . . . 5
⊢ 𝐾 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) |
103 | | prex 5359 |
. . . . . 6
⊢ {∅,
1o} ∈ V |
104 | | vex 3435 |
. . . . . . 7
⊢ 𝑠 ∈ V |
105 | | vex 3435 |
. . . . . . 7
⊢ 𝑡 ∈ V |
106 | 104, 105 | unex 7591 |
. . . . . 6
⊢ (𝑠 ∪ 𝑡) ∈ V |
107 | 103, 106 | ifex 4515 |
. . . . 5
⊢ if((𝑠 ∪ 𝑡) = {∅}, {∅, 1o},
(𝑠 ∪ 𝑡)) ∈ V |
108 | 101, 102,
107 | fvmpt 6872 |
. . . 4
⊢ ((𝑠 ∪ 𝑡) ∈ 𝒫 3o →
(𝐾‘(𝑠 ∪ 𝑡)) = if((𝑠 ∪ 𝑡) = {∅}, {∅, 1o},
(𝑠 ∪ 𝑡))) |
109 | 98, 108 | syl 17 |
. . 3
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → (𝐾‘(𝑠 ∪ 𝑡)) = if((𝑠 ∪ 𝑡) = {∅}, {∅, 1o},
(𝑠 ∪ 𝑡))) |
110 | | eqeq1 2744 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → (𝑟 = {∅} ↔ 𝑠 = {∅})) |
111 | | id 22 |
. . . . . . 7
⊢ (𝑟 = 𝑠 → 𝑟 = 𝑠) |
112 | 110, 111 | ifbieq2d 4491 |
. . . . . 6
⊢ (𝑟 = 𝑠 → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if(𝑠 = {∅}, {∅, 1o}, 𝑠)) |
113 | 103, 104 | ifex 4515 |
. . . . . 6
⊢ if(𝑠 = {∅}, {∅,
1o}, 𝑠) ∈
V |
114 | 112, 102,
113 | fvmpt 6872 |
. . . . 5
⊢ (𝑠 ∈ 𝒫 3o
→ (𝐾‘𝑠) = if(𝑠 = {∅}, {∅, 1o}, 𝑠)) |
115 | 114 | adantr 481 |
. . . 4
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → (𝐾‘𝑠) = if(𝑠 = {∅}, {∅, 1o}, 𝑠)) |
116 | | eqeq1 2744 |
. . . . . . 7
⊢ (𝑟 = 𝑡 → (𝑟 = {∅} ↔ 𝑡 = {∅})) |
117 | | id 22 |
. . . . . . 7
⊢ (𝑟 = 𝑡 → 𝑟 = 𝑡) |
118 | 116, 117 | ifbieq2d 4491 |
. . . . . 6
⊢ (𝑟 = 𝑡 → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if(𝑡 = {∅}, {∅, 1o}, 𝑡)) |
119 | 103, 105 | ifex 4515 |
. . . . . 6
⊢ if(𝑡 = {∅}, {∅,
1o}, 𝑡) ∈
V |
120 | 118, 102,
119 | fvmpt 6872 |
. . . . 5
⊢ (𝑡 ∈ 𝒫 3o
→ (𝐾‘𝑡) = if(𝑡 = {∅}, {∅, 1o}, 𝑡)) |
121 | 120 | adantl 482 |
. . . 4
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → (𝐾‘𝑡) = if(𝑡 = {∅}, {∅, 1o}, 𝑡)) |
122 | 115, 121 | uneq12d 4103 |
. . 3
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) = (if(𝑠 = {∅}, {∅, 1o}, 𝑠) ∪ if(𝑡 = {∅}, {∅, 1o}, 𝑡))) |
123 | 97, 109, 122 | 3sstr4d 3973 |
. 2
⊢ ((𝑠 ∈ 𝒫 3o
∧ 𝑡 ∈ 𝒫
3o) → (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))) |
124 | 123 | rgen2 3129 |
1
⊢
∀𝑠 ∈
𝒫 3o∀𝑡 ∈ 𝒫 3o(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)) |