| Step | Hyp | Ref
| Expression |
| 1 | | 3on 8524 |
. . 3
⊢
3o ∈ On |
| 2 | 1 | elexi 3503 |
. 2
⊢
3o ∈ V |
| 3 | | eqid 2737 |
. . . . 5
⊢ (𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟)) = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) |
| 4 | | notnotr 130 |
. . . . . . . . . . 11
⊢ (¬
¬ 𝑟 = {∅} →
𝑟 =
{∅}) |
| 5 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑟 ∈ 𝒫 3o
→ (¬ ¬ 𝑟 =
{∅} → 𝑟 =
{∅})) |
| 6 | | sssucid 6464 |
. . . . . . . . . . . . 13
⊢
2o ⊆ suc 2o |
| 7 | | 2oex 8517 |
. . . . . . . . . . . . . 14
⊢
2o ∈ V |
| 8 | 7 | elpw 4604 |
. . . . . . . . . . . . 13
⊢
(2o ∈ 𝒫 suc 2o ↔ 2o
⊆ suc 2o) |
| 9 | 6, 8 | mpbir 231 |
. . . . . . . . . . . 12
⊢
2o ∈ 𝒫 suc 2o |
| 10 | | df2o3 8514 |
. . . . . . . . . . . 12
⊢
2o = {∅, 1o} |
| 11 | | df-3o 8508 |
. . . . . . . . . . . . . 14
⊢
3o = suc 2o |
| 12 | 11 | eqcomi 2746 |
. . . . . . . . . . . . 13
⊢ suc
2o = 3o |
| 13 | 12 | pweqi 4616 |
. . . . . . . . . . . 12
⊢ 𝒫
suc 2o = 𝒫 3o |
| 14 | 9, 10, 13 | 3eltr3i 2853 |
. . . . . . . . . . 11
⊢ {∅,
1o} ∈ 𝒫 3o |
| 15 | 14 | 2a1i 12 |
. . . . . . . . . 10
⊢ (𝑟 ∈ 𝒫 3o
→ (¬ ¬ 𝑟 =
{∅} → {∅, 1o} ∈ 𝒫
3o)) |
| 16 | 5, 15 | jcad 512 |
. . . . . . . . 9
⊢ (𝑟 ∈ 𝒫 3o
→ (¬ ¬ 𝑟 =
{∅} → (𝑟 =
{∅} ∧ {∅, 1o} ∈ 𝒫
3o))) |
| 17 | 16 | con1d 145 |
. . . . . . . 8
⊢ (𝑟 ∈ 𝒫 3o
→ (¬ (𝑟 =
{∅} ∧ {∅, 1o} ∈ 𝒫 3o) →
¬ 𝑟 =
{∅})) |
| 18 | 17 | anc2ri 556 |
. . . . . . 7
⊢ (𝑟 ∈ 𝒫 3o
→ (¬ (𝑟 =
{∅} ∧ {∅, 1o} ∈ 𝒫 3o) →
(¬ 𝑟 = {∅} ∧
𝑟 ∈ 𝒫
3o))) |
| 19 | 18 | orrd 864 |
. . . . . 6
⊢ (𝑟 ∈ 𝒫 3o
→ ((𝑟 = {∅}
∧ {∅, 1o} ∈ 𝒫 3o) ∨ (¬
𝑟 = {∅} ∧ 𝑟 ∈ 𝒫
3o))) |
| 20 | | ifel 4570 |
. . . . . 6
⊢ (if(𝑟 = {∅}, {∅,
1o}, 𝑟) ∈
𝒫 3o ↔ ((𝑟 = {∅} ∧ {∅, 1o}
∈ 𝒫 3o) ∨ (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫
3o))) |
| 21 | 19, 20 | sylibr 234 |
. . . . 5
⊢ (𝑟 ∈ 𝒫 3o
→ if(𝑟 = {∅},
{∅, 1o}, 𝑟) ∈ 𝒫
3o) |
| 22 | 3, 21 | fmpti 7132 |
. . . 4
⊢ (𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟)):𝒫 3o⟶𝒫
3o |
| 23 | 2 | pwex 5380 |
. . . . 5
⊢ 𝒫
3o ∈ V |
| 24 | 23, 23 | elmap 8911 |
. . . 4
⊢ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟)) ∈ (𝒫 3o
↑m 𝒫 3o) ↔ (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)):𝒫 3o⟶𝒫
3o) |
| 25 | 22, 24 | mpbir 231 |
. . 3
⊢ (𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟)) ∈ (𝒫 3o
↑m 𝒫 3o) |
| 26 | 3 | clsk1indlem0 44054 |
. . . . . 6
⊢ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘∅) = ∅ |
| 27 | 3 | clsk1indlem2 44055 |
. . . . . 6
⊢
∀𝑠 ∈
𝒫 3o𝑠
⊆ ((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) |
| 28 | 26, 27 | pm3.2i 470 |
. . . . 5
⊢ (((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3o𝑠 ⊆
((𝑟 ∈ 𝒫
3o ↦ if(𝑟
= {∅}, {∅, 1o}, 𝑟))‘𝑠)) |
| 29 | 3 | clsk1indlem3 44056 |
. . . . . 6
⊢
∀𝑠 ∈
𝒫 3o∀𝑡 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) |
| 30 | 3 | clsk1indlem4 44057 |
. . . . . 6
⊢
∀𝑠 ∈
𝒫 3o((𝑟
∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) |
| 31 | 29, 30 | pm3.2i 470 |
. . . . 5
⊢
(∀𝑠 ∈
𝒫 3o∀𝑡 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) |
| 32 | 28, 31 | pm3.2i 470 |
. . . 4
⊢ ((((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3o𝑠 ⊆
((𝑟 ∈ 𝒫
3o ↦ if(𝑟
= {∅}, {∅, 1o}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
| 33 | 3 | clsk1indlem1 44058 |
. . . 4
⊢
∃𝑠 ∈
𝒫 3o∃𝑡 ∈ 𝒫 3o(𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) |
| 34 | 32, 33 | pm3.2i 470 |
. . 3
⊢
(((((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘∅) = ∅
∧ ∀𝑠 ∈
𝒫 3o𝑠
⊆ ((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) ∧ ∃𝑠 ∈ 𝒫 3o∃𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡))) |
| 35 | | fveq1 6905 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑘‘∅) = ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘∅)) |
| 36 | 35 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑘‘∅) =
∅ ↔ ((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘∅) =
∅)) |
| 37 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑘‘𝑠) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) |
| 38 | 37 | sseq2d 4016 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑠 ⊆ (𝑘‘𝑠) ↔ 𝑠 ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
| 39 | 38 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
| 40 | 36, 39 | anbi12d 632 |
. . . . . 6
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(((𝑘‘∅) =
∅ ∧ ∀𝑠
∈ 𝒫 3o𝑠 ⊆ (𝑘‘𝑠)) ↔ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3o𝑠 ⊆
((𝑟 ∈ 𝒫
3o ↦ if(𝑟
= {∅}, {∅, 1o}, 𝑟))‘𝑠)))) |
| 41 | | fveq1 6905 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑘‘(𝑠 ∪ 𝑡)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘(𝑠 ∪ 𝑡))) |
| 42 | | fveq1 6905 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑘‘𝑡) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) |
| 43 | 37, 42 | uneq12d 4169 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡))) |
| 44 | 41, 43 | sseq12d 4017 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
| 45 | 44 | 2ralbidv 3221 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(∀𝑠 ∈ 𝒫
3o∀𝑡
∈ 𝒫 3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
| 46 | | id 22 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))) |
| 47 | 46, 37 | fveq12d 6913 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑘‘(𝑘‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
| 48 | 47, 37 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠) ↔ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
| 49 | 48 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(∀𝑠 ∈ 𝒫
3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
| 50 | 45, 49 | anbi12d 632 |
. . . . . 6
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((∀𝑠 ∈
𝒫 3o∀𝑡 ∈ 𝒫 3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠)) ↔ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)))) |
| 51 | 40, 50 | anbi12d 632 |
. . . . 5
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((((𝑘‘∅) =
∅ ∧ ∀𝑠
∈ 𝒫 3o𝑠 ⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ↔ ((((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3o𝑠 ⊆
((𝑟 ∈ 𝒫
3o ↦ if(𝑟
= {∅}, {∅, 1o}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))))) |
| 52 | | rexnal2 3135 |
. . . . . 6
⊢
(∃𝑠 ∈
𝒫 3o∃𝑡 ∈ 𝒫 3o ¬ (𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
| 53 | | pm4.61 404 |
. . . . . . . 8
⊢ (¬
(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ (𝑠 ⊆ 𝑡 ∧ ¬ (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
| 54 | 37, 42 | sseq12d 4017 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑘‘𝑠) ⊆ (𝑘‘𝑡) ↔ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡))) |
| 55 | 54 | notbid 318 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(¬ (𝑘‘𝑠) ⊆ (𝑘‘𝑡) ↔ ¬ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡))) |
| 56 | 55 | anbi2d 630 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑠 ⊆ 𝑡 ∧ ¬ (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ (𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
| 57 | 53, 56 | bitrid 283 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(¬ (𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ (𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
| 58 | 57 | 2rexbidv 3222 |
. . . . . 6
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(∃𝑠 ∈ 𝒫
3o∃𝑡
∈ 𝒫 3o ¬ (𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∃𝑠 ∈ 𝒫 3o∃𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
| 59 | 52, 58 | bitr3id 285 |
. . . . 5
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(¬ ∀𝑠 ∈
𝒫 3o∀𝑡 ∈ 𝒫 3o(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∃𝑠 ∈ 𝒫 3o∃𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
| 60 | 51, 59 | anbi12d 632 |
. . . 4
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(((((𝑘‘∅) =
∅ ∧ ∀𝑠
∈ 𝒫 3o𝑠 ⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) ↔ (((((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3o𝑠 ⊆
((𝑟 ∈ 𝒫
3o ↦ if(𝑟
= {∅}, {∅, 1o}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) ∧ ∃𝑠 ∈ 𝒫 3o∃𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡))))) |
| 61 | 60 | rspcev 3622 |
. . 3
⊢ (((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟)) ∈ (𝒫 3o
↑m 𝒫 3o) ∧ (((((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3o𝑠 ⊆
((𝑟 ∈ 𝒫
3o ↦ if(𝑟
= {∅}, {∅, 1o}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) ∧ ∃𝑠 ∈ 𝒫 3o∃𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) → ∃𝑘 ∈ (𝒫 3o
↑m 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
| 62 | 25, 34, 61 | mp2an 692 |
. 2
⊢
∃𝑘 ∈
(𝒫 3o ↑m 𝒫 3o)((((𝑘‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
| 63 | | pweq 4614 |
. . . . . 6
⊢ (𝑏 = 3o →
𝒫 𝑏 = 𝒫
3o) |
| 64 | 63, 63 | oveq12d 7449 |
. . . . 5
⊢ (𝑏 = 3o →
(𝒫 𝑏
↑m 𝒫 𝑏) = (𝒫 3o
↑m 𝒫 3o)) |
| 65 | | pm4.61 404 |
. . . . . 6
⊢ (¬
(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ∧ ¬ 𝜓)) |
| 66 | | clsnim.k0 |
. . . . . . . . . 10
⊢ (𝜑 ↔ (𝑘‘∅) = ∅) |
| 67 | 66 | a1i 11 |
. . . . . . . . 9
⊢ (𝑏 = 3o → (𝜑 ↔ (𝑘‘∅) = ∅)) |
| 68 | | clsnim.k2 |
. . . . . . . . . 10
⊢ (𝜒 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑠 ⊆ (𝑘‘𝑠)) |
| 69 | 63 | raleqdv 3326 |
. . . . . . . . . 10
⊢ (𝑏 = 3o →
(∀𝑠 ∈ 𝒫
𝑏𝑠 ⊆ (𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘‘𝑠))) |
| 70 | 68, 69 | bitrid 283 |
. . . . . . . . 9
⊢ (𝑏 = 3o → (𝜒 ↔ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘‘𝑠))) |
| 71 | 67, 70 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑏 = 3o → ((𝜑 ∧ 𝜒) ↔ ((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)))) |
| 72 | | clsnim.k3 |
. . . . . . . . . 10
⊢ (𝜃 ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡))) |
| 73 | 63 | raleqdv 3326 |
. . . . . . . . . . 11
⊢ (𝑏 = 3o →
(∀𝑡 ∈ 𝒫
𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)))) |
| 74 | 63, 73 | raleqbidv 3346 |
. . . . . . . . . 10
⊢ (𝑏 = 3o →
(∀𝑠 ∈ 𝒫
𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)))) |
| 75 | 72, 74 | bitrid 283 |
. . . . . . . . 9
⊢ (𝑏 = 3o → (𝜃 ↔ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)))) |
| 76 | | clsnim.k4 |
. . . . . . . . . 10
⊢ (𝜏 ↔ ∀𝑠 ∈ 𝒫 𝑏(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠)) |
| 77 | 63 | raleqdv 3326 |
. . . . . . . . . 10
⊢ (𝑏 = 3o →
(∀𝑠 ∈ 𝒫
𝑏(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) |
| 78 | 76, 77 | bitrid 283 |
. . . . . . . . 9
⊢ (𝑏 = 3o → (𝜏 ↔ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) |
| 79 | 75, 78 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑏 = 3o → ((𝜃 ∧ 𝜏) ↔ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠)))) |
| 80 | 71, 79 | anbi12d 632 |
. . . . . . 7
⊢ (𝑏 = 3o → (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ↔ (((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))))) |
| 81 | | clsnim.k1 |
. . . . . . . . 9
⊢ (𝜓 ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
| 82 | 63 | raleqdv 3326 |
. . . . . . . . . 10
⊢ (𝑏 = 3o →
(∀𝑡 ∈ 𝒫
𝑏(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3o(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
| 83 | 63, 82 | raleqbidv 3346 |
. . . . . . . . 9
⊢ (𝑏 = 3o →
(∀𝑠 ∈ 𝒫
𝑏∀𝑡 ∈ 𝒫 𝑏(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
| 84 | 81, 83 | bitrid 283 |
. . . . . . . 8
⊢ (𝑏 = 3o → (𝜓 ↔ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
| 85 | 84 | notbid 318 |
. . . . . . 7
⊢ (𝑏 = 3o → (¬
𝜓 ↔ ¬ ∀𝑠 ∈ 𝒫
3o∀𝑡
∈ 𝒫 3o(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
| 86 | 80, 85 | anbi12d 632 |
. . . . . 6
⊢ (𝑏 = 3o →
((((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ∧ ¬ 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))))) |
| 87 | 65, 86 | bitrid 283 |
. . . . 5
⊢ (𝑏 = 3o → (¬
(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))))) |
| 88 | 64, 87 | rexeqbidv 3347 |
. . . 4
⊢ (𝑏 = 3o →
(∃𝑘 ∈ (𝒫
𝑏 ↑m
𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ∃𝑘 ∈ (𝒫 3o
↑m 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))))) |
| 89 | 88 | rspcev 3622 |
. . 3
⊢
((3o ∈ V ∧ ∃𝑘 ∈ (𝒫 3o
↑m 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) → ∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
| 90 | | rexnal2 3135 |
. . . 4
⊢
(∃𝑏 ∈ V
∃𝑘 ∈ (𝒫
𝑏 ↑m
𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ¬ ∀𝑏 ∈ V ∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
| 91 | | ralv 3508 |
. . . 4
⊢
(∀𝑏 ∈ V
∀𝑘 ∈ (𝒫
𝑏 ↑m
𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
| 92 | 90, 91 | xchbinx 334 |
. . 3
⊢
(∃𝑏 ∈ V
∃𝑘 ∈ (𝒫
𝑏 ↑m
𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
| 93 | 89, 92 | sylib 218 |
. 2
⊢
((3o ∈ V ∧ ∃𝑘 ∈ (𝒫 3o
↑m 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
| 94 | 2, 62, 93 | mp2an 692 |
1
⊢ ¬
∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑m 𝒫
𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) |