Step | Hyp | Ref
| Expression |
1 | | 3on 7842 |
. . 3
⊢
3o ∈ On |
2 | 1 | elexi 3430 |
. 2
⊢
3o ∈ V |
3 | | eqid 2825 |
. . . . 5
⊢ (𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟)) = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) |
4 | | notnotr 128 |
. . . . . . . . . . 11
⊢ (¬
¬ 𝑟 = {∅} →
𝑟 =
{∅}) |
5 | 4 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑟 ∈ 𝒫 3o
→ (¬ ¬ 𝑟 =
{∅} → 𝑟 =
{∅})) |
6 | | sssucid 6044 |
. . . . . . . . . . . . 13
⊢
2o ⊆ suc 2o |
7 | | 2on 7840 |
. . . . . . . . . . . . . . 15
⊢
2o ∈ On |
8 | 7 | elexi 3430 |
. . . . . . . . . . . . . 14
⊢
2o ∈ V |
9 | 8 | elpw 4386 |
. . . . . . . . . . . . 13
⊢
(2o ∈ 𝒫 suc 2o ↔ 2o
⊆ suc 2o) |
10 | 6, 9 | mpbir 223 |
. . . . . . . . . . . 12
⊢
2o ∈ 𝒫 suc 2o |
11 | | df2o3 7845 |
. . . . . . . . . . . 12
⊢
2o = {∅, 1o} |
12 | | df-3o 7833 |
. . . . . . . . . . . . . 14
⊢
3o = suc 2o |
13 | 12 | eqcomi 2834 |
. . . . . . . . . . . . 13
⊢ suc
2o = 3o |
14 | 13 | pweqi 4384 |
. . . . . . . . . . . 12
⊢ 𝒫
suc 2o = 𝒫 3o |
15 | 10, 11, 14 | 3eltr3i 2918 |
. . . . . . . . . . 11
⊢ {∅,
1o} ∈ 𝒫 3o |
16 | 15 | 2a1i 12 |
. . . . . . . . . 10
⊢ (𝑟 ∈ 𝒫 3o
→ (¬ ¬ 𝑟 =
{∅} → {∅, 1o} ∈ 𝒫
3o)) |
17 | 5, 16 | jcad 508 |
. . . . . . . . 9
⊢ (𝑟 ∈ 𝒫 3o
→ (¬ ¬ 𝑟 =
{∅} → (𝑟 =
{∅} ∧ {∅, 1o} ∈ 𝒫
3o))) |
18 | 17 | con1d 142 |
. . . . . . . 8
⊢ (𝑟 ∈ 𝒫 3o
→ (¬ (𝑟 =
{∅} ∧ {∅, 1o} ∈ 𝒫 3o) →
¬ 𝑟 =
{∅})) |
19 | 18 | anc2ri 552 |
. . . . . . 7
⊢ (𝑟 ∈ 𝒫 3o
→ (¬ (𝑟 =
{∅} ∧ {∅, 1o} ∈ 𝒫 3o) →
(¬ 𝑟 = {∅} ∧
𝑟 ∈ 𝒫
3o))) |
20 | 19 | orrd 894 |
. . . . . 6
⊢ (𝑟 ∈ 𝒫 3o
→ ((𝑟 = {∅}
∧ {∅, 1o} ∈ 𝒫 3o) ∨ (¬
𝑟 = {∅} ∧ 𝑟 ∈ 𝒫
3o))) |
21 | | ifel 4351 |
. . . . . 6
⊢ (if(𝑟 = {∅}, {∅,
1o}, 𝑟) ∈
𝒫 3o ↔ ((𝑟 = {∅} ∧ {∅, 1o}
∈ 𝒫 3o) ∨ (¬ 𝑟 = {∅} ∧ 𝑟 ∈ 𝒫
3o))) |
22 | 20, 21 | sylibr 226 |
. . . . 5
⊢ (𝑟 ∈ 𝒫 3o
→ if(𝑟 = {∅},
{∅, 1o}, 𝑟) ∈ 𝒫
3o) |
23 | 3, 22 | fmpti 6636 |
. . . 4
⊢ (𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟)):𝒫 3o⟶𝒫
3o |
24 | 2 | pwex 5082 |
. . . . 5
⊢ 𝒫
3o ∈ V |
25 | 24, 24 | elmap 8156 |
. . . 4
⊢ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟)) ∈ (𝒫 3o
↑𝑚 𝒫 3o) ↔ (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)):𝒫 3o⟶𝒫
3o) |
26 | 23, 25 | mpbir 223 |
. . 3
⊢ (𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟)) ∈ (𝒫 3o
↑𝑚 𝒫 3o) |
27 | 3 | clsk1indlem0 39174 |
. . . . . 6
⊢ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘∅) = ∅ |
28 | 3 | clsk1indlem2 39175 |
. . . . . 6
⊢
∀𝑠 ∈
𝒫 3o𝑠
⊆ ((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘𝑠) |
29 | 27, 28 | pm3.2i 464 |
. . . . 5
⊢ (((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3o𝑠 ⊆
((𝑟 ∈ 𝒫
3o ↦ if(𝑟
= {∅}, {∅, 1o}, 𝑟))‘𝑠)) |
30 | 3 | clsk1indlem3 39176 |
. . . . . 6
⊢
∀𝑠 ∈
𝒫 3o∀𝑡 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) |
31 | 3 | clsk1indlem4 39177 |
. . . . . 6
⊢
∀𝑠 ∈
𝒫 3o((𝑟
∈ 𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) |
32 | 30, 31 | pm3.2i 464 |
. . . . 5
⊢
(∀𝑠 ∈
𝒫 3o∀𝑡 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) |
33 | 29, 32 | pm3.2i 464 |
. . . 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}, 𝑟))‘𝑠))) |
34 | 3 | clsk1indlem1 39178 |
. . . 4
⊢
∃𝑠 ∈
𝒫 3o∃𝑡 ∈ 𝒫 3o(𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) |
35 | 33, 34 | pm3.2i 464 |
. . 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}, 𝑟))‘𝑡))) |
36 | | fveq1 6436 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑘‘∅) = ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘∅)) |
37 | 36 | eqeq1d 2827 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑘‘∅) =
∅ ↔ ((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘∅) =
∅)) |
38 | | fveq1 6436 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑘‘𝑠) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) |
39 | 38 | sseq2d 3858 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑠 ⊆ (𝑘‘𝑠) ↔ 𝑠 ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
40 | 39 | ralbidv 3195 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
41 | 37, 40 | anbi12d 624 |
. . . . . 6
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(((𝑘‘∅) =
∅ ∧ ∀𝑠
∈ 𝒫 3o𝑠 ⊆ (𝑘‘𝑠)) ↔ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘∅) = ∅ ∧
∀𝑠 ∈ 𝒫
3o𝑠 ⊆
((𝑟 ∈ 𝒫
3o ↦ if(𝑟
= {∅}, {∅, 1o}, 𝑟))‘𝑠)))) |
42 | | fveq1 6436 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑘‘(𝑠 ∪ 𝑡)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘(𝑠 ∪ 𝑡))) |
43 | | fveq1 6436 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑘‘𝑡) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)) |
44 | 38, 43 | uneq12d 3997 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑘‘𝑠) ∪ (𝑘‘𝑡)) = (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡))) |
45 | 42, 44 | sseq12d 3859 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
46 | 45 | 2ralbidv 3198 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(∀𝑠 ∈ 𝒫
3o∀𝑡
∈ 𝒫 3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o((𝑟 ∈
𝒫 3o ↦ if(𝑟 = {∅}, {∅, 1o}, 𝑟))‘(𝑠 ∪ 𝑡)) ⊆ (((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ∪ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
47 | | id 22 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))) |
48 | 47, 38 | fveq12d 6444 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(𝑘‘(𝑘‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
49 | 48, 38 | eqeq12d 2840 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠) ↔ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
50 | 49 | ralbidv 3195 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(∀𝑠 ∈ 𝒫
3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠)) = ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠))) |
51 | 46, 50 | anbi12d 624 |
. . . . . 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}, 𝑟))‘𝑠)))) |
52 | 41, 51 | anbi12d 624 |
. . . . 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}, 𝑟))‘𝑠))))) |
53 | | rexnal2 3253 |
. . . . . 6
⊢
(∃𝑠 ∈
𝒫 3o∃𝑡 ∈ 𝒫 3o ¬ (𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
54 | | pm4.61 395 |
. . . . . . . 8
⊢ (¬
(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ (𝑠 ⊆ 𝑡 ∧ ¬ (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
55 | 38, 43 | sseq12d 3859 |
. . . . . . . . . 10
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑘‘𝑠) ⊆ (𝑘‘𝑡) ↔ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡))) |
56 | 55 | notbid 310 |
. . . . . . . . 9
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(¬ (𝑘‘𝑠) ⊆ (𝑘‘𝑡) ↔ ¬ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡))) |
57 | 56 | anbi2d 622 |
. . . . . . . 8
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
((𝑠 ⊆ 𝑡 ∧ ¬ (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ (𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
58 | 54, 57 | syl5bb 275 |
. . . . . . 7
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(¬ (𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ (𝑠 ⊆ 𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
59 | 58 | 2rexbidv 3267 |
. . . . . 6
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(∃𝑠 ∈ 𝒫
3o∃𝑡
∈ 𝒫 3o ¬ (𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∃𝑠 ∈ 𝒫 3o∃𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
60 | 53, 59 | syl5bbr 277 |
. . . . 5
⊢ (𝑘 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) →
(¬ ∀𝑠 ∈
𝒫 3o∀𝑡 ∈ 𝒫 3o(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∃𝑠 ∈ 𝒫 3o∃𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 ∧ ¬ ((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟))‘𝑠) ⊆ ((𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟))‘𝑡)))) |
61 | 52, 60 | anbi12d 624 |
. . . 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}, 𝑟))‘𝑡))))) |
62 | 61 | rspcev 3526 |
. . 3
⊢ (((𝑟 ∈ 𝒫 3o
↦ if(𝑟 = {∅},
{∅, 1o}, 𝑟)) ∈ (𝒫 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}, 𝑟))‘𝑡)))) → ∃𝑘 ∈ (𝒫 3o
↑𝑚 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
63 | 26, 35, 62 | mp2an 683 |
. 2
⊢
∃𝑘 ∈
(𝒫 3o ↑𝑚 𝒫
3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
64 | | pweq 4383 |
. . . . . 6
⊢ (𝑏 = 3o →
𝒫 𝑏 = 𝒫
3o) |
65 | 64, 64 | oveq12d 6928 |
. . . . 5
⊢ (𝑏 = 3o →
(𝒫 𝑏
↑𝑚 𝒫 𝑏) = (𝒫 3o
↑𝑚 𝒫 3o)) |
66 | | pm4.61 395 |
. . . . . 6
⊢ (¬
(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ∧ ¬ 𝜓)) |
67 | | clsnim.k0 |
. . . . . . . . . 10
⊢ (𝜑 ↔ (𝑘‘∅) = ∅) |
68 | 67 | a1i 11 |
. . . . . . . . 9
⊢ (𝑏 = 3o → (𝜑 ↔ (𝑘‘∅) = ∅)) |
69 | | clsnim.k2 |
. . . . . . . . . 10
⊢ (𝜒 ↔ ∀𝑠 ∈ 𝒫 𝑏𝑠 ⊆ (𝑘‘𝑠)) |
70 | 64 | raleqdv 3356 |
. . . . . . . . . 10
⊢ (𝑏 = 3o →
(∀𝑠 ∈ 𝒫
𝑏𝑠 ⊆ (𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘‘𝑠))) |
71 | 69, 70 | syl5bb 275 |
. . . . . . . . 9
⊢ (𝑏 = 3o → (𝜒 ↔ ∀𝑠 ∈ 𝒫 3o𝑠 ⊆ (𝑘‘𝑠))) |
72 | 68, 71 | anbi12d 624 |
. . . . . . . 8
⊢ (𝑏 = 3o → ((𝜑 ∧ 𝜒) ↔ ((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)))) |
73 | | clsnim.k3 |
. . . . . . . . . 10
⊢ (𝜃 ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡))) |
74 | 64 | raleqdv 3356 |
. . . . . . . . . . 11
⊢ (𝑏 = 3o →
(∀𝑡 ∈ 𝒫
𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)))) |
75 | 64, 74 | raleqbidv 3364 |
. . . . . . . . . 10
⊢ (𝑏 = 3o →
(∀𝑠 ∈ 𝒫
𝑏∀𝑡 ∈ 𝒫 𝑏(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)))) |
76 | 73, 75 | syl5bb 275 |
. . . . . . . . 9
⊢ (𝑏 = 3o → (𝜃 ↔ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)))) |
77 | | clsnim.k4 |
. . . . . . . . . 10
⊢ (𝜏 ↔ ∀𝑠 ∈ 𝒫 𝑏(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠)) |
78 | 64 | raleqdv 3356 |
. . . . . . . . . 10
⊢ (𝑏 = 3o →
(∀𝑠 ∈ 𝒫
𝑏(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠) ↔ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) |
79 | 77, 78 | syl5bb 275 |
. . . . . . . . 9
⊢ (𝑏 = 3o → (𝜏 ↔ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) |
80 | 76, 79 | anbi12d 624 |
. . . . . . . 8
⊢ (𝑏 = 3o → ((𝜃 ∧ 𝜏) ↔ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠)))) |
81 | 72, 80 | anbi12d 624 |
. . . . . . 7
⊢ (𝑏 = 3o → (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ↔ (((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))))) |
82 | | clsnim.k1 |
. . . . . . . . 9
⊢ (𝜓 ↔ ∀𝑠 ∈ 𝒫 𝑏∀𝑡 ∈ 𝒫 𝑏(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))) |
83 | 64 | raleqdv 3356 |
. . . . . . . . . 10
⊢ (𝑏 = 3o →
(∀𝑡 ∈ 𝒫
𝑏(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∀𝑡 ∈ 𝒫 3o(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
84 | 64, 83 | raleqbidv 3364 |
. . . . . . . . 9
⊢ (𝑏 = 3o →
(∀𝑠 ∈ 𝒫
𝑏∀𝑡 ∈ 𝒫 𝑏(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)) ↔ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
85 | 82, 84 | syl5bb 275 |
. . . . . . . 8
⊢ (𝑏 = 3o → (𝜓 ↔ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
86 | 85 | notbid 310 |
. . . . . . 7
⊢ (𝑏 = 3o → (¬
𝜓 ↔ ¬ ∀𝑠 ∈ 𝒫
3o∀𝑡
∈ 𝒫 3o(𝑠 ⊆ 𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) |
87 | 81, 86 | anbi12d 624 |
. . . . . 6
⊢ (𝑏 = 3o →
((((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) ∧ ¬ 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))))) |
88 | 66, 87 | syl5bb 275 |
. . . . 5
⊢ (𝑏 = 3o → (¬
(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))))) |
89 | 65, 88 | rexeqbidv 3365 |
. . . 4
⊢ (𝑏 = 3o →
(∃𝑘 ∈ (𝒫
𝑏
↑𝑚 𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ∃𝑘 ∈ (𝒫 3o
↑𝑚 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡))))) |
90 | 89 | rspcev 3526 |
. . 3
⊢
((3o ∈ V ∧ ∃𝑘 ∈ (𝒫 3o
↑𝑚 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) → ∃𝑏 ∈ V ∃𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
91 | | rexnal2 3253 |
. . . 4
⊢
(∃𝑏 ∈ V
∃𝑘 ∈ (𝒫
𝑏
↑𝑚 𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ¬ ∀𝑏 ∈ V ∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
92 | | ralv 3436 |
. . . 4
⊢
(∀𝑏 ∈ V
∀𝑘 ∈ (𝒫
𝑏
↑𝑚 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
93 | 91, 92 | xchbinx 326 |
. . 3
⊢
(∃𝑏 ∈ V
∃𝑘 ∈ (𝒫
𝑏
↑𝑚 𝒫 𝑏) ¬ (((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) ↔ ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
94 | 90, 93 | sylib 210 |
. 2
⊢
((3o ∈ V ∧ ∃𝑘 ∈ (𝒫 3o
↑𝑚 𝒫 3o)((((𝑘‘∅) = ∅ ∧ ∀𝑠 ∈ 𝒫
3o𝑠 ⊆
(𝑘‘𝑠)) ∧ (∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑘‘(𝑠 ∪ 𝑡)) ⊆ ((𝑘‘𝑠) ∪ (𝑘‘𝑡)) ∧ ∀𝑠 ∈ 𝒫 3o(𝑘‘(𝑘‘𝑠)) = (𝑘‘𝑠))) ∧ ¬ ∀𝑠 ∈ 𝒫 3o∀𝑡 ∈ 𝒫
3o(𝑠 ⊆
𝑡 → (𝑘‘𝑠) ⊆ (𝑘‘𝑡)))) → ¬ ∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚 𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓)) |
95 | 2, 63, 94 | mp2an 683 |
1
⊢ ¬
∀𝑏∀𝑘 ∈ (𝒫 𝑏 ↑𝑚
𝒫 𝑏)(((𝜑 ∧ 𝜒) ∧ (𝜃 ∧ 𝜏)) → 𝜓) |