Proof of Theorem clsk1indlem4
Step | Hyp | Ref
| Expression |
1 | | tpex 7617 |
. . . . . . . . . 10
⊢ {∅,
1o, 2o} ∈ V |
2 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ {∅, 1o, 2o} ∈ V) |
3 | | snsstp1 4752 |
. . . . . . . . . . . 12
⊢ {∅}
⊆ {∅, 1o, 2o} |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ {∅} ⊆ {∅, 1o,
2o}) |
5 | | 0ex 5234 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
6 | 5 | snss 4722 |
. . . . . . . . . . 11
⊢ (∅
∈ {∅, 1o, 2o} ↔ {∅} ⊆
{∅, 1o, 2o}) |
7 | 4, 6 | sylibr 233 |
. . . . . . . . . 10
⊢ (⊤
→ ∅ ∈ {∅, 1o, 2o}) |
8 | | snsstp2 4753 |
. . . . . . . . . . . 12
⊢
{1o} ⊆ {∅, 1o,
2o} |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ {1o} ⊆ {∅, 1o,
2o}) |
10 | | 1oex 8327 |
. . . . . . . . . . . 12
⊢
1o ∈ V |
11 | 10 | snss 4722 |
. . . . . . . . . . 11
⊢
(1o ∈ {∅, 1o, 2o} ↔
{1o} ⊆ {∅, 1o,
2o}) |
12 | 9, 11 | sylibr 233 |
. . . . . . . . . 10
⊢ (⊤
→ 1o ∈ {∅, 1o,
2o}) |
13 | 7, 12 | prssd 4758 |
. . . . . . . . 9
⊢ (⊤
→ {∅, 1o} ⊆ {∅, 1o,
2o}) |
14 | 2, 13 | sselpwd 5253 |
. . . . . . . 8
⊢ (⊤
→ {∅, 1o} ∈ 𝒫 {∅, 1o,
2o}) |
15 | 14 | mptru 1544 |
. . . . . . 7
⊢ {∅,
1o} ∈ 𝒫 {∅, 1o,
2o} |
16 | | df3o2 41658 |
. . . . . . . 8
⊢
3o = {∅, 1o, 2o} |
17 | 16 | pweqi 4554 |
. . . . . . 7
⊢ 𝒫
3o = 𝒫 {∅, 1o,
2o} |
18 | 15, 17 | eleqtrri 2833 |
. . . . . 6
⊢ {∅,
1o} ∈ 𝒫 3o |
19 | 18 | a1i 11 |
. . . . 5
⊢ (𝑠 ∈ 𝒫 3o
→ {∅, 1o} ∈ 𝒫
3o) |
20 | | id 22 |
. . . . 5
⊢ (𝑠 ∈ 𝒫 3o
→ 𝑠 ∈ 𝒫
3o) |
21 | 19, 20 | ifcld 4508 |
. . . 4
⊢ (𝑠 ∈ 𝒫 3o
→ if(𝑠 = {∅},
{∅, 1o}, 𝑠) ∈ 𝒫
3o) |
22 | | eqeq1 2737 |
. . . . . . . 8
⊢ (𝑟 = if(𝑠 = {∅}, {∅, 1o}, 𝑠) → (𝑟 = {∅} ↔ if(𝑠 = {∅}, {∅, 1o}, 𝑠) = {∅})) |
23 | | eqcom 2740 |
. . . . . . . . 9
⊢ (if(𝑠 = {∅}, {∅,
1o}, 𝑠) =
{∅} ↔ {∅} = if(𝑠 = {∅}, {∅, 1o}, 𝑠)) |
24 | | eqif 4503 |
. . . . . . . . 9
⊢
({∅} = if(𝑠 =
{∅}, {∅, 1o}, 𝑠) ↔ ((𝑠 = {∅} ∧ {∅} = {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ {∅} = 𝑠))) |
25 | 23, 24 | bitri 274 |
. . . . . . . 8
⊢ (if(𝑠 = {∅}, {∅,
1o}, 𝑠) =
{∅} ↔ ((𝑠 =
{∅} ∧ {∅} = {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ {∅} =
𝑠))) |
26 | 22, 25 | bitrdi 286 |
. . . . . . 7
⊢ (𝑟 = if(𝑠 = {∅}, {∅, 1o}, 𝑠) → (𝑟 = {∅} ↔ ((𝑠 = {∅} ∧ {∅} = {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ {∅} = 𝑠)))) |
27 | | id 22 |
. . . . . . 7
⊢ (𝑟 = if(𝑠 = {∅}, {∅, 1o}, 𝑠) → 𝑟 = if(𝑠 = {∅}, {∅, 1o}, 𝑠)) |
28 | 26, 27 | ifbieq2d 4488 |
. . . . . 6
⊢ (𝑟 = if(𝑠 = {∅}, {∅, 1o}, 𝑠) → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if(((𝑠 = {∅} ∧ {∅} = {∅,
1o}) ∨ (¬ 𝑠 = {∅} ∧ {∅} = 𝑠)), {∅, 1o},
if(𝑠 = {∅}, {∅,
1o}, 𝑠))) |
29 | | 1n0 8338 |
. . . . . . . . . 10
⊢
1o ≠ ∅ |
30 | | dfsn2 4577 |
. . . . . . . . . . . 12
⊢ {∅}
= {∅, ∅} |
31 | 30 | eqeq1i 2738 |
. . . . . . . . . . 11
⊢
({∅} = {∅, 1o} ↔ {∅, ∅} =
{∅, 1o}) |
32 | 5 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ∅ ∈ V) |
33 | | 1on 8329 |
. . . . . . . . . . . . . 14
⊢
1o ∈ On |
34 | 33 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 1o ∈ On) |
35 | 32, 34 | preq2b 4781 |
. . . . . . . . . . . 12
⊢ (⊤
→ ({∅, ∅} = {∅, 1o} ↔ ∅ =
1o)) |
36 | 35 | mptru 1544 |
. . . . . . . . . . 11
⊢
({∅, ∅} = {∅, 1o} ↔ ∅ =
1o) |
37 | | eqcom 2740 |
. . . . . . . . . . 11
⊢ (∅
= 1o ↔ 1o = ∅) |
38 | 31, 36, 37 | 3bitri 296 |
. . . . . . . . . 10
⊢
({∅} = {∅, 1o} ↔ 1o =
∅) |
39 | 29, 38 | nemtbir 3035 |
. . . . . . . . 9
⊢ ¬
{∅} = {∅, 1o} |
40 | 39 | intnan 486 |
. . . . . . . 8
⊢ ¬
(𝑠 = {∅} ∧
{∅} = {∅, 1o}) |
41 | | pm3.24 402 |
. . . . . . . . 9
⊢ ¬
(𝑠 = {∅} ∧ ¬
𝑠 =
{∅}) |
42 | | eqcom 2740 |
. . . . . . . . . 10
⊢ (𝑠 = {∅} ↔ {∅} =
𝑠) |
43 | 42 | anbi2ci 624 |
. . . . . . . . 9
⊢ ((𝑠 = {∅} ∧ ¬ 𝑠 = {∅}) ↔ (¬
𝑠 = {∅} ∧
{∅} = 𝑠)) |
44 | 41, 43 | mtbi 321 |
. . . . . . . 8
⊢ ¬
(¬ 𝑠 = {∅} ∧
{∅} = 𝑠) |
45 | 40, 44 | pm3.2ni 877 |
. . . . . . 7
⊢ ¬
((𝑠 = {∅} ∧
{∅} = {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ {∅} = 𝑠)) |
46 | 45 | iffalsei 4472 |
. . . . . 6
⊢
if(((𝑠 = {∅}
∧ {∅} = {∅, 1o}) ∨ (¬ 𝑠 = {∅} ∧ {∅} = 𝑠)), {∅, 1o},
if(𝑠 = {∅}, {∅,
1o}, 𝑠)) =
if(𝑠 = {∅}, {∅,
1o}, 𝑠) |
47 | 28, 46 | eqtrdi 2789 |
. . . . 5
⊢ (𝑟 = if(𝑠 = {∅}, {∅, 1o}, 𝑠) → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if(𝑠 = {∅}, {∅, 1o}, 𝑠)) |
48 | | clsk1indlem.k |
. . . . 5
⊢ 𝐾 = (𝑟 ∈ 𝒫 3o ↦
if(𝑟 = {∅}, {∅,
1o}, 𝑟)) |
49 | | prex 5358 |
. . . . . 6
⊢ {∅,
1o} ∈ V |
50 | | vex 3438 |
. . . . . 6
⊢ 𝑠 ∈ V |
51 | 49, 50 | ifex 4512 |
. . . . 5
⊢ if(𝑠 = {∅}, {∅,
1o}, 𝑠) ∈
V |
52 | 47, 48, 51 | fvmpt 6895 |
. . . 4
⊢ (if(𝑠 = {∅}, {∅,
1o}, 𝑠) ∈
𝒫 3o → (𝐾‘if(𝑠 = {∅}, {∅, 1o}, 𝑠)) = if(𝑠 = {∅}, {∅, 1o}, 𝑠)) |
53 | 21, 52 | syl 17 |
. . 3
⊢ (𝑠 ∈ 𝒫 3o
→ (𝐾‘if(𝑠 = {∅}, {∅,
1o}, 𝑠)) =
if(𝑠 = {∅}, {∅,
1o}, 𝑠)) |
54 | | eqeq1 2737 |
. . . . . 6
⊢ (𝑟 = 𝑠 → (𝑟 = {∅} ↔ 𝑠 = {∅})) |
55 | | id 22 |
. . . . . 6
⊢ (𝑟 = 𝑠 → 𝑟 = 𝑠) |
56 | 54, 55 | ifbieq2d 4488 |
. . . . 5
⊢ (𝑟 = 𝑠 → if(𝑟 = {∅}, {∅, 1o}, 𝑟) = if(𝑠 = {∅}, {∅, 1o}, 𝑠)) |
57 | 56, 48, 51 | fvmpt 6895 |
. . . 4
⊢ (𝑠 ∈ 𝒫 3o
→ (𝐾‘𝑠) = if(𝑠 = {∅}, {∅, 1o}, 𝑠)) |
58 | 57 | fveq2d 6796 |
. . 3
⊢ (𝑠 ∈ 𝒫 3o
→ (𝐾‘(𝐾‘𝑠)) = (𝐾‘if(𝑠 = {∅}, {∅, 1o}, 𝑠))) |
59 | 53, 58, 57 | 3eqtr4d 2783 |
. 2
⊢ (𝑠 ∈ 𝒫 3o
→ (𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠)) |
60 | 59 | rgen 3061 |
1
⊢
∀𝑠 ∈
𝒫 3o(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠) |