Metamath Proof Explorer


Theorem conncompcld

Description: The connected component containing A is a closed set. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Hypothesis conncomp.2 𝑆 = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴𝑥 ∧ ( 𝐽t 𝑥 ) ∈ Conn ) }
Assertion conncompcld ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴𝑋 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )

Proof

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 ‘ 𝐽 ) )