Proof of Theorem clsk1indlem1
Step | Hyp | Ref
| Expression |
1 | | tpex 6957 |
. . . . . 6
⊢ {∅,
1𝑜, 2𝑜} ∈ V |
2 | 1 | a1i 11 |
. . . . 5
⊢ (⊤
→ {∅, 1𝑜, 2𝑜} ∈
V) |
3 | | snsstp1 4347 |
. . . . . 6
⊢ {∅}
⊆ {∅, 1𝑜,
2𝑜} |
4 | 3 | a1i 11 |
. . . . 5
⊢ (⊤
→ {∅} ⊆ {∅, 1𝑜,
2𝑜}) |
5 | 2, 4 | sselpwd 4807 |
. . . 4
⊢ (⊤
→ {∅} ∈ 𝒫 {∅, 1𝑜,
2𝑜}) |
6 | 5 | trud 1493 |
. . 3
⊢ {∅}
∈ 𝒫 {∅, 1𝑜,
2𝑜} |
7 | | df3o2 38322 |
. . . 4
⊢
3𝑜 = {∅, 1𝑜,
2𝑜} |
8 | 7 | pweqi 4162 |
. . 3
⊢ 𝒫
3𝑜 = 𝒫 {∅, 1𝑜,
2𝑜} |
9 | 6, 8 | eleqtrri 2700 |
. 2
⊢ {∅}
∈ 𝒫 3𝑜 |
10 | | 0ex 4790 |
. . . . . . . 8
⊢ ∅
∈ V |
11 | 10 | snss 4316 |
. . . . . . 7
⊢ (∅
∈ {∅, 1𝑜, 2𝑜} ↔ {∅}
⊆ {∅, 1𝑜,
2𝑜}) |
12 | 4, 11 | sylibr 224 |
. . . . . 6
⊢ (⊤
→ ∅ ∈ {∅, 1𝑜,
2𝑜}) |
13 | | snsstp3 4349 |
. . . . . . . 8
⊢
{2𝑜} ⊆ {∅, 1𝑜,
2𝑜} |
14 | 13 | a1i 11 |
. . . . . . 7
⊢ (⊤
→ {2𝑜} ⊆ {∅, 1𝑜,
2𝑜}) |
15 | | 2on 7568 |
. . . . . . . . 9
⊢
2𝑜 ∈ On |
16 | 15 | elexi 3213 |
. . . . . . . 8
⊢
2𝑜 ∈ V |
17 | 16 | snss 4316 |
. . . . . . 7
⊢
(2𝑜 ∈ {∅, 1𝑜,
2𝑜} ↔ {2𝑜} ⊆ {∅,
1𝑜, 2𝑜}) |
18 | 14, 17 | sylibr 224 |
. . . . . 6
⊢ (⊤
→ 2𝑜 ∈ {∅, 1𝑜,
2𝑜}) |
19 | 12, 18 | prssd 4354 |
. . . . 5
⊢ (⊤
→ {∅, 2𝑜} ⊆ {∅,
1𝑜, 2𝑜}) |
20 | 2, 19 | sselpwd 4807 |
. . . 4
⊢ (⊤
→ {∅, 2𝑜} ∈ 𝒫 {∅,
1𝑜, 2𝑜}) |
21 | 20 | trud 1493 |
. . 3
⊢ {∅,
2𝑜} ∈ 𝒫 {∅, 1𝑜,
2𝑜} |
22 | 21, 8 | eleqtrri 2700 |
. 2
⊢ {∅,
2𝑜} ∈ 𝒫 3𝑜 |
23 | | simpl 473 |
. . 3
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) → {∅}
∈ 𝒫 3𝑜) |
24 | | sseq1 3626 |
. . . . . 6
⊢ (𝑠 = {∅} → (𝑠 ⊆ 𝑡 ↔ {∅} ⊆ 𝑡)) |
25 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑠 = {∅} → (𝐾‘𝑠) = (𝐾‘{∅})) |
26 | 25 | sseq1d 3632 |
. . . . . . 7
⊢ (𝑠 = {∅} → ((𝐾‘𝑠) ⊆ (𝐾‘𝑡) ↔ (𝐾‘{∅}) ⊆ (𝐾‘𝑡))) |
27 | 26 | notbid 308 |
. . . . . 6
⊢ (𝑠 = {∅} → (¬
(𝐾‘𝑠) ⊆ (𝐾‘𝑡) ↔ ¬ (𝐾‘{∅}) ⊆ (𝐾‘𝑡))) |
28 | 24, 27 | anbi12d 747 |
. . . . 5
⊢ (𝑠 = {∅} → ((𝑠 ⊆ 𝑡 ∧ ¬ (𝐾‘𝑠) ⊆ (𝐾‘𝑡)) ↔ ({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘𝑡)))) |
29 | 28 | rexbidv 3052 |
. . . 4
⊢ (𝑠 = {∅} →
(∃𝑡 ∈ 𝒫
3𝑜(𝑠
⊆ 𝑡 ∧ ¬
(𝐾‘𝑠) ⊆ (𝐾‘𝑡)) ↔ ∃𝑡 ∈ 𝒫
3𝑜({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘𝑡)))) |
30 | 29 | adantl 482 |
. . 3
⊢
((({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) ∧ 𝑠 = {∅}) →
(∃𝑡 ∈ 𝒫
3𝑜(𝑠
⊆ 𝑡 ∧ ¬
(𝐾‘𝑠) ⊆ (𝐾‘𝑡)) ↔ ∃𝑡 ∈ 𝒫
3𝑜({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘𝑡)))) |
31 | | simpr 477 |
. . . 4
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) → {∅,
2𝑜} ∈ 𝒫 3𝑜) |
32 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑡 = {∅,
2𝑜} → (𝐾‘𝑡) = (𝐾‘{∅,
2𝑜})) |
33 | 32 | sseq2d 3633 |
. . . . . . 7
⊢ (𝑡 = {∅,
2𝑜} → ((𝐾‘{∅}) ⊆ (𝐾‘𝑡) ↔ (𝐾‘{∅}) ⊆ (𝐾‘{∅,
2𝑜}))) |
34 | 33 | notbid 308 |
. . . . . 6
⊢ (𝑡 = {∅,
2𝑜} → (¬ (𝐾‘{∅}) ⊆ (𝐾‘𝑡) ↔ ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅,
2𝑜}))) |
35 | 34 | cleq2lem 37914 |
. . . . 5
⊢ (𝑡 = {∅,
2𝑜} → (({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘𝑡)) ↔ ({∅} ⊆ {∅,
2𝑜} ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅,
2𝑜})))) |
36 | 35 | adantl 482 |
. . . 4
⊢
((({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) ∧ 𝑡 = {∅,
2𝑜}) → (({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘𝑡)) ↔ ({∅} ⊆ {∅,
2𝑜} ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅,
2𝑜})))) |
37 | | 1on 7567 |
. . . . . . . . 9
⊢
1𝑜 ∈ On |
38 | 37 | elexi 3213 |
. . . . . . . 8
⊢
1𝑜 ∈ V |
39 | 38 | prid2 4298 |
. . . . . . 7
⊢
1𝑜 ∈ {∅,
1𝑜} |
40 | | iftrue 4092 |
. . . . . . . . 9
⊢ (𝑟 = {∅} → if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)
= {∅, 1𝑜}) |
41 | | clsk1indlem.k |
. . . . . . . . 9
⊢ 𝐾 = (𝑟 ∈ 𝒫 3𝑜
↦ if(𝑟 = {∅},
{∅, 1𝑜}, 𝑟)) |
42 | | prex 4909 |
. . . . . . . . 9
⊢ {∅,
1𝑜} ∈ V |
43 | 40, 41, 42 | fvmpt 6282 |
. . . . . . . 8
⊢
({∅} ∈ 𝒫 3𝑜 → (𝐾‘{∅}) = {∅,
1𝑜}) |
44 | 43 | adantr 481 |
. . . . . . 7
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) → (𝐾‘{∅}) = {∅,
1𝑜}) |
45 | 39, 44 | syl5eleqr 2708 |
. . . . . 6
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) →
1𝑜 ∈ (𝐾‘{∅})) |
46 | | 1n0 7575 |
. . . . . . . . . . 11
⊢
1𝑜 ≠ ∅ |
47 | 46 | neii 2796 |
. . . . . . . . . 10
⊢ ¬
1𝑜 = ∅ |
48 | | eqcom 2629 |
. . . . . . . . . . . 12
⊢
(1𝑜 = 2𝑜 ↔
2𝑜 = 1𝑜) |
49 | | df-2o 7561 |
. . . . . . . . . . . . 13
⊢
2𝑜 = suc 1𝑜 |
50 | | df-1o 7560 |
. . . . . . . . . . . . 13
⊢
1𝑜 = suc ∅ |
51 | 49, 50 | eqeq12i 2636 |
. . . . . . . . . . . 12
⊢
(2𝑜 = 1𝑜 ↔ suc
1𝑜 = suc ∅) |
52 | | suc11reg 8516 |
. . . . . . . . . . . 12
⊢ (suc
1𝑜 = suc ∅ ↔ 1𝑜 =
∅) |
53 | 48, 51, 52 | 3bitri 286 |
. . . . . . . . . . 11
⊢
(1𝑜 = 2𝑜 ↔
1𝑜 = ∅) |
54 | 46, 53 | nemtbir 2889 |
. . . . . . . . . 10
⊢ ¬
1𝑜 = 2𝑜 |
55 | 47, 54 | pm3.2ni 899 |
. . . . . . . . 9
⊢ ¬
(1𝑜 = ∅ ∨ 1𝑜 =
2𝑜) |
56 | | elpri 4197 |
. . . . . . . . 9
⊢
(1𝑜 ∈ {∅, 2𝑜} →
(1𝑜 = ∅ ∨ 1𝑜 =
2𝑜)) |
57 | 55, 56 | mto 188 |
. . . . . . . 8
⊢ ¬
1𝑜 ∈ {∅, 2𝑜} |
58 | 57 | a1i 11 |
. . . . . . 7
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) → ¬
1𝑜 ∈ {∅, 2𝑜}) |
59 | | eqeq1 2626 |
. . . . . . . . . . 11
⊢ (𝑟 = {∅,
2𝑜} → (𝑟 = {∅} ↔ {∅,
2𝑜} = {∅})) |
60 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑟 = {∅,
2𝑜} → 𝑟 = {∅,
2𝑜}) |
61 | 59, 60 | ifbieq2d 4111 |
. . . . . . . . . 10
⊢ (𝑟 = {∅,
2𝑜} → if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)
= if({∅, 2𝑜} = {∅}, {∅,
1𝑜}, {∅, 2𝑜})) |
62 | 16 | prid2 4298 |
. . . . . . . . . . . 12
⊢
2𝑜 ∈ {∅,
2𝑜} |
63 | | 2on0 7569 |
. . . . . . . . . . . . 13
⊢
2𝑜 ≠ ∅ |
64 | | nelsn 4212 |
. . . . . . . . . . . . 13
⊢
(2𝑜 ≠ ∅ → ¬ 2𝑜
∈ {∅}) |
65 | 63, 64 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ ¬
2𝑜 ∈ {∅} |
66 | | nelneq2 2726 |
. . . . . . . . . . . 12
⊢
((2𝑜 ∈ {∅, 2𝑜} ∧
¬ 2𝑜 ∈ {∅}) → ¬ {∅,
2𝑜} = {∅}) |
67 | 62, 65, 66 | mp2an 708 |
. . . . . . . . . . 11
⊢ ¬
{∅, 2𝑜} = {∅} |
68 | 67 | iffalsei 4096 |
. . . . . . . . . 10
⊢
if({∅, 2𝑜} = {∅}, {∅,
1𝑜}, {∅, 2𝑜}) = {∅,
2𝑜} |
69 | 61, 68 | syl6eq 2672 |
. . . . . . . . 9
⊢ (𝑟 = {∅,
2𝑜} → if(𝑟 = {∅}, {∅,
1𝑜}, 𝑟)
= {∅, 2𝑜}) |
70 | | prex 4909 |
. . . . . . . . 9
⊢ {∅,
2𝑜} ∈ V |
71 | 69, 41, 70 | fvmpt 6282 |
. . . . . . . 8
⊢
({∅, 2𝑜} ∈ 𝒫 3𝑜
→ (𝐾‘{∅,
2𝑜}) = {∅, 2𝑜}) |
72 | 71 | adantl 482 |
. . . . . . 7
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) → (𝐾‘{∅,
2𝑜}) = {∅, 2𝑜}) |
73 | 58, 72 | neleqtrrd 2723 |
. . . . . 6
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) → ¬
1𝑜 ∈ (𝐾‘{∅,
2𝑜})) |
74 | | nelss 3664 |
. . . . . 6
⊢
((1𝑜 ∈ (𝐾‘{∅}) ∧ ¬
1𝑜 ∈ (𝐾‘{∅, 2𝑜}))
→ ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅,
2𝑜})) |
75 | 45, 73, 74 | syl2anc 693 |
. . . . 5
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) → ¬
(𝐾‘{∅}) ⊆
(𝐾‘{∅,
2𝑜})) |
76 | | snsspr1 4345 |
. . . . 5
⊢ {∅}
⊆ {∅, 2𝑜} |
77 | 75, 76 | jctil 560 |
. . . 4
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) →
({∅} ⊆ {∅, 2𝑜} ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘{∅,
2𝑜}))) |
78 | 31, 36, 77 | rspcedvd 3317 |
. . 3
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) →
∃𝑡 ∈ 𝒫
3𝑜({∅} ⊆ 𝑡 ∧ ¬ (𝐾‘{∅}) ⊆ (𝐾‘𝑡))) |
79 | 23, 30, 78 | rspcedvd 3317 |
. 2
⊢
(({∅} ∈ 𝒫 3𝑜 ∧ {∅,
2𝑜} ∈ 𝒫 3𝑜) →
∃𝑠 ∈ 𝒫
3𝑜∃𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 ∧ ¬ (𝐾‘𝑠) ⊆ (𝐾‘𝑡))) |
80 | 9, 22, 79 | mp2an 708 |
1
⊢
∃𝑠 ∈
𝒫 3𝑜∃𝑡 ∈ 𝒫 3𝑜(𝑠 ⊆ 𝑡 ∧ ¬ (𝐾‘𝑠) ⊆ (𝐾‘𝑡)) |