Step | Hyp | Ref
| Expression |
1 | | 3on 7570 |
. . 3
⊢
3𝑜 ∈ On |
2 | 1 | elexi 3213 |
. 2
⊢
3𝑜 ∈ V |
3 | | eqid 2622 |
. . . . 5
⊢ (𝑟 ∈ 𝒫
3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))
= (𝑟 ∈ 𝒫
3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)) |
4 | | notnotr 125 |
. . . . . . . . . . 11
⊢ (¬
¬ 𝑟 = {∅} →
𝑟 =
{∅}) |
5 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑟 ∈ 𝒫
3𝑜 → (¬ ¬ 𝑟 = {∅} → 𝑟 = {∅})) |
6 | | sssucid 5802 |
. . . . . . . . . . . . 13
⊢
2𝑜 ⊆ suc 2𝑜 |
7 | | 2on 7568 |
. . . . . . . . . . . . . . 15
⊢
2𝑜 ∈ On |
8 | 7 | elexi 3213 |
. . . . . . . . . . . . . 14
⊢
2𝑜 ∈ V |
9 | 8 | elpw 4164 |
. . . . . . . . . . . . 13
⊢
(2𝑜 ∈ 𝒫 suc 2𝑜 ↔
2𝑜 ⊆ suc 2𝑜) |
10 | 6, 9 | mpbir 221 |
. . . . . . . . . . . 12
⊢
2𝑜 ∈ 𝒫 suc
2𝑜 |
11 | | df2o3 7573 |
. . . . . . . . . . . 12
⊢
2𝑜 = {∅,
1𝑜} |
12 | | df-3o 7562 |
. . . . . . . . . . . . . 14
⊢
3𝑜 = suc 2𝑜 |
13 | 12 | eqcomi 2631 |
. . . . . . . . . . . . 13
⊢ suc
2𝑜 = 3𝑜 |
14 | 13 | pweqi 4162 |
. . . . . . . . . . . 12
⊢ 𝒫
suc 2𝑜 = 𝒫 3𝑜 |
15 | 10, 11, 14 | 3eltr3i 2713 |
. . . . . . . . . . 11
⊢ {∅,
1𝑜} ∈ 𝒫 3𝑜 |
16 | 15 | 2a1i 12 |
. . . . . . . . . 10
⊢ (𝑟 ∈ 𝒫
3𝑜 → (¬ ¬ 𝑟 = {∅} → {∅,
1𝑜} ∈ 𝒫
3𝑜)) |
17 | 5, 16 | jcad 555 |
. . . . . . . . 9
⊢ (𝑟 ∈ 𝒫
3𝑜 → (¬ ¬ 𝑟 = {∅} → (𝑟 = {∅} ∧ {∅,
1𝑜} ∈ 𝒫
3𝑜))) |
18 | 17 | con1d 139 |
. . . . . . . 8
⊢ (𝑟 ∈ 𝒫
3𝑜 → (¬ (𝑟 = {∅} ∧ {∅,
1𝑜} ∈ 𝒫 3𝑜) → ¬
𝑟 =
{∅})) |
19 | 18 | anc2ri 581 |
. . . . . . 7
⊢ (𝑟 ∈ 𝒫
3𝑜 → (¬ (𝑟 = {∅} ∧ {∅,
1𝑜} ∈ 𝒫 3𝑜) → (¬
𝑟 = {∅} ∧ 𝑟 ∈ 𝒫
3𝑜))) |
20 | 19 | orrd 393 |
. . . . . 6
⊢ (𝑟 ∈ 𝒫
3𝑜 → ((𝑟 = {∅} ∧ {∅,
1𝑜} ∈ 𝒫 3𝑜) ∨ (¬
𝑟 = {∅} ∧ 𝑟 ∈ 𝒫
3𝑜))) |
21 | | ifel 4129 |
. . . . . 6
⊢ (if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)
∈ 𝒫 3𝑜 ↔ ((𝑟 = {∅} ∧ {∅,
1𝑜} ∈ 𝒫 3𝑜) ∨ (¬
𝑟 = {∅} ∧ 𝑟 ∈ 𝒫
3𝑜))) |
22 | 20, 21 | sylibr 224 |
. . . . 5
⊢ (𝑟 ∈ 𝒫
3𝑜 → if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)
∈ 𝒫 3𝑜) |
23 | 3, 22 | fmpti 6383 |
. . . 4
⊢ (𝑟 ∈ 𝒫
3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)):𝒫
3𝑜⟶𝒫 3𝑜 |
24 | 2 | pwex 4848 |
. . . . 5
⊢ 𝒫
3𝑜 ∈ V |
25 | 24, 24 | elmap 7886 |
. . . 4
⊢ ((𝑟 ∈ 𝒫
3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))
∈ (𝒫 3𝑜 ↑𝑚 𝒫
3𝑜) ↔ (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)):𝒫
3𝑜⟶𝒫 3𝑜) |
26 | 23, 25 | mpbir 221 |
. . 3
⊢ (𝑟 ∈ 𝒫
3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))
∈ (𝒫 3𝑜 ↑𝑚 𝒫
3𝑜) |
27 | 3 | clsk1indlem0 38339 |
. . . . . 6
⊢ ((𝑟 ∈ 𝒫
3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘∅) = ∅ |
28 | 3 | clsk1indlem2 38340 |
. . . . . 6
⊢
∀𝑠 ∈
𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) |
29 | 27, 28 | pm3.2i 471 |
. . . . 5
⊢ (((𝑟 ∈ 𝒫
3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ ((𝑟 ∈
𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘𝑠)) |
30 | 3 | clsk1indlem3 38341 |
. . . . . 6
⊢
∀𝑠 ∈
𝒫 3𝑜∀𝑡 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)) |
31 | 3 | clsk1indlem4 38342 |
. . . . . 6
⊢
∀𝑠 ∈
𝒫 3𝑜((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) |
32 | 30, 31 | pm3.2i 471 |
. . . . 5
⊢
(∀𝑠 ∈
𝒫 3𝑜∀𝑡 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) |
33 | 29, 32 | pm3.2i 471 |
. . . 4
⊢ ((((𝑟 ∈ 𝒫
3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ ((𝑟 ∈
𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠))) |
34 | 3 | clsk1indlem1 38343 |
. . . 4
⊢
∃𝑠 ∈
𝒫 3𝑜∃𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)) |
35 | 33, 34 | pm3.2i 471 |
. . 3
⊢
(((((𝑟 ∈
𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ ((𝑟 ∈
𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠))) ∧ ∃𝑠 ∈ 𝒫
3𝑜∃𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡))) |
36 | | fveq1 6190 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (𝑘‘∅) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘∅)) |
37 | 36 | eqeq1d 2624 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → ((𝑘‘∅) = ∅ ↔ ((𝑟 ∈ 𝒫
3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘∅) =
∅)) |
38 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (𝑘‘𝑠) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) |
39 | 38 | sseq2d 3633 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (𝑠 ⊆ (𝑘‘𝑠) ↔ 𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠))) |
40 | 39 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠))) |
41 | 37, 40 | anbi12d 747 |
. . . . . 6
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ↔ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ ((𝑟 ∈
𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘𝑠)))) |
42 | | fveq1 6190 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (𝑘‘(𝑠 ∪ 𝑡)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡))) |
43 | | fveq1 6190 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (𝑘‘𝑡) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)) |
44 | 38, 43 | uneq12d 3768 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡))) |
45 | 42, 44 | sseq12d 3634 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → ((𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)))) |
46 | 45 | 2ralbidv 2989 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)))) |
47 | | id 22 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → 𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))) |
48 | 47, 38 | fveq12d 6197 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (𝑘‘(𝑘‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠))) |
49 | 48, 38 | eqeq12d 2637 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → ((𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠) ↔ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠))) |
50 | 49 | ralbidv 2986 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠))) |
51 | 46, 50 | anbi12d 747 |
. . . . . 6
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → ((∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠)) ↔ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)))) |
52 | 41, 51 | anbi12d 747 |
. . . . 5
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ↔ ((((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ ((𝑟 ∈
𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠))))) |
53 | | rexnal2 3043 |
. . . . . 6
⊢
(∃𝑠 ∈
𝒫 3𝑜∃𝑡 ∈ 𝒫 3𝑜 ¬
(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ¬ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
54 | | pm4.61 442 |
. . . . . . . 8
⊢ (¬
(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ (𝑠 ⊆ 𝑡 ∧ ¬ (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
55 | 38, 43 | sseq12d 3634 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → ((𝑘‘𝑠) ⊆ (𝑘‘𝑡) ↔ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡))) |
56 | 55 | notbid 308 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (¬ (𝑘‘𝑠) ⊆ (𝑘‘𝑡) ↔ ¬ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡))) |
57 | 56 | anbi2d 740 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → ((𝑠 ⊆ 𝑡 ∧ ¬ (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ (𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)))) |
58 | 54, 57 | syl5bb 272 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (¬ (𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ (𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)))) |
59 | 58 | 2rexbidv 3057 |
. . . . . 6
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (∃𝑠 ∈ 𝒫
3𝑜∃𝑡 ∈ 𝒫 3𝑜 ¬
(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∃𝑠 ∈ 𝒫
3𝑜∃𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)))) |
60 | 53, 59 | syl5bbr 274 |
. . . . 5
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (¬ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∃𝑠 ∈ 𝒫
3𝑜∃𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)))) |
61 | 52, 60 | anbi12d 747 |
. . . 4
⊢ (𝑘 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) → (((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) ↔ (((((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ ((𝑟 ∈
𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠))) ∧ ∃𝑠 ∈ 𝒫
3𝑜∃𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡))))) |
62 | 61 | rspcev 3309 |
. . 3
⊢ (((𝑟 ∈ 𝒫
3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))
∈ (𝒫 3𝑜 ↑𝑚 𝒫
3𝑜) ∧ (((((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ ((𝑟 ∈
𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫
3𝑜((𝑟
∈ 𝒫 3𝑜 ↦ if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟))‘((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠))) ∧ ∃𝑠 ∈ 𝒫
3𝑜∃𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟))‘𝑡)))) → ∃𝑘 ∈ (𝒫 3𝑜
↑𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
63 | 26, 35, 62 | mp2an 708 |
. 2
⊢
∃𝑘 ∈
(𝒫 3𝑜 ↑𝑚 𝒫
3𝑜)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
64 | | pweq 4161 |
. . . . . 6
⊢ (𝑏 = 3𝑜 →
𝒫 𝑏 = 𝒫
3𝑜) |
65 | 64, 64 | oveq12d 6668 |
. . . . 5
⊢ (𝑏 = 3𝑜 →
(𝒫 𝑏
↑𝑚 𝒫 𝑏) = (𝒫 3𝑜
↑𝑚 𝒫 3𝑜)) |
66 | | pm4.61 442 |
. . . . . 6
⊢ (¬
(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ∧ ¬ 𝜓)) |
67 | | clsnim.k0 |
. . . . . . . . . 10
⊢ (𝜑 ↔ (𝑘‘∅) = ∅) |
68 | 67 | a1i 11 |
. . . . . . . . 9
⊢ (𝑏 = 3𝑜 →
(𝜑 ↔ (𝑘‘∅) = ∅)) |
69 | | clsnim.k2 |
. . . . . . . . . 10
⊢ (𝜒 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑠 ⊆ (𝑘‘𝑠)) |
70 | 64 | raleqdv 3144 |
. . . . . . . . . 10
⊢ (𝑏 = 3𝑜 →
(∀𝑠 ∈ 𝒫
𝑏𝑠 ⊆ (𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜𝑠 ⊆ (𝑘‘𝑠))) |
71 | 69, 70 | syl5bb 272 |
. . . . . . . . 9
⊢ (𝑏 = 3𝑜 →
(𝜒 ↔ ∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠))) |
72 | 68, 71 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑏 = 3𝑜 →
((𝜑 ∧ 𝜒) ↔ ((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)))) |
73 | | clsnim.k3 |
. . . . . . . . . 10
⊢ (𝜃 ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡))) |
74 | 64 | raleqdv 3144 |
. . . . . . . . . . 11
⊢ (𝑏 = 3𝑜 →
(∀𝑡 ∈ 𝒫
𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)))) |
75 | 64, 74 | raleqbidv 3152 |
. . . . . . . . . 10
⊢ (𝑏 = 3𝑜 →
(∀𝑠 ∈ 𝒫
𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)))) |
76 | 73, 75 | syl5bb 272 |
. . . . . . . . 9
⊢ (𝑏 = 3𝑜 →
(𝜃 ↔ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)))) |
77 | | clsnim.k4 |
. . . . . . . . . 10
⊢ (𝜏 ↔ ∀𝑠 ∈ 𝒫 𝑏(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠)) |
78 | 64 | raleqdv 3144 |
. . . . . . . . . 10
⊢ (𝑏 = 3𝑜 →
(∀𝑠 ∈ 𝒫
𝑏(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) |
79 | 77, 78 | syl5bb 272 |
. . . . . . . . 9
⊢ (𝑏 = 3𝑜 →
(𝜏 ↔ ∀𝑠 ∈ 𝒫
3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) |
80 | 76, 79 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑏 = 3𝑜 →
((𝜃 ∧ 𝜏) ↔ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠)))) |
81 | 72, 80 | anbi12d 747 |
. . . . . . 7
⊢ (𝑏 = 3𝑜 →
(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ↔ (((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))))) |
82 | | clsnim.k1 |
. . . . . . . . 9
⊢ (𝜓 ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
83 | 64 | raleqdv 3144 |
. . . . . . . . . 10
⊢ (𝑏 = 3𝑜 →
(∀𝑡 ∈ 𝒫
𝑏(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
84 | 64, 83 | raleqbidv 3152 |
. . . . . . . . 9
⊢ (𝑏 = 3𝑜 →
(∀𝑠 ∈ 𝒫
𝑏∀𝑡 ∈ 𝒫 𝑏(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
85 | 82, 84 | syl5bb 272 |
. . . . . . . 8
⊢ (𝑏 = 3𝑜 →
(𝜓 ↔ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
86 | 85 | notbid 308 |
. . . . . . 7
⊢ (𝑏 = 3𝑜 →
(¬ 𝜓 ↔ ¬
∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
87 | 81, 86 | anbi12d 747 |
. . . . . 6
⊢ (𝑏 = 3𝑜 →
((((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ∧ ¬ 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))))) |
88 | 66, 87 | syl5bb 272 |
. . . . 5
⊢ (𝑏 = 3𝑜 →
(¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))))) |
89 | 65, 88 | rexeqbidv 3153 |
. . . 4
⊢ (𝑏 = 3𝑜 →
(∃𝑘 ∈ (𝒫
𝑏
↑𝑚 𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ∃𝑘 ∈ (𝒫 3𝑜
↑𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))))) |
90 | 89 | rspcev 3309 |
. . 3
⊢
((3𝑜 ∈ V ∧ ∃𝑘 ∈ (𝒫 3𝑜
↑𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) → ∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
91 | | rexnal2 3043 |
. . . 4
⊢
(∃𝑏 ∈ V
∃𝑘 ∈ (𝒫
𝑏
↑𝑚 𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ¬ ∀𝑏 ∈ V ∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
92 | | ralv 3219 |
. . . 4
⊢
(∀𝑏 ∈ V
∀𝑘 ∈ (𝒫
𝑏
↑𝑚 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
93 | 91, 92 | xchbinx 324 |
. . 3
⊢
(∃𝑏 ∈ V
∃𝑘 ∈ (𝒫
𝑏
↑𝑚 𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
94 | 90, 93 | sylib 208 |
. 2
⊢
((3𝑜 ∈ V ∧ ∃𝑘 ∈ (𝒫 3𝑜
↑𝑚 𝒫 3𝑜)((((𝑘‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3𝑜𝑠
⊆ (𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3𝑜(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫
3𝑜∀𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
95 | 2, 63, 94 | mp2an 708 |
1
⊢ ¬
∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) |