Step |
Hyp |
Ref |
Expression |
1 |
|
hauscmp.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
simp2 |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) → 𝑆 ⊆ 𝑋 ) |
3 |
|
eqid |
⊢ { 𝑦 ∈ 𝐽 ∣ ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) } = { 𝑦 ∈ 𝐽 ∣ ∃ 𝑤 ∈ 𝐽 ( 𝑥 ∈ 𝑤 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑤 ) ⊆ ( 𝑋 ∖ 𝑦 ) ) } |
4 |
|
simpl1 |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ) → 𝐽 ∈ Haus ) |
5 |
|
simpl2 |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ) → 𝑆 ⊆ 𝑋 ) |
6 |
|
simpl3 |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ) → ( 𝐽 ↾t 𝑆 ) ∈ Comp ) |
7 |
|
simpr |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ) → 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ) |
8 |
1 3 4 5 6 7
|
hauscmplem |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) ) |
9 |
|
haustop |
⊢ ( 𝐽 ∈ Haus → 𝐽 ∈ Top ) |
10 |
9
|
3ad2ant1 |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) → 𝐽 ∈ Top ) |
11 |
|
elssuni |
⊢ ( 𝑧 ∈ 𝐽 → 𝑧 ⊆ ∪ 𝐽 ) |
12 |
11 1
|
sseqtrrdi |
⊢ ( 𝑧 ∈ 𝐽 → 𝑧 ⊆ 𝑋 ) |
13 |
1
|
sscls |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑧 ⊆ 𝑋 ) → 𝑧 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) |
14 |
10 12 13
|
syl2an |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) ∧ 𝑧 ∈ 𝐽 ) → 𝑧 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ) |
15 |
|
sstr2 |
⊢ ( 𝑧 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) → 𝑧 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) |
16 |
14 15
|
syl |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) ∧ 𝑧 ∈ 𝐽 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) → 𝑧 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) |
17 |
16
|
anim2d |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) ∧ 𝑧 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) → ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) ) |
18 |
17
|
reximdva |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) → ( ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) ) |
19 |
18
|
adantr |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ) → ( ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑧 ) ⊆ ( 𝑋 ∖ 𝑆 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) ) |
20 |
8 19
|
mpd |
⊢ ( ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) ∧ 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ) → ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) |
21 |
20
|
ralrimiva |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) → ∀ 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) |
22 |
|
eltop2 |
⊢ ( 𝐽 ∈ Top → ( ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) ) |
23 |
10 22
|
syl |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) → ( ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( 𝑋 ∖ 𝑆 ) ∃ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ∧ 𝑧 ⊆ ( 𝑋 ∖ 𝑆 ) ) ) ) |
24 |
21 23
|
mpbird |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) → ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) |
25 |
1
|
iscld |
⊢ ( 𝐽 ∈ Top → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) ) |
26 |
10 25
|
syl |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑆 ⊆ 𝑋 ∧ ( 𝑋 ∖ 𝑆 ) ∈ 𝐽 ) ) ) |
27 |
2 24 26
|
mpbir2and |
⊢ ( ( 𝐽 ∈ Haus ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Comp ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) |