Step | Hyp | Ref
| Expression |
1 | | elssuni 4403 |
. . . . . 6
⊢ (𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽) |
2 | | ufildr.1 |
. . . . . . . . . 10
⊢ 𝐽 = (𝐹 ∪ {∅}) |
3 | 2 | unieqi 4381 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ (𝐹 ∪ {∅}) |
4 | | uniun 4392 |
. . . . . . . . . 10
⊢ ∪ (𝐹
∪ {∅}) = (∪ 𝐹 ∪ ∪
{∅}) |
5 | | 0ex 4718 |
. . . . . . . . . . . 12
⊢ ∅
∈ V |
6 | 5 | unisn 4387 |
. . . . . . . . . . 11
⊢ ∪ {∅} = ∅ |
7 | 6 | uneq2i 3726 |
. . . . . . . . . 10
⊢ (∪ 𝐹
∪ ∪ {∅}) = (∪
𝐹 ∪
∅) |
8 | | un0 3919 |
. . . . . . . . . 10
⊢ (∪ 𝐹
∪ ∅) = ∪ 𝐹 |
9 | 4, 7, 8 | 3eqtri 2636 |
. . . . . . . . 9
⊢ ∪ (𝐹
∪ {∅}) = ∪ 𝐹 |
10 | 3, 9 | eqtr2i 2633 |
. . . . . . . 8
⊢ ∪ 𝐹 =
∪ 𝐽 |
11 | | ufilfil 21518 |
. . . . . . . . 9
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
12 | | filunibas 21495 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 =
𝑋) |
13 | 11, 12 | syl 17 |
. . . . . . . 8
⊢ (𝐹 ∈ (UFil‘𝑋) → ∪ 𝐹 =
𝑋) |
14 | 10, 13 | syl5reqr 2659 |
. . . . . . 7
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝑋 = ∪ 𝐽) |
15 | 14 | sseq2d 3596 |
. . . . . 6
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ⊆ 𝑋 ↔ 𝑥 ⊆ ∪ 𝐽)) |
16 | 1, 15 | syl5ibr 235 |
. . . . 5
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ 𝐽 → 𝑥 ⊆ 𝑋)) |
17 | | eqid 2610 |
. . . . . . 7
⊢ ∪ 𝐽 =
∪ 𝐽 |
18 | 17 | cldss 20643 |
. . . . . 6
⊢ (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ ∪ 𝐽) |
19 | 18, 15 | syl5ibr 235 |
. . . . 5
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ (Clsd‘𝐽) → 𝑥 ⊆ 𝑋)) |
20 | 16, 19 | jaod 394 |
. . . 4
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ⊆ 𝑋)) |
21 | | ufilss 21519 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹)) |
22 | | ssun1 3738 |
. . . . . . . . . 10
⊢ 𝐹 ⊆ (𝐹 ∪ {∅}) |
23 | 22, 2 | sseqtr4i 3601 |
. . . . . . . . 9
⊢ 𝐹 ⊆ 𝐽 |
24 | 23 | a1i 11 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝐹 ⊆ 𝐽) |
25 | 24 | sseld 3567 |
. . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐹 → 𝑥 ∈ 𝐽)) |
26 | 24 | sseld 3567 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → (𝑋 ∖ 𝑥) ∈ 𝐽)) |
27 | | filcon 21497 |
. . . . . . . . . . . . 13
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {∅}) ∈
Con) |
28 | | contop 21030 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∪ {∅}) ∈ Con
→ (𝐹 ∪ {∅})
∈ Top) |
29 | 11, 27, 28 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐹 ∪ {∅}) ∈
Top) |
30 | 2, 29 | syl5eqel 2692 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (UFil‘𝑋) → 𝐽 ∈ Top) |
31 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝐽 ∈ Top) |
32 | 15 | biimpa 500 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → 𝑥 ⊆ ∪ 𝐽) |
33 | 17 | iscld2 20642 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽)
→ (𝑥 ∈
(Clsd‘𝐽) ↔
(∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
34 | 31, 32, 33 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ (Clsd‘𝐽) ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
35 | 14 | difeq1d 3689 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑋 ∖ 𝑥) = (∪ 𝐽 ∖ 𝑥)) |
36 | 35 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
37 | 36 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐽 ↔ (∪ 𝐽 ∖ 𝑥) ∈ 𝐽)) |
38 | 34, 37 | bitr4d 270 |
. . . . . . . 8
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ (Clsd‘𝐽) ↔ (𝑋 ∖ 𝑥) ∈ 𝐽)) |
39 | 26, 38 | sylibrd 248 |
. . . . . . 7
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑋 ∖ 𝑥) ∈ 𝐹 → 𝑥 ∈ (Clsd‘𝐽))) |
40 | 25, 39 | orim12d 879 |
. . . . . 6
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → ((𝑥 ∈ 𝐹 ∨ (𝑋 ∖ 𝑥) ∈ 𝐹) → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)))) |
41 | 21, 40 | mpd 15 |
. . . . 5
⊢ ((𝐹 ∈ (UFil‘𝑋) ∧ 𝑥 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽))) |
42 | 41 | ex 449 |
. . . 4
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ⊆ 𝑋 → (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)))) |
43 | 20, 42 | impbid 201 |
. . 3
⊢ (𝐹 ∈ (UFil‘𝑋) → ((𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽)) ↔ 𝑥 ⊆ 𝑋)) |
44 | | elun 3715 |
. . 3
⊢ (𝑥 ∈ (𝐽 ∪ (Clsd‘𝐽)) ↔ (𝑥 ∈ 𝐽 ∨ 𝑥 ∈ (Clsd‘𝐽))) |
45 | | selpw 4115 |
. . 3
⊢ (𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋) |
46 | 43, 44, 45 | 3bitr4g 302 |
. 2
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝑥 ∈ (𝐽 ∪ (Clsd‘𝐽)) ↔ 𝑥 ∈ 𝒫 𝑋)) |
47 | 46 | eqrdv 2608 |
1
⊢ (𝐹 ∈ (UFil‘𝑋) → (𝐽 ∪ (Clsd‘𝐽)) = 𝒫 𝑋) |