Step |
Hyp |
Ref |
Expression |
1 |
|
conncomp.2 |
⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } |
2 |
|
topontop |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top ) |
3 |
|
ssrab2 |
⊢ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝒫 𝑋 |
4 |
|
sspwuni |
⊢ ( { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝒫 𝑋 ↔ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝑋 ) |
5 |
3 4
|
mpbi |
⊢ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ⊆ 𝑋 |
6 |
1 5
|
eqsstri |
⊢ 𝑆 ⊆ 𝑋 |
7 |
|
toponuni |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
8 |
7
|
adantr |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
9 |
6 8
|
sseqtrid |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ⊆ ∪ 𝐽 ) |
10 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
11 |
10
|
clsss3 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 ) |
12 |
2 9 11
|
syl2an2r |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 ) |
13 |
12 8
|
sseqtrrd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 ) |
14 |
10
|
sscls |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) |
15 |
2 9 14
|
syl2an2r |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) |
16 |
1
|
conncompid |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑆 ) |
17 |
15 16
|
sseldd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) |
18 |
|
simpl |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
19 |
6
|
a1i |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ⊆ 𝑋 ) |
20 |
1
|
conncompconn |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t 𝑆 ) ∈ Conn ) |
21 |
|
clsconn |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝐽 ↾t 𝑆 ) ∈ Conn ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ Conn ) |
22 |
18 19 20 21
|
syl3anc |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ Conn ) |
23 |
1
|
conncompss |
⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ Conn ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) |
24 |
13 17 22 23
|
syl3anc |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) |
25 |
10
|
iscld4 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) ) |
26 |
2 9 25
|
syl2an2r |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) ) |
27 |
24 26
|
mpbird |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) |