Metamath Proof Explorer

Theorem conncompclo

Description: The connected component containing A is a subset of any clopen set containing A . (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypothesis conncomp.2 
|- S = U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) }
Assertion conncompclo 
|- ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> S C_ T )

Proof

Step Hyp Ref Expression
1 conncomp.2 
 |-  S = U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) }
2 eqid 
 |-  U. J = U. J
3 simp1 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> J e. ( TopOn ` X ) )
4 simp2 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> T e. ( J i^i ( Clsd ` J ) ) )
5 4 elin1d 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> T e. J )
6 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. J ) -> T C_ X )
7 3 5 6 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> T C_ X )
8 simp3 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> A e. T )
9 7 8 sseldd 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> A e. X )
10 1 conncompcld 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> S e. ( Clsd ` J ) )
11 3 9 10 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> S e. ( Clsd ` J ) )
12 2 cldss 
 |-  ( S e. ( Clsd ` J ) -> S C_ U. J )
13 11 12 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> S C_ U. J )
14 1 conncompconn 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t S ) e. Conn )
15 3 9 14 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> ( J |`t S ) e. Conn )
16 1 conncompid 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. S )
17 3 9 16 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> A e. S )
18 inelcm 
 |-  ( ( A e. T /\ A e. S ) -> ( T i^i S ) =/= (/) )
19 8 17 18 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> ( T i^i S ) =/= (/) )
20 4 elin2d 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> T e. ( Clsd ` J ) )
21 2 13 15 5 19 20 connsubclo 
 |-  ( ( J e. ( TopOn ` X ) /\ T e. ( J i^i ( Clsd ` J ) ) /\ A e. T ) -> S C_ T )