Proof of Theorem clsk1indlem4
Step | Hyp | Ref
| Expression |
1 | | tpex 6957 |
. . . . . . . . . 10
⊢ {∅,
1𝑜, 2𝑜} ∈ V |
2 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (⊤
→ {∅, 1𝑜, 2𝑜} ∈
V) |
3 | | snsstp1 4347 |
. . . . . . . . . . . 12
⊢ {∅}
⊆ {∅, 1𝑜,
2𝑜} |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ {∅} ⊆ {∅, 1𝑜,
2𝑜}) |
5 | | 0ex 4790 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
6 | 5 | snss 4316 |
. . . . . . . . . . 11
⊢ (∅
∈ {∅, 1𝑜, 2𝑜} ↔ {∅}
⊆ {∅, 1𝑜,
2𝑜}) |
7 | 4, 6 | sylibr 224 |
. . . . . . . . . 10
⊢ (⊤
→ ∅ ∈ {∅, 1𝑜,
2𝑜}) |
8 | | snsstp2 4348 |
. . . . . . . . . . . 12
⊢
{1𝑜} ⊆ {∅, 1𝑜,
2𝑜} |
9 | 8 | a1i 11 |
. . . . . . . . . . 11
⊢ (⊤
→ {1𝑜} ⊆ {∅, 1𝑜,
2𝑜}) |
10 | | 1on 7567 |
. . . . . . . . . . . . 13
⊢
1𝑜 ∈ On |
11 | 10 | elexi 3213 |
. . . . . . . . . . . 12
⊢
1𝑜 ∈ V |
12 | 11 | snss 4316 |
. . . . . . . . . . 11
⊢
(1𝑜 ∈ {∅, 1𝑜,
2𝑜} ↔ {1𝑜} ⊆ {∅,
1𝑜, 2𝑜}) |
13 | 9, 12 | sylibr 224 |
. . . . . . . . . 10
⊢ (⊤
→ 1𝑜 ∈ {∅, 1𝑜,
2𝑜}) |
14 | 7, 13 | prssd 4354 |
. . . . . . . . 9
⊢ (⊤
→ {∅, 1𝑜} ⊆ {∅,
1𝑜, 2𝑜}) |
15 | 2, 14 | sselpwd 4807 |
. . . . . . . 8
⊢ (⊤
→ {∅, 1𝑜} ∈ 𝒫 {∅,
1𝑜, 2𝑜}) |
16 | 15 | trud 1493 |
. . . . . . 7
⊢ {∅,
1𝑜} ∈ 𝒫 {∅, 1𝑜,
2𝑜} |
17 | | df3o2 38322 |
. . . . . . . 8
⊢
3𝑜 = {∅, 1𝑜,
2𝑜} |
18 | 17 | pweqi 4162 |
. . . . . . 7
⊢ 𝒫
3𝑜 = 𝒫 {∅, 1𝑜,
2𝑜} |
19 | 16, 18 | eleqtrri 2700 |
. . . . . 6
⊢ {∅,
1𝑜} ∈ 𝒫 3𝑜 |
20 | 19 | a1i 11 |
. . . . 5
⊢ (𝑠 ∈ 𝒫
3𝑜 → {∅, 1𝑜} ∈ 𝒫
3𝑜) |
21 | | id 22 |
. . . . 5
⊢ (𝑠 ∈ 𝒫
3𝑜 → 𝑠 ∈ 𝒫
3𝑜) |
22 | 20, 21 | ifcld 4131 |
. . . 4
⊢ (𝑠 ∈ 𝒫
3𝑜 → if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∈ 𝒫 3𝑜) |
23 | | eqeq1 2626 |
. . . . . . . 8
⊢ (𝑟 = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
→ (𝑟 = {∅}
↔ if(𝑠 = {∅},
{∅, 1𝑜}, 𝑠) = {∅})) |
24 | | eqcom 2629 |
. . . . . . . . 9
⊢ (if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
= {∅} ↔ {∅} = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)) |
25 | | eqif 4126 |
. . . . . . . . 9
⊢
({∅} = if(𝑠 =
{∅}, {∅, 1𝑜}, 𝑠) ↔ ((𝑠 = {∅} ∧ {∅} = {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ {∅} = 𝑠))) |
26 | 24, 25 | bitri 264 |
. . . . . . . 8
⊢ (if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
= {∅} ↔ ((𝑠 =
{∅} ∧ {∅} = {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ {∅} =
𝑠))) |
27 | 23, 26 | syl6bb 276 |
. . . . . . 7
⊢ (𝑟 = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
→ (𝑟 = {∅}
↔ ((𝑠 = {∅}
∧ {∅} = {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ {∅} =
𝑠)))) |
28 | | id 22 |
. . . . . . 7
⊢ (𝑟 = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
→ 𝑟 = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)) |
29 | 27, 28 | ifbieq2d 4111 |
. . . . . 6
⊢ (𝑟 = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
→ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟) = if(((𝑠 = {∅} ∧ {∅} = {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ {∅} = 𝑠)), {∅,
1𝑜}, if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠))) |
30 | | 1n0 7575 |
. . . . . . . . . 10
⊢
1𝑜 ≠ ∅ |
31 | | dfsn2 4190 |
. . . . . . . . . . . 12
⊢ {∅}
= {∅, ∅} |
32 | 31 | eqeq1i 2627 |
. . . . . . . . . . 11
⊢
({∅} = {∅, 1𝑜} ↔ {∅, ∅}
= {∅, 1𝑜}) |
33 | 5 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ ∅ ∈ V) |
34 | 10 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (⊤
→ 1𝑜 ∈ On) |
35 | 33, 34 | preq2b 4378 |
. . . . . . . . . . . 12
⊢ (⊤
→ ({∅, ∅} = {∅, 1𝑜} ↔ ∅ =
1𝑜)) |
36 | 35 | trud 1493 |
. . . . . . . . . . 11
⊢
({∅, ∅} = {∅, 1𝑜} ↔ ∅ =
1𝑜) |
37 | | eqcom 2629 |
. . . . . . . . . . 11
⊢ (∅
= 1𝑜 ↔ 1𝑜 =
∅) |
38 | 32, 36, 37 | 3bitri 286 |
. . . . . . . . . 10
⊢
({∅} = {∅, 1𝑜} ↔
1𝑜 = ∅) |
39 | 30, 38 | nemtbir 2889 |
. . . . . . . . 9
⊢ ¬
{∅} = {∅, 1𝑜} |
40 | 39 | intnan 960 |
. . . . . . . 8
⊢ ¬
(𝑠 = {∅} ∧
{∅} = {∅, 1𝑜}) |
41 | | pm3.24 926 |
. . . . . . . . 9
⊢ ¬
(𝑠 = {∅} ∧ ¬
𝑠 =
{∅}) |
42 | | eqcom 2629 |
. . . . . . . . . 10
⊢ (𝑠 = {∅} ↔ {∅} =
𝑠) |
43 | 42 | anbi2ci 732 |
. . . . . . . . 9
⊢ ((𝑠 = {∅} ∧ ¬ 𝑠 = {∅}) ↔ (¬
𝑠 = {∅} ∧
{∅} = 𝑠)) |
44 | 41, 43 | mtbi 312 |
. . . . . . . 8
⊢ ¬
(¬ 𝑠 = {∅} ∧
{∅} = 𝑠) |
45 | 40, 44 | pm3.2ni 899 |
. . . . . . 7
⊢ ¬
((𝑠 = {∅} ∧
{∅} = {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ {∅} = 𝑠)) |
46 | 45 | iffalsei 4096 |
. . . . . 6
⊢
if(((𝑠 = {∅}
∧ {∅} = {∅, 1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ {∅} =
𝑠)), {∅,
1𝑜}, if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠))
= if(𝑠 = {∅},
{∅, 1𝑜}, 𝑠) |
47 | 29, 46 | syl6eq 2672 |
. . . . 5
⊢ (𝑟 = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
→ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟) = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)) |
48 | | clsk1indlem.k |
. . . . 5
⊢ 𝐾 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) |
49 | | prex 4909 |
. . . . . 6
⊢ {∅,
1𝑜} ∈ V |
50 | | vex 3203 |
. . . . . 6
⊢ 𝑠 ∈ V |
51 | 49, 50 | ifex 4156 |
. . . . 5
⊢ if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∈ V |
52 | 47, 48, 51 | fvmpt 6282 |
. . . 4
⊢ (if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∈ 𝒫 3𝑜 → (𝐾‘if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠))
= if(𝑠 = {∅},
{∅, 1𝑜}, 𝑠)) |
53 | 22, 52 | syl 17 |
. . 3
⊢ (𝑠 ∈ 𝒫
3𝑜 → (𝐾‘if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠))
= if(𝑠 = {∅},
{∅, 1𝑜}, 𝑠)) |
54 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑟 = 𝑠 → (𝑟 = {∅} ↔ 𝑠 = {∅})) |
55 | | id 22 |
. . . . . 6
⊢ (𝑟 = 𝑠 → 𝑟 = 𝑠) |
56 | 54, 55 | ifbieq2d 4111 |
. . . . 5
⊢ (𝑟 = 𝑠 → if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)
= if(𝑠 = {∅},
{∅, 1𝑜}, 𝑠)) |
57 | 56, 48, 51 | fvmpt 6282 |
. . . 4
⊢ (𝑠 ∈ 𝒫
3𝑜 → (𝐾‘𝑠) = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)) |
58 | 57 | fveq2d 6195 |
. . 3
⊢ (𝑠 ∈ 𝒫
3𝑜 → (𝐾‘(𝐾‘𝑠)) = (𝐾‘if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠))) |
59 | 53, 58, 57 | 3eqtr4d 2666 |
. 2
⊢ (𝑠 ∈ 𝒫
3𝑜 → (𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠)) |
60 | 59 | rgen 2922 |
1
⊢
∀𝑠 ∈
𝒫 3𝑜(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠) |