| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prex 5436 | . . . . 5
⊢ {𝑆, {𝒫 ∪ 𝑆}}
∈ V | 
| 2 |  | vex 3483 | . . . . . . . 8
⊢ 𝑥 ∈ V | 
| 3 | 2 | elpr 4649 | . . . . . . 7
⊢ (𝑥 ∈ {𝑆, {𝒫 ∪
𝑆}} ↔ (𝑥 = 𝑆 ∨ 𝑥 = {𝒫 ∪
𝑆})) | 
| 4 |  | vex 3483 | . . . . . . . 8
⊢ 𝑦 ∈ V | 
| 5 | 4 | elpr 4649 | . . . . . . 7
⊢ (𝑦 ∈ {𝑆, {𝒫 ∪
𝑆}} ↔ (𝑦 = 𝑆 ∨ 𝑦 = {𝒫 ∪
𝑆})) | 
| 6 |  | eqtr3 2762 | . . . . . . . . 9
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑆) → 𝑥 = 𝑦) | 
| 7 | 6 | orcd 873 | . . . . . . . 8
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = 𝑆) → (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | 
| 8 |  | ineq12 4214 | . . . . . . . . . 10
⊢ ((𝑥 = {𝒫 ∪ 𝑆}
∧ 𝑦 = 𝑆) → (𝑥 ∩ 𝑦) = ({𝒫 ∪
𝑆} ∩ 𝑆)) | 
| 9 |  | incom 4208 | . . . . . . . . . . 11
⊢
({𝒫 ∪ 𝑆} ∩ 𝑆) = (𝑆 ∩ {𝒫 ∪ 𝑆}) | 
| 10 |  | pwuninel 8301 | . . . . . . . . . . . 12
⊢  ¬
𝒫 ∪ 𝑆 ∈ 𝑆 | 
| 11 |  | disjsn 4710 | . . . . . . . . . . . 12
⊢ ((𝑆 ∩ {𝒫 ∪ 𝑆})
= ∅ ↔ ¬ 𝒫 ∪ 𝑆 ∈ 𝑆) | 
| 12 | 10, 11 | mpbir 231 | . . . . . . . . . . 11
⊢ (𝑆 ∩ {𝒫 ∪ 𝑆})
= ∅ | 
| 13 | 9, 12 | eqtri 2764 | . . . . . . . . . 10
⊢
({𝒫 ∪ 𝑆} ∩ 𝑆) = ∅ | 
| 14 | 8, 13 | eqtrdi 2792 | . . . . . . . . 9
⊢ ((𝑥 = {𝒫 ∪ 𝑆}
∧ 𝑦 = 𝑆) → (𝑥 ∩ 𝑦) = ∅) | 
| 15 | 14 | olcd 874 | . . . . . . . 8
⊢ ((𝑥 = {𝒫 ∪ 𝑆}
∧ 𝑦 = 𝑆) → (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | 
| 16 |  | ineq12 4214 | . . . . . . . . . 10
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = {𝒫 ∪
𝑆}) → (𝑥 ∩ 𝑦) = (𝑆 ∩ {𝒫 ∪ 𝑆})) | 
| 17 | 16, 12 | eqtrdi 2792 | . . . . . . . . 9
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = {𝒫 ∪
𝑆}) → (𝑥 ∩ 𝑦) = ∅) | 
| 18 | 17 | olcd 874 | . . . . . . . 8
⊢ ((𝑥 = 𝑆 ∧ 𝑦 = {𝒫 ∪
𝑆}) → (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | 
| 19 |  | eqtr3 2762 | . . . . . . . . 9
⊢ ((𝑥 = {𝒫 ∪ 𝑆}
∧ 𝑦 = {𝒫 ∪ 𝑆})
→ 𝑥 = 𝑦) | 
| 20 | 19 | orcd 873 | . . . . . . . 8
⊢ ((𝑥 = {𝒫 ∪ 𝑆}
∧ 𝑦 = {𝒫 ∪ 𝑆})
→ (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | 
| 21 | 7, 15, 18, 20 | ccase 1037 | . . . . . . 7
⊢ (((𝑥 = 𝑆 ∨ 𝑥 = {𝒫 ∪
𝑆}) ∧ (𝑦 = 𝑆 ∨ 𝑦 = {𝒫 ∪
𝑆})) → (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | 
| 22 | 3, 5, 21 | syl2anb 598 | . . . . . 6
⊢ ((𝑥 ∈ {𝑆, {𝒫 ∪
𝑆}} ∧ 𝑦 ∈ {𝑆, {𝒫 ∪
𝑆}}) → (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) | 
| 23 | 22 | rgen2 3198 | . . . . 5
⊢
∀𝑥 ∈
{𝑆, {𝒫 ∪ 𝑆}}∀𝑦 ∈ {𝑆, {𝒫 ∪
𝑆}} (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅) | 
| 24 |  | baspartn 22962 | . . . . 5
⊢ (({𝑆, {𝒫 ∪ 𝑆}}
∈ V ∧ ∀𝑥
∈ {𝑆, {𝒫 ∪ 𝑆}}∀𝑦 ∈ {𝑆, {𝒫 ∪
𝑆}} (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → {𝑆, {𝒫 ∪
𝑆}} ∈
TopBases) | 
| 25 | 1, 23, 24 | mp2an 692 | . . . 4
⊢ {𝑆, {𝒫 ∪ 𝑆}}
∈ TopBases | 
| 26 |  | tgcl 22977 | . . . 4
⊢ ({𝑆, {𝒫 ∪ 𝑆}}
∈ TopBases → (topGen‘{𝑆, {𝒫 ∪
𝑆}}) ∈
Top) | 
| 27 | 25, 26 | mp1i 13 | . . 3
⊢ (𝑆 ∈ 𝑉 → (topGen‘{𝑆, {𝒫 ∪
𝑆}}) ∈
Top) | 
| 28 |  | prfi 9364 | . . . . . 6
⊢ {𝑆, {𝒫 ∪ 𝑆}}
∈ Fin | 
| 29 |  | pwfi 9358 | . . . . . 6
⊢ ({𝑆, {𝒫 ∪ 𝑆}}
∈ Fin ↔ 𝒫 {𝑆, {𝒫 ∪
𝑆}} ∈
Fin) | 
| 30 | 28, 29 | mpbi 230 | . . . . 5
⊢ 𝒫
{𝑆, {𝒫 ∪ 𝑆}}
∈ Fin | 
| 31 |  | tgdom 22986 | . . . . . 6
⊢ ({𝑆, {𝒫 ∪ 𝑆}}
∈ V → (topGen‘{𝑆, {𝒫 ∪
𝑆}}) ≼ 𝒫
{𝑆, {𝒫 ∪ 𝑆}}) | 
| 32 | 1, 31 | ax-mp 5 | . . . . 5
⊢
(topGen‘{𝑆,
{𝒫 ∪ 𝑆}}) ≼ 𝒫 {𝑆, {𝒫 ∪
𝑆}} | 
| 33 |  | domfi 9230 | . . . . 5
⊢
((𝒫 {𝑆,
{𝒫 ∪ 𝑆}} ∈ Fin ∧ (topGen‘{𝑆, {𝒫 ∪ 𝑆}})
≼ 𝒫 {𝑆,
{𝒫 ∪ 𝑆}}) → (topGen‘{𝑆, {𝒫 ∪
𝑆}}) ∈
Fin) | 
| 34 | 30, 32, 33 | mp2an 692 | . . . 4
⊢
(topGen‘{𝑆,
{𝒫 ∪ 𝑆}}) ∈ Fin | 
| 35 | 34 | a1i 11 | . . 3
⊢ (𝑆 ∈ 𝑉 → (topGen‘{𝑆, {𝒫 ∪
𝑆}}) ∈
Fin) | 
| 36 | 27, 35 | elind 4199 | . 2
⊢ (𝑆 ∈ 𝑉 → (topGen‘{𝑆, {𝒫 ∪
𝑆}}) ∈ (Top ∩
Fin)) | 
| 37 |  | fincmp 23402 | . 2
⊢
((topGen‘{𝑆,
{𝒫 ∪ 𝑆}}) ∈ (Top ∩ Fin) →
(topGen‘{𝑆,
{𝒫 ∪ 𝑆}}) ∈ Comp) | 
| 38 | 36, 37 | syl 17 | 1
⊢ (𝑆 ∈ 𝑉 → (topGen‘{𝑆, {𝒫 ∪
𝑆}}) ∈
Comp) |