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 = U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) }
Assertion conncompcld 
|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 conncomp.2 
 |-  S = U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) }
2 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
3 ssrab2 
 |-  { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } C_ ~P X
4 sspwuni 
 |-  ( { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } C_ ~P X <-> U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } C_ X )
5 3 4 mpbi 
 |-  U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } C_ X
6 1 5 eqsstri 
 |-  S C_ X
7 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
8 7 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> X = U. J )
9 6 8 sseqtrid 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S C_ U. J )
10 eqid 
 |-  U. J = U. J
11 10 clsss3 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( ( cls ` J ) ` S ) C_ U. J )
12 2 9 11 syl2an2r 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( ( cls ` J ) ` S ) C_ U. J )
13 12 8 sseqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( ( cls ` J ) ` S ) C_ X )
14 10 sscls 
 |-  ( ( J e. Top /\ S C_ U. J ) -> S C_ ( ( cls ` J ) ` S ) )
15 2 9 14 syl2an2r 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S C_ ( ( cls ` J ) ` S ) )
16 1 conncompid 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. S )
17 15 16 sseldd 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. ( ( cls ` J ) ` S ) )
18 simpl 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> J e. ( TopOn ` X ) )
19 6 a1i 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S C_ X )
20 1 conncompconn 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t S ) e. Conn )
21 clsconn 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X /\ ( J |`t S ) e. Conn ) -> ( J |`t ( ( cls ` J ) ` S ) ) e. Conn )
22 18 19 20 21 syl3anc 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t ( ( cls ` J ) ` S ) ) e. Conn )
23 1 conncompss 
 |-  ( ( ( ( cls ` J ) ` S ) C_ X /\ A e. ( ( cls ` J ) ` S ) /\ ( J |`t ( ( cls ` J ) ` S ) ) e. Conn ) -> ( ( cls ` J ) ` S ) C_ S )
24 13 17 22 23 syl3anc 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( ( cls ` J ) ` S ) C_ S )
25 10 iscld4 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( S e. ( Clsd ` J ) <-> ( ( cls ` J ) ` S ) C_ S ) )
26 2 9 25 syl2an2r 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( S e. ( Clsd ` J ) <-> ( ( cls ` J ) ` S ) C_ S ) )
27 24 26 mpbird 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S e. ( Clsd ` J ) )