| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elssuni 4936 | . . . . . 6
⊢ (𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽) | 
| 2 |  | ufilfil 23913 | . . . . . . . . 9
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) | 
| 3 |  | filunibas 23890 | . . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 =
𝑋) | 
| 4 | 2, 3 | syl 17 | . . . . . . . 8
⊢ (𝐹 ∈ (UFil‘𝑋) → ∪ 𝐹 =
𝑋) | 
| 5 |  | ufildr.1 | . . . . . . . . . 10
⊢ 𝐽 = (𝐹 ∪ {∅}) | 
| 6 | 5 | unieqi 4918 | . . . . . . . . 9
⊢ ∪ 𝐽 =
∪ (𝐹 ∪ {∅}) | 
| 7 |  | uniun 4929 | . . . . . . . . . 10
⊢ ∪ (𝐹
∪ {∅}) = (∪ 𝐹 ∪ ∪
{∅}) | 
| 8 |  | 0ex 5306 | . . . . . . . . . . . 12
⊢ ∅
∈ V | 
| 9 | 8 | unisn 4925 | . . . . . . . . . . 11
⊢ ∪ {∅} = ∅ | 
| 10 | 9 | uneq2i 4164 | . . . . . . . . . 10
⊢ (∪ 𝐹
∪ ∪ {∅}) = (∪
𝐹 ∪
∅) | 
| 11 |  | un0 4393 | . . . . . . . . . 10
⊢ (∪ 𝐹
∪ ∅) = ∪ 𝐹 | 
| 12 | 7, 10, 11 | 3eqtri 2768 | . . . . . . . . 9
⊢ ∪ (𝐹
∪ {∅}) = ∪ 𝐹 | 
| 13 | 6, 12 | eqtr2i 2765 | . . . . . . . 8
⊢ ∪ 𝐹 =
∪ 𝐽 | 
| 14 | 4, 13 | eqtr3di 2791 | . . . . . . 7
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝑋 = ∪ 𝐽) | 
| 15 | 14 | sseq2d 4015 | . . . . . 6
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ⊆ 𝑋 ↔ 𝑥 ⊆ ∪ 𝐽)) | 
| 16 | 1, 15 | imbitrrid 246 | . . . . 5
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝐽 → 𝑥 ⊆ 𝑋)) | 
| 17 |  | eqid 2736 | . . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 | 
| 18 | 17 | cldss 23038 | . . . . . 6
⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽) | 
| 19 | 18, 15 | imbitrrid 246 | . . . . 5
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ 𝑋)) | 
| 20 | 16, 19 | jaod 859 | . . . 4
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ 𝑋)) | 
| 21 |  | ufilss 23914 | . . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)) | 
| 22 |  | ssun1 4177 | . . . . . . . . . 10
⊢ 𝐹 ⊆ (𝐹 ∪ {∅}) | 
| 23 | 22, 5 | sseqtrri 4032 | . . . . . . . . 9
⊢ 𝐹 ⊆ 𝐽 | 
| 24 | 23 | a1i 11 | . . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ 𝐽) | 
| 25 | 24 | sseld 3981 | . . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 → 𝑥 ∈ 𝐽)) | 
| 26 | 24 | sseld 3981 | . . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → (𝑋 ∖ 𝑥) ∈ 𝐽)) | 
| 27 |  | filconn 23892 | . . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {∅}) ∈
Conn) | 
| 28 |  | conntop 23426 | . . . . . . . . . . . 12
⊢ ((𝐹 ∪ {∅}) ∈ Conn
→ (𝐹 ∪ {∅})
∈ Top) | 
| 29 | 2, 27, 28 | 3syl 18 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐹 ∪ {∅}) ∈
Top) | 
| 30 | 5, 29 | eqeltrid 2844 | . . . . . . . . . 10
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐽 ∈ Top) | 
| 31 | 15 | biimpa 476 | . . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝑥 ⊆ ∪ 𝐽) | 
| 32 | 17 | iscld2 23037 | . . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽)
→ (𝑥 ∈
(Clsd‘𝐽) ↔
(∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) | 
| 33 | 30, 31, 32 | syl2an2r 685 | . . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ (Clsd‘𝐽) ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) | 
| 34 | 14 | difeq1d 4124 | . . . . . . . . . . 11
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑋 ∖ 𝑥) = (∪ 𝐽 ∖ 𝑥)) | 
| 35 | 34 | eleq1d 2825 | . . . . . . . . . 10
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) | 
| 37 | 33, 36 | bitr4d 282 | . . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑥) ∈ 𝐽)) | 
| 38 | 26, 37 | sylibrd 259 | . . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → 𝑥 ∈ (Clsd‘𝐽))) | 
| 39 | 25, 38 | orim12d 966 | . . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹) → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)))) | 
| 40 | 21, 39 | mpd 15 | . . . . 5
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽))) | 
| 41 | 40 | ex 412 | . . . 4
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)))) | 
| 42 | 20, 41 | impbid 212 | . . 3
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)) ↔ 𝑥 ⊆ 𝑋)) | 
| 43 |  | elun 4152 | . . 3
⊢ (𝑥 ∈ (𝐽 ∪ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽))) | 
| 44 |  | velpw 4604 | . . 3
⊢ (𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋) | 
| 45 | 42, 43, 44 | 3bitr4g 314 | . 2
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ (𝐽 ∪ (Clsd‘𝐽)) ↔ 𝑥 ∈ 𝒫 𝑋)) | 
| 46 | 45 | eqrdv 2734 | 1
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐽 ∪ (Clsd‘𝐽)) = 𝒫 𝑋) |