Step | Hyp | Ref
| Expression |
1 | | elssuni 4868 |
. . . . . 6
⊢ (𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽) |
2 | | ufildr.1 |
. . . . . . . . . 10
⊢ 𝐽 = (𝐹 ∪ {∅}) |
3 | 2 | unieqi 4851 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ (𝐹 ∪ {∅}) |
4 | | uniun 4861 |
. . . . . . . . . 10
⊢ ∪ (𝐹
∪ {∅}) = (∪ 𝐹 ∪ ∪
{∅}) |
5 | | 0ex 5211 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
6 | 5 | unisn 4858 |
. . . . . . . . . . 11
⊢ ∪ {∅} = ∅ |
7 | 6 | uneq2i 4136 |
. . . . . . . . . 10
⊢ (∪ 𝐹
∪ ∪ {∅}) = (∪
𝐹 ∪
∅) |
8 | | un0 4344 |
. . . . . . . . . 10
⊢ (∪ 𝐹
∪ ∅) = ∪ 𝐹 |
9 | 4, 7, 8 | 3eqtri 2848 |
. . . . . . . . 9
⊢ ∪ (𝐹
∪ {∅}) = ∪ 𝐹 |
10 | 3, 9 | eqtr2i 2845 |
. . . . . . . 8
⊢ ∪ 𝐹 =
∪ 𝐽 |
11 | | ufilfil 22512 |
. . . . . . . . 9
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
12 | | filunibas 22489 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 =
𝑋) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (UFil‘𝑋) → ∪ 𝐹 =
𝑋) |
14 | 10, 13 | syl5reqr 2871 |
. . . . . . 7
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝑋 = ∪ 𝐽) |
15 | 14 | sseq2d 3999 |
. . . . . 6
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ⊆ 𝑋 ↔ 𝑥 ⊆ ∪ 𝐽)) |
16 | 1, 15 | syl5ibr 248 |
. . . . 5
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝐽 → 𝑥 ⊆ 𝑋)) |
17 | | eqid 2821 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
18 | 17 | cldss 21637 |
. . . . . 6
⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽) |
19 | 18, 15 | syl5ibr 248 |
. . . . 5
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ 𝑋)) |
20 | 16, 19 | jaod 855 |
. . . 4
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ 𝑋)) |
21 | | ufilss 22513 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
22 | | ssun1 4148 |
. . . . . . . . . 10
⊢ 𝐹 ⊆ (𝐹 ∪ {∅}) |
23 | 22, 2 | sseqtrri 4004 |
. . . . . . . . 9
⊢ 𝐹 ⊆ 𝐽 |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ 𝐽) |
25 | 24 | sseld 3966 |
. . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 → 𝑥 ∈ 𝐽)) |
26 | 24 | sseld 3966 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → (𝑋 ∖ 𝑥) ∈ 𝐽)) |
27 | | filconn 22491 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {∅}) ∈
Conn) |
28 | | conntop 22025 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∪ {∅}) ∈ Conn
→ (𝐹 ∪ {∅})
∈ Top) |
29 | 11, 27, 28 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐹 ∪ {∅}) ∈
Top) |
30 | 2, 29 | eqeltrid 2917 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐽 ∈ Top) |
31 | 15 | biimpa 479 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝑥 ⊆ ∪ 𝐽) |
32 | 17 | iscld2 21636 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽)
→ (𝑥 ∈
(Clsd‘𝐽) ↔
(∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
33 | 30, 31, 32 | syl2an2r 683 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ (Clsd‘𝐽) ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
34 | 14 | difeq1d 4098 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑋 ∖ 𝑥) = (∪ 𝐽 ∖ 𝑥)) |
35 | 34 | eleq1d 2897 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
36 | 35 | adantr 483 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
37 | 33, 36 | bitr4d 284 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑥) ∈ 𝐽)) |
38 | 26, 37 | sylibrd 261 |
. . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → 𝑥 ∈ (Clsd‘𝐽))) |
39 | 25, 38 | orim12d 961 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹) → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)))) |
40 | 21, 39 | mpd 15 |
. . . . 5
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽))) |
41 | 40 | ex 415 |
. . . 4
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)))) |
42 | 20, 41 | impbid 214 |
. . 3
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)) ↔ 𝑥 ⊆ 𝑋)) |
43 | | elun 4125 |
. . 3
⊢ (𝑥 ∈ (𝐽 ∪ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽))) |
44 | | velpw 4544 |
. . 3
⊢ (𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋) |
45 | 42, 43, 44 | 3bitr4g 316 |
. 2
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ (𝐽 ∪ (Clsd‘𝐽)) ↔ 𝑥 ∈ 𝒫 𝑋)) |
46 | 45 | eqrdv 2819 |
1
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐽 ∪ (Clsd‘𝐽)) = 𝒫 𝑋) |