Step | Hyp | Ref
| Expression |
1 | | elssuni 4690 |
. . . . . 6
⊢ (𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽) |
2 | | ufildr.1 |
. . . . . . . . . 10
⊢ 𝐽 = (𝐹 ∪ {∅}) |
3 | 2 | unieqi 4668 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ (𝐹 ∪ {∅}) |
4 | | uniun 4680 |
. . . . . . . . . 10
⊢ ∪ (𝐹
∪ {∅}) = (∪ 𝐹 ∪ ∪
{∅}) |
5 | | 0ex 5015 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
6 | 5 | unisn 4675 |
. . . . . . . . . . 11
⊢ ∪ {∅} = ∅ |
7 | 6 | uneq2i 3992 |
. . . . . . . . . 10
⊢ (∪ 𝐹
∪ ∪ {∅}) = (∪
𝐹 ∪
∅) |
8 | | un0 4193 |
. . . . . . . . . 10
⊢ (∪ 𝐹
∪ ∅) = ∪ 𝐹 |
9 | 4, 7, 8 | 3eqtri 2854 |
. . . . . . . . 9
⊢ ∪ (𝐹
∪ {∅}) = ∪ 𝐹 |
10 | 3, 9 | eqtr2i 2851 |
. . . . . . . 8
⊢ ∪ 𝐹 =
∪ 𝐽 |
11 | | ufilfil 22079 |
. . . . . . . . 9
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
12 | | filunibas 22056 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 =
𝑋) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (UFil‘𝑋) → ∪ 𝐹 =
𝑋) |
14 | 10, 13 | syl5reqr 2877 |
. . . . . . 7
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝑋 = ∪ 𝐽) |
15 | 14 | sseq2d 3859 |
. . . . . 6
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ⊆ 𝑋 ↔ 𝑥 ⊆ ∪ 𝐽)) |
16 | 1, 15 | syl5ibr 238 |
. . . . 5
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝐽 → 𝑥 ⊆ 𝑋)) |
17 | | eqid 2826 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
18 | 17 | cldss 21205 |
. . . . . 6
⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽) |
19 | 18, 15 | syl5ibr 238 |
. . . . 5
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ 𝑋)) |
20 | 16, 19 | jaod 892 |
. . . 4
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ 𝑋)) |
21 | | ufilss 22080 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
22 | | ssun1 4004 |
. . . . . . . . . 10
⊢ 𝐹 ⊆ (𝐹 ∪ {∅}) |
23 | 22, 2 | sseqtr4i 3864 |
. . . . . . . . 9
⊢ 𝐹 ⊆ 𝐽 |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ 𝐽) |
25 | 24 | sseld 3827 |
. . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 → 𝑥 ∈ 𝐽)) |
26 | 24 | sseld 3827 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → (𝑋 ∖ 𝑥) ∈ 𝐽)) |
27 | | filconn 22058 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {∅}) ∈
Conn) |
28 | | conntop 21592 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∪ {∅}) ∈ Conn
→ (𝐹 ∪ {∅})
∈ Top) |
29 | 11, 27, 28 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐹 ∪ {∅}) ∈
Top) |
30 | 2, 29 | syl5eqel 2911 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐽 ∈ Top) |
31 | 30 | adantr 474 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝐽 ∈ Top) |
32 | 15 | biimpa 470 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝑥 ⊆ ∪ 𝐽) |
33 | 17 | iscld2 21204 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽)
→ (𝑥 ∈
(Clsd‘𝐽) ↔
(∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
34 | 31, 32, 33 | syl2anc 581 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ (Clsd‘𝐽) ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
35 | 14 | difeq1d 3955 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑋 ∖ 𝑥) = (∪ 𝐽 ∖ 𝑥)) |
36 | 35 | eleq1d 2892 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
37 | 36 | adantr 474 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
38 | 34, 37 | bitr4d 274 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑥) ∈ 𝐽)) |
39 | 26, 38 | sylibrd 251 |
. . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → 𝑥 ∈ (Clsd‘𝐽))) |
40 | 25, 39 | orim12d 994 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹) → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)))) |
41 | 21, 40 | mpd 15 |
. . . . 5
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽))) |
42 | 41 | ex 403 |
. . . 4
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)))) |
43 | 20, 42 | impbid 204 |
. . 3
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)) ↔ 𝑥 ⊆ 𝑋)) |
44 | | elun 3981 |
. . 3
⊢ (𝑥 ∈ (𝐽 ∪ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽))) |
45 | | selpw 4386 |
. . 3
⊢ (𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋) |
46 | 43, 44, 45 | 3bitr4g 306 |
. 2
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ (𝐽 ∪ (Clsd‘𝐽)) ↔ 𝑥 ∈ 𝒫 𝑋)) |
47 | 46 | eqrdv 2824 |
1
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐽 ∪ (Clsd‘𝐽)) = 𝒫 𝑋) |