Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (Fil‘𝑋)) |
2 | | filunibas 22778 |
. . . 4
⊢ (𝐹 ∈ (Fil‘𝑋) → ∪ 𝐹 =
𝑋) |
3 | 2 | fveq2d 6721 |
. . 3
⊢ (𝐹 ∈ (Fil‘𝑋) → (Fil‘∪ 𝐹) =
(Fil‘𝑋)) |
4 | 1, 3 | eleqtrrd 2841 |
. 2
⊢ (𝐹 ∈ (Fil‘𝑋) → 𝐹 ∈ (Fil‘∪ 𝐹)) |
5 | | nss 3963 |
. . . . . . . 8
⊢ (¬
𝑥 ⊆ {∅} ↔
∃𝑦(𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ {∅})) |
6 | | simpll 767 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ (𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ {∅})) → 𝐹 ∈ (Fil‘∪ 𝐹)) |
7 | | ssel2 3895 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ⊆ (𝐹 ∪ {∅}) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (𝐹 ∪ {∅})) |
8 | 7 | adantll 714 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ (𝐹 ∪ {∅})) |
9 | | elun 4063 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ (𝐹 ∪ {∅}) ↔ (𝑦 ∈ 𝐹 ∨ 𝑦 ∈ {∅})) |
10 | 8, 9 | sylib 221 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∈ 𝐹 ∨ 𝑦 ∈ {∅})) |
11 | 10 | orcomd 871 |
. . . . . . . . . . . . . 14
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ 𝑦 ∈ 𝑥) → (𝑦 ∈ {∅} ∨ 𝑦 ∈ 𝐹)) |
12 | 11 | ord 864 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ 𝑦 ∈ 𝑥) → (¬ 𝑦 ∈ {∅} → 𝑦 ∈ 𝐹)) |
13 | 12 | impr 458 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ (𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ {∅})) → 𝑦 ∈ 𝐹) |
14 | | uniss 4827 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊆ (𝐹 ∪ {∅}) → ∪ 𝑥
⊆ ∪ (𝐹 ∪ {∅})) |
15 | 14 | ad2antlr 727 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ (𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ {∅})) → ∪ 𝑥
⊆ ∪ (𝐹 ∪ {∅})) |
16 | | uniun 4844 |
. . . . . . . . . . . . . 14
⊢ ∪ (𝐹
∪ {∅}) = (∪ 𝐹 ∪ ∪
{∅}) |
17 | | 0ex 5200 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ V |
18 | 17 | unisn 4841 |
. . . . . . . . . . . . . . 15
⊢ ∪ {∅} = ∅ |
19 | 18 | uneq2i 4074 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝐹
∪ ∪ {∅}) = (∪
𝐹 ∪
∅) |
20 | | un0 4305 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝐹
∪ ∅) = ∪ 𝐹 |
21 | 16, 19, 20 | 3eqtrri 2770 |
. . . . . . . . . . . . 13
⊢ ∪ 𝐹 =
∪ (𝐹 ∪ {∅}) |
22 | 15, 21 | sseqtrrdi 3952 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ (𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ {∅})) → ∪ 𝑥
⊆ ∪ 𝐹) |
23 | | elssuni 4851 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ 𝑥 → 𝑦 ⊆ ∪ 𝑥) |
24 | 23 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ (𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ {∅})) → 𝑦 ⊆ ∪ 𝑥) |
25 | | filss 22750 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ (𝑦 ∈ 𝐹 ∧ ∪ 𝑥
⊆ ∪ 𝐹 ∧ 𝑦 ⊆ ∪ 𝑥)) → ∪ 𝑥
∈ 𝐹) |
26 | 6, 13, 22, 24, 25 | syl13anc 1374 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ (𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ {∅})) → ∪ 𝑥
∈ 𝐹) |
27 | | elun1 4090 |
. . . . . . . . . . 11
⊢ (∪ 𝑥
∈ 𝐹 → ∪ 𝑥
∈ (𝐹 ∪
{∅})) |
28 | 26, 27 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) ∧ (𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ {∅})) → ∪ 𝑥
∈ (𝐹 ∪
{∅})) |
29 | 28 | ex 416 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) →
((𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ {∅}) → ∪ 𝑥
∈ (𝐹 ∪
{∅}))) |
30 | 29 | exlimdv 1941 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) →
(∃𝑦(𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ {∅}) → ∪ 𝑥
∈ (𝐹 ∪
{∅}))) |
31 | 5, 30 | syl5bi 245 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) → (¬
𝑥 ⊆ {∅} →
∪ 𝑥 ∈ (𝐹 ∪ {∅}))) |
32 | | uni0b 4847 |
. . . . . . . 8
⊢ (∪ 𝑥 =
∅ ↔ 𝑥 ⊆
{∅}) |
33 | | ssun2 4087 |
. . . . . . . . . 10
⊢ {∅}
⊆ (𝐹 ∪
{∅}) |
34 | 17 | snid 4577 |
. . . . . . . . . 10
⊢ ∅
∈ {∅} |
35 | 33, 34 | sselii 3897 |
. . . . . . . . 9
⊢ ∅
∈ (𝐹 ∪
{∅}) |
36 | | eleq1 2825 |
. . . . . . . . 9
⊢ (∪ 𝑥 =
∅ → (∪ 𝑥 ∈ (𝐹 ∪ {∅}) ↔ ∅ ∈
(𝐹 ∪
{∅}))) |
37 | 35, 36 | mpbiri 261 |
. . . . . . . 8
⊢ (∪ 𝑥 =
∅ → ∪ 𝑥 ∈ (𝐹 ∪ {∅})) |
38 | 32, 37 | sylbir 238 |
. . . . . . 7
⊢ (𝑥 ⊆ {∅} → ∪ 𝑥
∈ (𝐹 ∪
{∅})) |
39 | 31, 38 | pm2.61d2 184 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ⊆ (𝐹 ∪ {∅})) → ∪ 𝑥
∈ (𝐹 ∪
{∅})) |
40 | 39 | ex 416 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ (𝑥 ⊆ (𝐹 ∪ {∅}) → ∪ 𝑥
∈ (𝐹 ∪
{∅}))) |
41 | 40 | alrimiv 1935 |
. . . 4
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ ∀𝑥(𝑥 ⊆ (𝐹 ∪ {∅}) → ∪ 𝑥
∈ (𝐹 ∪
{∅}))) |
42 | | filin 22751 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 ∩ 𝑦) ∈ 𝐹) |
43 | | elun1 4090 |
. . . . . . . . . 10
⊢ ((𝑥 ∩ 𝑦) ∈ 𝐹 → (𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
45 | 44 | 3expa 1120 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ 𝐹) ∧ 𝑦 ∈ 𝐹) → (𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
46 | 45 | ralrimiva 3105 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ 𝐹) → ∀𝑦 ∈ 𝐹 (𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
47 | | elsni 4558 |
. . . . . . . . 9
⊢ (𝑦 ∈ {∅} → 𝑦 = ∅) |
48 | | ineq2 4121 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → (𝑥 ∩ 𝑦) = (𝑥 ∩ ∅)) |
49 | | in0 4306 |
. . . . . . . . . . 11
⊢ (𝑥 ∩ ∅) =
∅ |
50 | 48, 49 | eqtrdi 2794 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → (𝑥 ∩ 𝑦) = ∅) |
51 | 50, 35 | eqeltrdi 2846 |
. . . . . . . . 9
⊢ (𝑦 = ∅ → (𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
52 | 47, 51 | syl 17 |
. . . . . . . 8
⊢ (𝑦 ∈ {∅} → (𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
53 | 52 | rgen 3071 |
. . . . . . 7
⊢
∀𝑦 ∈
{∅} (𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅}) |
54 | | ralun 4106 |
. . . . . . 7
⊢
((∀𝑦 ∈
𝐹 (𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅}) ∧ ∀𝑦 ∈ {∅} (𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) → ∀𝑦 ∈ (𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
55 | 46, 53, 54 | sylancl 589 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ 𝐹) → ∀𝑦 ∈ (𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
56 | 55 | ralrimiva 3105 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ ∀𝑥 ∈
𝐹 ∀𝑦 ∈ (𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
57 | | elsni 4558 |
. . . . . . 7
⊢ (𝑥 ∈ {∅} → 𝑥 = ∅) |
58 | | ineq1 4120 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → (𝑥 ∩ 𝑦) = (∅ ∩ 𝑦)) |
59 | | 0in 4308 |
. . . . . . . . . 10
⊢ (∅
∩ 𝑦) =
∅ |
60 | 58, 59 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝑥 ∩ 𝑦) = ∅) |
61 | 60, 35 | eqeltrdi 2846 |
. . . . . . . 8
⊢ (𝑥 = ∅ → (𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
62 | 61 | ralrimivw 3106 |
. . . . . . 7
⊢ (𝑥 = ∅ → ∀𝑦 ∈ (𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
63 | 57, 62 | syl 17 |
. . . . . 6
⊢ (𝑥 ∈ {∅} →
∀𝑦 ∈ (𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
64 | 63 | rgen 3071 |
. . . . 5
⊢
∀𝑥 ∈
{∅}∀𝑦 ∈
(𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅}) |
65 | | ralun 4106 |
. . . . 5
⊢
((∀𝑥 ∈
𝐹 ∀𝑦 ∈ (𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅}) ∧ ∀𝑥 ∈ {∅}∀𝑦 ∈ (𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) → ∀𝑥 ∈ (𝐹 ∪ {∅})∀𝑦 ∈ (𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
66 | 56, 64, 65 | sylancl 589 |
. . . 4
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ ∀𝑥 ∈
(𝐹 ∪
{∅})∀𝑦 ∈
(𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})) |
67 | | p0ex 5277 |
. . . . . 6
⊢ {∅}
∈ V |
68 | | unexg 7534 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ {∅} ∈ V) → (𝐹 ∪ {∅}) ∈ V) |
69 | 67, 68 | mpan2 691 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ (𝐹 ∪ {∅})
∈ V) |
70 | | istopg 21792 |
. . . . 5
⊢ ((𝐹 ∪ {∅}) ∈ V
→ ((𝐹 ∪ {∅})
∈ Top ↔ (∀𝑥(𝑥 ⊆ (𝐹 ∪ {∅}) → ∪ 𝑥
∈ (𝐹 ∪ {∅}))
∧ ∀𝑥 ∈
(𝐹 ∪
{∅})∀𝑦 ∈
(𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})))) |
71 | 69, 70 | syl 17 |
. . . 4
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ ((𝐹 ∪ {∅})
∈ Top ↔ (∀𝑥(𝑥 ⊆ (𝐹 ∪ {∅}) → ∪ 𝑥
∈ (𝐹 ∪ {∅}))
∧ ∀𝑥 ∈
(𝐹 ∪
{∅})∀𝑦 ∈
(𝐹 ∪ {∅})(𝑥 ∩ 𝑦) ∈ (𝐹 ∪ {∅})))) |
72 | 41, 66, 71 | mpbir2and 713 |
. . 3
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ (𝐹 ∪ {∅})
∈ Top) |
73 | 21 | cldopn 21928 |
. . . . . . . 8
⊢ (𝑥 ∈ (Clsd‘(𝐹 ∪ {∅})) → (∪ 𝐹
∖ 𝑥) ∈ (𝐹 ∪
{∅})) |
74 | | elun 4063 |
. . . . . . . 8
⊢ ((∪ 𝐹
∖ 𝑥) ∈ (𝐹 ∪ {∅}) ↔ ((∪ 𝐹
∖ 𝑥) ∈ 𝐹 ∨ (∪ 𝐹
∖ 𝑥) ∈
{∅})) |
75 | 73, 74 | sylib 221 |
. . . . . . 7
⊢ (𝑥 ∈ (Clsd‘(𝐹 ∪ {∅})) →
((∪ 𝐹 ∖ 𝑥) ∈ 𝐹 ∨ (∪ 𝐹 ∖ 𝑥) ∈ {∅})) |
76 | | elun 4063 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (𝐹 ∪ {∅}) ↔ (𝑥 ∈ 𝐹 ∨ 𝑥 ∈ {∅})) |
77 | | filfbas 22745 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ 𝐹 ∈
(fBas‘∪ 𝐹)) |
78 | | fbncp 22736 |
. . . . . . . . . . . . . 14
⊢ ((𝐹 ∈ (fBas‘∪ 𝐹)
∧ 𝑥 ∈ 𝐹) → ¬ (∪ 𝐹
∖ 𝑥) ∈ 𝐹) |
79 | 77, 78 | sylan 583 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ 𝐹) → ¬ (∪ 𝐹
∖ 𝑥) ∈ 𝐹) |
80 | 79 | pm2.21d 121 |
. . . . . . . . . . . 12
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ 𝐹) → ((∪ 𝐹
∖ 𝑥) ∈ 𝐹 → 𝑥 = ∅)) |
81 | 80 | ex 416 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ (𝑥 ∈ 𝐹 → ((∪ 𝐹
∖ 𝑥) ∈ 𝐹 → 𝑥 = ∅))) |
82 | 57 | a1i13 27 |
. . . . . . . . . . 11
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ (𝑥 ∈ {∅}
→ ((∪ 𝐹 ∖ 𝑥) ∈ 𝐹 → 𝑥 = ∅))) |
83 | 81, 82 | jaod 859 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ ((𝑥 ∈ 𝐹 ∨ 𝑥 ∈ {∅}) → ((∪ 𝐹
∖ 𝑥) ∈ 𝐹 → 𝑥 = ∅))) |
84 | 76, 83 | syl5bi 245 |
. . . . . . . . 9
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ (𝑥 ∈ (𝐹 ∪ {∅}) → ((∪ 𝐹
∖ 𝑥) ∈ 𝐹 → 𝑥 = ∅))) |
85 | 84 | imp 410 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ (𝐹 ∪ {∅})) →
((∪ 𝐹 ∖ 𝑥) ∈ 𝐹 → 𝑥 = ∅)) |
86 | | elsni 4558 |
. . . . . . . . 9
⊢ ((∪ 𝐹
∖ 𝑥) ∈ {∅}
→ (∪ 𝐹 ∖ 𝑥) = ∅) |
87 | | elssuni 4851 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (𝐹 ∪ {∅}) → 𝑥 ⊆ ∪ (𝐹 ∪
{∅})) |
88 | 87, 21 | sseqtrrdi 3952 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (𝐹 ∪ {∅}) → 𝑥 ⊆ ∪ 𝐹) |
89 | 88 | adantl 485 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ (𝐹 ∪ {∅})) → 𝑥 ⊆ ∪ 𝐹) |
90 | | ssdif0 4278 |
. . . . . . . . . . 11
⊢ (∪ 𝐹
⊆ 𝑥 ↔ (∪ 𝐹
∖ 𝑥) =
∅) |
91 | 90 | biimpri 231 |
. . . . . . . . . 10
⊢ ((∪ 𝐹
∖ 𝑥) = ∅ →
∪ 𝐹 ⊆ 𝑥) |
92 | | eqss 3916 |
. . . . . . . . . . 11
⊢ (𝑥 = ∪
𝐹 ↔ (𝑥 ⊆ ∪ 𝐹
∧ ∪ 𝐹 ⊆ 𝑥)) |
93 | 92 | simplbi2 504 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ ∪ 𝐹
→ (∪ 𝐹 ⊆ 𝑥 → 𝑥 = ∪ 𝐹)) |
94 | 89, 91, 93 | syl2im 40 |
. . . . . . . . 9
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ (𝐹 ∪ {∅})) →
((∪ 𝐹 ∖ 𝑥) = ∅ → 𝑥 = ∪ 𝐹)) |
95 | 86, 94 | syl5 34 |
. . . . . . . 8
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ (𝐹 ∪ {∅})) →
((∪ 𝐹 ∖ 𝑥) ∈ {∅} → 𝑥 = ∪ 𝐹)) |
96 | 85, 95 | orim12d 965 |
. . . . . . 7
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ (𝐹 ∪ {∅})) →
(((∪ 𝐹 ∖ 𝑥) ∈ 𝐹 ∨ (∪ 𝐹 ∖ 𝑥) ∈ {∅}) → (𝑥 = ∅ ∨ 𝑥 = ∪
𝐹))) |
97 | 75, 96 | syl5 34 |
. . . . . 6
⊢ ((𝐹 ∈ (Fil‘∪ 𝐹)
∧ 𝑥 ∈ (𝐹 ∪ {∅})) → (𝑥 ∈ (Clsd‘(𝐹 ∪ {∅})) → (𝑥 = ∅ ∨ 𝑥 = ∪
𝐹))) |
98 | 97 | expimpd 457 |
. . . . 5
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ ((𝑥 ∈ (𝐹 ∪ {∅}) ∧ 𝑥 ∈ (Clsd‘(𝐹 ∪ {∅}))) →
(𝑥 = ∅ ∨ 𝑥 = ∪
𝐹))) |
99 | | elin 3882 |
. . . . 5
⊢ (𝑥 ∈ ((𝐹 ∪ {∅}) ∩ (Clsd‘(𝐹 ∪ {∅}))) ↔
(𝑥 ∈ (𝐹 ∪ {∅}) ∧ 𝑥 ∈ (Clsd‘(𝐹 ∪
{∅})))) |
100 | | vex 3412 |
. . . . . 6
⊢ 𝑥 ∈ V |
101 | 100 | elpr 4564 |
. . . . 5
⊢ (𝑥 ∈ {∅, ∪ 𝐹}
↔ (𝑥 = ∅ ∨
𝑥 = ∪ 𝐹)) |
102 | 98, 99, 101 | 3imtr4g 299 |
. . . 4
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ (𝑥 ∈ ((𝐹 ∪ {∅}) ∩
(Clsd‘(𝐹 ∪
{∅}))) → 𝑥
∈ {∅, ∪ 𝐹})) |
103 | 102 | ssrdv 3907 |
. . 3
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ ((𝐹 ∪ {∅})
∩ (Clsd‘(𝐹 ∪
{∅}))) ⊆ {∅, ∪ 𝐹}) |
104 | 21 | isconn2 22311 |
. . 3
⊢ ((𝐹 ∪ {∅}) ∈ Conn
↔ ((𝐹 ∪ {∅})
∈ Top ∧ ((𝐹 ∪
{∅}) ∩ (Clsd‘(𝐹 ∪ {∅}))) ⊆ {∅, ∪ 𝐹})) |
105 | 72, 103, 104 | sylanbrc 586 |
. 2
⊢ (𝐹 ∈ (Fil‘∪ 𝐹)
→ (𝐹 ∪ {∅})
∈ Conn) |
106 | 4, 105 | syl 17 |
1
⊢ (𝐹 ∈ (Fil‘𝑋) → (𝐹 ∪ {∅}) ∈
Conn) |