Step | Hyp | Ref
| Expression |
1 | | reldom 7847 |
. . 3
⊢ Rel
≼ |
2 | 1 | brrelexi 5082 |
. 2
⊢ (𝑋 ≼ ω → 𝑋 ∈ V) |
3 | | elex 3185 |
. . 3
⊢
(𝒫 𝑋 ∈
2nd𝜔 → 𝒫 𝑋 ∈ V) |
4 | | pwexb 6867 |
. . 3
⊢ (𝑋 ∈ V ↔ 𝒫 𝑋 ∈ V) |
5 | 3, 4 | sylibr 223 |
. 2
⊢
(𝒫 𝑋 ∈
2nd𝜔 → 𝑋 ∈ V) |
6 | | elex 3185 |
. . . . 5
⊢ (𝑋 ∈ V → 𝑋 ∈ V) |
7 | | snex 4835 |
. . . . . . . 8
⊢ {𝑥} ∈ V |
8 | 7 | 2a1i 12 |
. . . . . . 7
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 → {𝑥} ∈ V)) |
9 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
10 | 9 | sneqr 4311 |
. . . . . . . . 9
⊢ ({𝑥} = {𝑦} → 𝑥 = 𝑦) |
11 | | sneq 4135 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
12 | 10, 11 | impbii 198 |
. . . . . . . 8
⊢ ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦) |
13 | 12 | 2a1i 12 |
. . . . . . 7
⊢ (𝑋 ∈ V → ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → ({𝑥} = {𝑦} ↔ 𝑥 = 𝑦))) |
14 | 8, 13 | dom2lem 7881 |
. . . . . 6
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1→V) |
15 | | f1f1orn 6061 |
. . . . . 6
⊢ ((𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1→V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) |
16 | 14, 15 | syl 17 |
. . . . 5
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) |
17 | | f1oeng 7860 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋–1-1-onto→ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) → 𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
18 | 6, 16, 17 | syl2anc 691 |
. . . 4
⊢ (𝑋 ∈ V → 𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
19 | | domen1 7987 |
. . . 4
⊢ (𝑋 ≈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) → (𝑋 ≼ ω ↔ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
20 | 18, 19 | syl 17 |
. . 3
⊢ (𝑋 ∈ V → (𝑋 ≼ ω ↔ ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
21 | | distop 20610 |
. . . . . . 7
⊢ (𝑋 ∈ V → 𝒫 𝑋 ∈ Top) |
22 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
23 | 9 | snelpw 4840 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 ↔ {𝑥} ∈ 𝒫 𝑋) |
24 | 22, 23 | sylib 207 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝒫 𝑋) |
25 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝑋 ↦ {𝑥}) = (𝑥 ∈ 𝑋 ↦ {𝑥}) |
26 | 24, 25 | fmptd 6292 |
. . . . . . . 8
⊢ (𝑋 ∈ V → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋) |
27 | | frn 5966 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝒫 𝑋 → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋) |
28 | 26, 27 | syl 17 |
. . . . . . 7
⊢ (𝑋 ∈ V → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋) |
29 | | elpwi 4117 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝒫 𝑋 → 𝑦 ⊆ 𝑋) |
30 | 29 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑦 ⊆ 𝑋) |
31 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝑦) |
32 | 30, 31 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ 𝑋) |
33 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} = {𝑧}) |
34 | | sneq 4135 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → {𝑥} = {𝑧}) |
35 | 34 | eqeq2d 2620 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → ({𝑧} = {𝑥} ↔ {𝑧} = {𝑧})) |
36 | 35 | rspcev 3282 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝑋 ∧ {𝑧} = {𝑧}) → ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
37 | 32, 33, 36 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
38 | | snex 4835 |
. . . . . . . . . . 11
⊢ {𝑧} ∈ V |
39 | 25 | elrnmpt 5293 |
. . . . . . . . . . 11
⊢ ({𝑧} ∈ V → ({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ↔ ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥})) |
40 | 38, 39 | ax-mp 5 |
. . . . . . . . . 10
⊢ ({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ↔ ∃𝑥 ∈ 𝑋 {𝑧} = {𝑥}) |
41 | 37, 40 | sylibr 223 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})) |
42 | | vsnid 4156 |
. . . . . . . . . 10
⊢ 𝑧 ∈ {𝑧} |
43 | 42 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → 𝑧 ∈ {𝑧}) |
44 | 31 | snssd 4281 |
. . . . . . . . 9
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → {𝑧} ⊆ 𝑦) |
45 | | eleq2 2677 |
. . . . . . . . . . 11
⊢ (𝑤 = {𝑧} → (𝑧 ∈ 𝑤 ↔ 𝑧 ∈ {𝑧})) |
46 | | sseq1 3589 |
. . . . . . . . . . 11
⊢ (𝑤 = {𝑧} → (𝑤 ⊆ 𝑦 ↔ {𝑧} ⊆ 𝑦)) |
47 | 45, 46 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑤 = {𝑧} → ((𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦) ↔ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦))) |
48 | 47 | rspcev 3282 |
. . . . . . . . 9
⊢ (({𝑧} ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ∧ (𝑧 ∈ {𝑧} ∧ {𝑧} ⊆ 𝑦)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
49 | 41, 43, 44, 48 | syl12anc 1316 |
. . . . . . . 8
⊢ ((𝑋 ∈ V ∧ (𝑦 ∈ 𝒫 𝑋 ∧ 𝑧 ∈ 𝑦)) → ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
50 | 49 | ralrimivva 2954 |
. . . . . . 7
⊢ (𝑋 ∈ V → ∀𝑦 ∈ 𝒫 𝑋∀𝑧 ∈ 𝑦 ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) |
51 | | basgen2 20604 |
. . . . . . 7
⊢
((𝒫 𝑋 ∈
Top ∧ ran (𝑥 ∈
𝑋 ↦ {𝑥}) ⊆ 𝒫 𝑋 ∧ ∀𝑦 ∈ 𝒫 𝑋∀𝑧 ∈ 𝑦 ∃𝑤 ∈ ran (𝑥 ∈ 𝑋 ↦ {𝑥})(𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ 𝑦)) → (topGen‘ran (𝑥 ∈ 𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
52 | 21, 28, 50, 51 | syl3anc 1318 |
. . . . . 6
⊢ (𝑋 ∈ V →
(topGen‘ran (𝑥 ∈
𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
53 | 52 | adantr 480 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) = 𝒫 𝑋) |
54 | 52, 21 | eqeltrd 2688 |
. . . . . . 7
⊢ (𝑋 ∈ V →
(topGen‘ran (𝑥 ∈
𝑋 ↦ {𝑥})) ∈ Top) |
55 | | tgclb 20585 |
. . . . . . 7
⊢ (ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases ↔ (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈ Top) |
56 | 54, 55 | sylibr 223 |
. . . . . 6
⊢ (𝑋 ∈ V → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases) |
57 | | 2ndci 21061 |
. . . . . 6
⊢ ((ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ∈ TopBases ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈
2nd𝜔) |
58 | 56, 57 | sylan 487 |
. . . . 5
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → (topGen‘ran
(𝑥 ∈ 𝑋 ↦ {𝑥})) ∈
2nd𝜔) |
59 | 53, 58 | eqeltrrd 2689 |
. . . 4
⊢ ((𝑋 ∈ V ∧ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) → 𝒫 𝑋 ∈
2nd𝜔) |
60 | | is2ndc 21059 |
. . . . . 6
⊢
(𝒫 𝑋 ∈
2nd𝜔 ↔ ∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧ (topGen‘𝑏) = 𝒫 𝑋)) |
61 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑏 ∈ V |
62 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
63 | 62, 23 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝒫 𝑋) |
64 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → (topGen‘𝑏) = 𝒫 𝑋) |
65 | 63, 64 | eleqtrrd 2691 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ (topGen‘𝑏)) |
66 | | vsnid 4156 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ {𝑥} |
67 | | tg2 20580 |
. . . . . . . . . . . . . 14
⊢ (({𝑥} ∈ (topGen‘𝑏) ∧ 𝑥 ∈ {𝑥}) → ∃𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥})) |
68 | 65, 66, 67 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → ∃𝑦 ∈ 𝑏 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥})) |
69 | | simprrl 800 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑥 ∈ 𝑦) |
70 | 69 | snssd 4281 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} ⊆ 𝑦) |
71 | | simprrr 801 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑦 ⊆ {𝑥}) |
72 | 70, 71 | eqssd 3585 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} = 𝑦) |
73 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → 𝑦 ∈ 𝑏) |
74 | 72, 73 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈ V
∧ 𝑏 ∈ TopBases)
∧ (𝑏 ≼ ω
∧ (topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) ∧ (𝑦 ∈ 𝑏 ∧ (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ {𝑥}))) → {𝑥} ∈ 𝑏) |
75 | 68, 74 | rexlimddv 3017 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ 𝑏) |
76 | 75, 25 | fmptd 6292 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → (𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝑏) |
77 | | frn 5966 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝑋 ↦ {𝑥}):𝑋⟶𝑏 → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝑏) |
78 | 76, 77 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝑏) |
79 | | ssdomg 7887 |
. . . . . . . . . 10
⊢ (𝑏 ∈ V → (ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ⊆ 𝑏 → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏)) |
80 | 61, 78, 79 | mpsyl 66 |
. . . . . . . . 9
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏) |
81 | | simprl 790 |
. . . . . . . . 9
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → 𝑏 ≼
ω) |
82 | | domtr 7895 |
. . . . . . . . 9
⊢ ((ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ 𝑏 ∧ 𝑏 ≼ ω) → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
83 | 80, 81, 82 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) ∧ (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋)) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
84 | 83 | ex 449 |
. . . . . . 7
⊢ ((𝑋 ∈ V ∧ 𝑏 ∈ TopBases) → ((𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
85 | 84 | rexlimdva 3013 |
. . . . . 6
⊢ (𝑋 ∈ V → (∃𝑏 ∈ TopBases (𝑏 ≼ ω ∧
(topGen‘𝑏) =
𝒫 𝑋) → ran
(𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
86 | 60, 85 | syl5bi 231 |
. . . . 5
⊢ (𝑋 ∈ V → (𝒫
𝑋 ∈
2nd𝜔 → ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω)) |
87 | 86 | imp 444 |
. . . 4
⊢ ((𝑋 ∈ V ∧ 𝒫 𝑋 ∈ 2nd𝜔)
→ ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω) |
88 | 59, 87 | impbida 873 |
. . 3
⊢ (𝑋 ∈ V → (ran (𝑥 ∈ 𝑋 ↦ {𝑥}) ≼ ω ↔ 𝒫 𝑋 ∈
2nd𝜔)) |
89 | 20, 88 | bitrd 267 |
. 2
⊢ (𝑋 ∈ V → (𝑋 ≼ ω ↔
𝒫 𝑋 ∈
2nd𝜔)) |
90 | 2, 5, 89 | pm5.21nii 367 |
1
⊢ (𝑋 ≼ ω ↔
𝒫 𝑋 ∈
2nd𝜔) |