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 ⊢ S = ⋃ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn
Assertion conncompcld ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → S ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 conncomp.2 ⊢ S = ⋃ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn
2 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
3 ssrab2 ⊢ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn ⊆ 𝒫 X
4 sspwuni ⊢ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn ⊆ 𝒫 X ↔ ⋃ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn ⊆ X
5 3 4 mpbi ⊢ ⋃ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn ⊆ X
6 1 5 eqsstri ⊢ S ⊆ X
7 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
8 7 adantr ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → X = ⋃ J
9 6 8 sseqtrid ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → S ⊆ ⋃ J
10 eqid ⊢ ⋃ J = ⋃ J
11 10 clsss3 ⊢ J ∈ Top ∧ S ⊆ ⋃ J → cls ⁡ J ⁡ S ⊆ ⋃ J
12 2 9 11 syl2an2r ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → cls ⁡ J ⁡ S ⊆ ⋃ J
13 12 8 sseqtrrd ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → cls ⁡ J ⁡ S ⊆ X
14 10 sscls ⊢ J ∈ Top ∧ S ⊆ ⋃ J → S ⊆ cls ⁡ J ⁡ S
15 2 9 14 syl2an2r ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → S ⊆ cls ⁡ J ⁡ S
16 1 conncompid ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → A ∈ S
17 15 16 sseldd ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → A ∈ cls ⁡ J ⁡ S
18 simpl ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → J ∈ TopOn ⁡ X
19 6 a1i ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → S ⊆ X
20 1 conncompconn ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → J ↾ 𝑡 S ∈ Conn
21 clsconn ⊢ J ∈ TopOn ⁡ X ∧ S ⊆ X ∧ J ↾ 𝑡 S ∈ Conn → J ↾ 𝑡 cls ⁡ J ⁡ S ∈ Conn
22 18 19 20 21 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → J ↾ 𝑡 cls ⁡ J ⁡ S ∈ Conn
23 1 conncompss ⊢ cls ⁡ J ⁡ S ⊆ X ∧ A ∈ cls ⁡ J ⁡ S ∧ J ↾ 𝑡 cls ⁡ J ⁡ S ∈ Conn → cls ⁡ J ⁡ S ⊆ S
24 13 17 22 23 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → cls ⁡ J ⁡ S ⊆ S
25 10 iscld4 ⊢ J ∈ Top ∧ S ⊆ ⋃ J → S ∈ Clsd ⁡ J ↔ cls ⁡ J ⁡ S ⊆ S
26 2 9 25 syl2an2r ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → S ∈ Clsd ⁡ J ↔ cls ⁡ J ⁡ S ⊆ S
27 24 26 mpbird ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → S ∈ Clsd ⁡ J