Proof of Theorem clsk1indlem2
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . . . . 10
⊢ (𝑠 = {∅} → 𝑠 = {∅}) |
2 | | snsspr1 4345 |
. . . . . . . . . 10
⊢ {∅}
⊆ {∅, 1𝑜} |
3 | 1, 2 | syl6eqss 3655 |
. . . . . . . . 9
⊢ (𝑠 = {∅} → 𝑠 ⊆ {∅,
1𝑜}) |
4 | 3 | ancli 574 |
. . . . . . . 8
⊢ (𝑠 = {∅} → (𝑠 = {∅} ∧ 𝑠 ⊆ {∅,
1𝑜})) |
5 | 4 | con3i 150 |
. . . . . . 7
⊢ (¬
(𝑠 = {∅} ∧ 𝑠 ⊆ {∅,
1𝑜}) → ¬ 𝑠 = {∅}) |
6 | | ssid 3624 |
. . . . . . 7
⊢ 𝑠 ⊆ 𝑠 |
7 | 5, 6 | jctir 561 |
. . . . . 6
⊢ (¬
(𝑠 = {∅} ∧ 𝑠 ⊆ {∅,
1𝑜}) → (¬ 𝑠 = {∅} ∧ 𝑠 ⊆ 𝑠)) |
8 | 7 | orri 391 |
. . . . 5
⊢ ((𝑠 = {∅} ∧ 𝑠 ⊆ {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑠 ⊆ 𝑠)) |
9 | 8 | a1i 11 |
. . . 4
⊢ (𝑠 ∈ 𝒫
3𝑜 → ((𝑠 = {∅} ∧ 𝑠 ⊆ {∅, 1𝑜})
∨ (¬ 𝑠 = {∅}
∧ 𝑠 ⊆ 𝑠))) |
10 | | sseq2 3627 |
. . . . 5
⊢ (if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
= {∅, 1𝑜} → (𝑠 ⊆ if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
↔ 𝑠 ⊆ {∅,
1𝑜})) |
11 | | sseq2 3627 |
. . . . 5
⊢ (if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
= 𝑠 → (𝑠 ⊆ if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
↔ 𝑠 ⊆ 𝑠)) |
12 | 10, 11 | elimif 4122 |
. . . 4
⊢ (𝑠 ⊆ if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
↔ ((𝑠 = {∅}
∧ 𝑠 ⊆ {∅,
1𝑜}) ∨ (¬ 𝑠 = {∅} ∧ 𝑠 ⊆ 𝑠))) |
13 | 9, 12 | sylibr 224 |
. . 3
⊢ (𝑠 ∈ 𝒫
3𝑜 → 𝑠 ⊆ if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)) |
14 | | eqeq1 2626 |
. . . . 5
⊢ (𝑟 = 𝑠 → (𝑟 = {∅} ↔ 𝑠 = {∅})) |
15 | | id 22 |
. . . . 5
⊢ (𝑟 = 𝑠 → 𝑟 = 𝑠) |
16 | 14, 15 | ifbieq2d 4111 |
. . . 4
⊢ (𝑟 = 𝑠 → if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)
= if(𝑠 = {∅},
{∅, 1𝑜}, 𝑠)) |
17 | | clsk1indlem.k |
. . . 4
⊢ 𝐾 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) |
18 | | prex 4909 |
. . . . 5
⊢ {∅,
1𝑜} ∈ V |
19 | | vex 3203 |
. . . . 5
⊢ 𝑠 ∈ V |
20 | 18, 19 | ifex 4156 |
. . . 4
⊢ if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)
∈ V |
21 | 16, 17, 20 | fvmpt 6282 |
. . 3
⊢ (𝑠 ∈ 𝒫
3𝑜 → (𝐾‘𝑠) = if(𝑠 = {∅}, {∅,
1𝑜}, 𝑠)) |
22 | 13, 21 | sseqtr4d 3642 |
. 2
⊢ (𝑠 ∈ 𝒫
3𝑜 → 𝑠 ⊆ (𝐾‘𝑠)) |
23 | 22 | rgen 2922 |
1
⊢
∀𝑠 ∈
𝒫 3𝑜𝑠 ⊆ (𝐾‘𝑠) |