Metamath Proof Explorer

Theorem conncompid

Description: The connected component containing A contains A . (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 conncompid 
|- ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. S )

Proof

Step Hyp Ref Expression
1 conncomp.2 
 |-  S = U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) }
2 simpr 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. X )
3 2 snssd 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> { A } C_ X )
4 snex 
 |-  { A } e. _V
5 4 elpw 
 |-  ( { A } e. ~P X <-> { A } C_ X )
6 3 5 sylibr 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> { A } e. ~P X )
7 snidg 
 |-  ( A e. X -> A e. { A } )
8 7 adantl 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. { A } )
9 restsn2 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t { A } ) = ~P { A } )
10 pwsn 
 |-  ~P { A } = { (/) , { A } }
11 indisconn 
 |-  { (/) , { A } } e. Conn
12 10 11 eqeltri 
 |-  ~P { A } e. Conn
13 9 12 eqeltrdi 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( J |`t { A } ) e. Conn )
14 8 13 jca 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> ( A e. { A } /\ ( J |`t { A } ) e. Conn ) )
15 eleq2 
 |-  ( x = { A } -> ( A e. x <-> A e. { A } ) )
16 oveq2 
 |-  ( x = { A } -> ( J |`t x ) = ( J |`t { A } ) )
17 16 eleq1d 
 |-  ( x = { A } -> ( ( J |`t x ) e. Conn <-> ( J |`t { A } ) e. Conn ) )
18 15 17 anbi12d 
 |-  ( x = { A } -> ( ( A e. x /\ ( J |`t x ) e. Conn ) <-> ( A e. { A } /\ ( J |`t { A } ) e. Conn ) ) )
19 15 18 anbi12d 
 |-  ( x = { A } -> ( ( A e. x /\ ( A e. x /\ ( J |`t x ) e. Conn ) ) <-> ( A e. { A } /\ ( A e. { A } /\ ( J |`t { A } ) e. Conn ) ) ) )
20 19 rspcev 
 |-  ( ( { A } e. ~P X /\ ( A e. { A } /\ ( A e. { A } /\ ( J |`t { A } ) e. Conn ) ) ) -> E. x e. ~P X ( A e. x /\ ( A e. x /\ ( J |`t x ) e. Conn ) ) )
21 6 8 14 20 syl12anc 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> E. x e. ~P X ( A e. x /\ ( A e. x /\ ( J |`t x ) e. Conn ) ) )
22 elunirab 
 |-  ( A e. U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } <-> E. x e. ~P X ( A e. x /\ ( A e. x /\ ( J |`t x ) e. Conn ) ) )
23 21 22 sylibr 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. U. { x e. ~P X | ( A e. x /\ ( J |`t x ) e. Conn ) } )
24 23 1 eleqtrrdi 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. X ) -> A e. S )