Step | Hyp | Ref
| Expression |
1 | | elssuni 4830 |
. . . . . 6
⊢ (𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽) |
2 | | ufildr.1 |
. . . . . . . . . 10
⊢ 𝐽 = (𝐹 ∪ {∅}) |
3 | 2 | unieqi 4813 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ (𝐹 ∪ {∅}) |
4 | | uniun 4823 |
. . . . . . . . . 10
⊢ ∪ (𝐹
∪ {∅}) = (∪ 𝐹 ∪ ∪
{∅}) |
5 | | 0ex 5175 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
6 | 5 | unisn 4820 |
. . . . . . . . . . 11
⊢ ∪ {∅} = ∅ |
7 | 6 | uneq2i 4087 |
. . . . . . . . . 10
⊢ (∪ 𝐹
∪ ∪ {∅}) = (∪
𝐹 ∪
∅) |
8 | | un0 4298 |
. . . . . . . . . 10
⊢ (∪ 𝐹
∪ ∅) = ∪ 𝐹 |
9 | 4, 7, 8 | 3eqtri 2825 |
. . . . . . . . 9
⊢ ∪ (𝐹
∪ {∅}) = ∪ 𝐹 |
10 | 3, 9 | eqtr2i 2822 |
. . . . . . . 8
⊢ ∪ 𝐹 =
∪ 𝐽 |
11 | | ufilfil 22509 |
. . . . . . . . 9
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
12 | | filunibas 22486 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 =
𝑋) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (UFil‘𝑋) → ∪ 𝐹 =
𝑋) |
14 | 10, 13 | syl5reqr 2848 |
. . . . . . 7
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝑋 = ∪ 𝐽) |
15 | 14 | sseq2d 3947 |
. . . . . 6
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ⊆ 𝑋 ↔ 𝑥 ⊆ ∪ 𝐽)) |
16 | 1, 15 | syl5ibr 249 |
. . . . 5
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝐽 → 𝑥 ⊆ 𝑋)) |
17 | | eqid 2798 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
18 | 17 | cldss 21634 |
. . . . . 6
⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽) |
19 | 18, 15 | syl5ibr 249 |
. . . . 5
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ 𝑋)) |
20 | 16, 19 | jaod 856 |
. . . 4
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ 𝑋)) |
21 | | ufilss 22510 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
22 | | ssun1 4099 |
. . . . . . . . . 10
⊢ 𝐹 ⊆ (𝐹 ∪ {∅}) |
23 | 22, 2 | sseqtrri 3952 |
. . . . . . . . 9
⊢ 𝐹 ⊆ 𝐽 |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ 𝐽) |
25 | 24 | sseld 3914 |
. . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 → 𝑥 ∈ 𝐽)) |
26 | 24 | sseld 3914 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → (𝑋 ∖ 𝑥) ∈ 𝐽)) |
27 | | filconn 22488 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {∅}) ∈
Conn) |
28 | | conntop 22022 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∪ {∅}) ∈ Conn
→ (𝐹 ∪ {∅})
∈ Top) |
29 | 11, 27, 28 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐹 ∪ {∅}) ∈
Top) |
30 | 2, 29 | eqeltrid 2894 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐽 ∈ Top) |
31 | 15 | biimpa 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝑥 ⊆ ∪ 𝐽) |
32 | 17 | iscld2 21633 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽)
→ (𝑥 ∈
(Clsd‘𝐽) ↔
(∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
33 | 30, 31, 32 | syl2an2r 684 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ (Clsd‘𝐽) ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
34 | 14 | difeq1d 4049 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑋 ∖ 𝑥) = (∪ 𝐽 ∖ 𝑥)) |
35 | 34 | eleq1d 2874 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
36 | 35 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
37 | 33, 36 | bitr4d 285 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑥) ∈ 𝐽)) |
38 | 26, 37 | sylibrd 262 |
. . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → 𝑥 ∈ (Clsd‘𝐽))) |
39 | 25, 38 | orim12d 962 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹) → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)))) |
40 | 21, 39 | mpd 15 |
. . . . 5
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽))) |
41 | 40 | ex 416 |
. . . 4
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)))) |
42 | 20, 41 | impbid 215 |
. . 3
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)) ↔ 𝑥 ⊆ 𝑋)) |
43 | | elun 4076 |
. . 3
⊢ (𝑥 ∈ (𝐽 ∪ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽))) |
44 | | velpw 4502 |
. . 3
⊢ (𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋) |
45 | 42, 43, 44 | 3bitr4g 317 |
. 2
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ (𝐽 ∪ (Clsd‘𝐽)) ↔ 𝑥 ∈ 𝒫 𝑋)) |
46 | 45 | eqrdv 2796 |
1
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐽 ∪ (Clsd‘𝐽)) = 𝒫 𝑋) |