This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem clsconn

Description: The closure of a connected set is connected. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion clsconn 
|- ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) -> ( J |`t ( ( cls ` J ) ` A ) ) e. Conn )

Proof

Step Hyp Ref Expression
1 simpll3 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) ) -> ( J |`t A ) e. Conn )
2 simpll1 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> J e. ( TopOn ` X ) )
3 simpll2 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> A C_ X )
4 simplrl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> x e. J )
5 simplrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> y e. J )
6 simprl1 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) )
7 n0 
 |-  ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) <-> E. z z e. ( x i^i ( ( cls ` J ) ` A ) ) )
8 6 7 sylib 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> E. z z e. ( x i^i ( ( cls ` J ) ` A ) ) )
9 2 adantr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( x i^i ( ( cls ` J ) ` A ) ) ) -> J e. ( TopOn ` X ) )
10 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
11 9 10 syl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( x i^i ( ( cls ` J ) ` A ) ) ) -> J e. Top )
12 3 adantr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( x i^i ( ( cls ` J ) ` A ) ) ) -> A C_ X )
13 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
14 9 13 syl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( x i^i ( ( cls ` J ) ` A ) ) ) -> X = U. J )
15 12 14 sseqtrd 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( x i^i ( ( cls ` J ) ` A ) ) ) -> A C_ U. J )
16 simpr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( x i^i ( ( cls ` J ) ` A ) ) ) -> z e. ( x i^i ( ( cls ` J ) ` A ) ) )
17 16 elin2d 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( x i^i ( ( cls ` J ) ` A ) ) ) -> z e. ( ( cls ` J ) ` A ) )
18 4 adantr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( x i^i ( ( cls ` J ) ` A ) ) ) -> x e. J )
19 16 elin1d 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( x i^i ( ( cls ` J ) ` A ) ) ) -> z e. x )
20 eqid 
 |-  U. J = U. J
21 20 clsndisj 
 |-  ( ( ( J e. Top /\ A C_ U. J /\ z e. ( ( cls ` J ) ` A ) ) /\ ( x e. J /\ z e. x ) ) -> ( x i^i A ) =/= (/) )
22 11 15 17 18 19 21 syl32anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( x i^i ( ( cls ` J ) ` A ) ) ) -> ( x i^i A ) =/= (/) )
23 8 22 exlimddv 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> ( x i^i A ) =/= (/) )
24 simprl2 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) )
25 n0 
 |-  ( ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) <-> E. z z e. ( y i^i ( ( cls ` J ) ` A ) ) )
26 24 25 sylib 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> E. z z e. ( y i^i ( ( cls ` J ) ` A ) ) )
27 2 adantr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( y i^i ( ( cls ` J ) ` A ) ) ) -> J e. ( TopOn ` X ) )
28 27 10 syl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( y i^i ( ( cls ` J ) ` A ) ) ) -> J e. Top )
29 3 adantr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( y i^i ( ( cls ` J ) ` A ) ) ) -> A C_ X )
30 27 13 syl 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( y i^i ( ( cls ` J ) ` A ) ) ) -> X = U. J )
31 29 30 sseqtrd 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( y i^i ( ( cls ` J ) ` A ) ) ) -> A C_ U. J )
32 simpr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( y i^i ( ( cls ` J ) ` A ) ) ) -> z e. ( y i^i ( ( cls ` J ) ` A ) ) )
33 32 elin2d 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( y i^i ( ( cls ` J ) ` A ) ) ) -> z e. ( ( cls ` J ) ` A ) )
34 5 adantr 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( y i^i ( ( cls ` J ) ` A ) ) ) -> y e. J )
35 32 elin1d 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( y i^i ( ( cls ` J ) ` A ) ) ) -> z e. y )
36 20 clsndisj 
 |-  ( ( ( J e. Top /\ A C_ U. J /\ z e. ( ( cls ` J ) ` A ) ) /\ ( y e. J /\ z e. y ) ) -> ( y i^i A ) =/= (/) )
37 28 31 33 34 35 36 syl32anc 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) /\ z e. ( y i^i ( ( cls ` J ) ` A ) ) ) -> ( y i^i A ) =/= (/) )
38 26 37 exlimddv 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> ( y i^i A ) =/= (/) )
39 simprl3 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) )
40 2 10 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> J e. Top )
41 2 13 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> X = U. J )
42 3 41 sseqtrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> A C_ U. J )
43 20 sscls 
 |-  ( ( J e. Top /\ A C_ U. J ) -> A C_ ( ( cls ` J ) ` A ) )
44 40 42 43 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> A C_ ( ( cls ` J ) ` A ) )
45 44 sscond 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> ( X \ ( ( cls ` J ) ` A ) ) C_ ( X \ A ) )
46 39 45 sstrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> ( x i^i y ) C_ ( X \ A ) )
47 ssv 
 |-  X C_ _V
48 ssdif 
 |-  ( X C_ _V -> ( X \ A ) C_ ( _V \ A ) )
49 47 48 ax-mp 
 |-  ( X \ A ) C_ ( _V \ A )
50 46 49 sstrdi 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> ( x i^i y ) C_ ( _V \ A ) )
51 disj2 
 |-  ( ( ( x i^i y ) i^i A ) = (/) <-> ( x i^i y ) C_ ( _V \ A ) )
52 50 51 sylibr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> ( ( x i^i y ) i^i A ) = (/) )
53 simprr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> ( ( cls ` J ) ` A ) C_ ( x u. y ) )
54 44 53 sstrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> A C_ ( x u. y ) )
55 2 3 4 5 23 38 52 54 nconnsubb 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) /\ ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) -> -. ( J |`t A ) e. Conn )
56 55 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) ) -> ( ( ( cls ` J ) ` A ) C_ ( x u. y ) -> -. ( J |`t A ) e. Conn ) )
57 1 56 mt2d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) /\ ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) ) -> -. ( ( cls ` J ) ` A ) C_ ( x u. y ) )
58 57 ex 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) /\ ( x e. J /\ y e. J ) ) -> ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) -> -. ( ( cls ` J ) ` A ) C_ ( x u. y ) ) )
59 58 ralrimivva 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) -> A. x e. J A. y e. J ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) -> -. ( ( cls ` J ) ` A ) C_ ( x u. y ) ) )
60 simp1 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) -> J e. ( TopOn ` X ) )
61 13 sseq2d 
 |-  ( J e. ( TopOn ` X ) -> ( A C_ X <-> A C_ U. J ) )
62 61 biimpa 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A C_ U. J )
63 20 clsss3 
 |-  ( ( J e. Top /\ A C_ U. J ) -> ( ( cls ` J ) ` A ) C_ U. J )
64 10 62 63 syl2an2r 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( ( cls ` J ) ` A ) C_ U. J )
65 13 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> X = U. J )
66 64 65 sseqtrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( ( cls ` J ) ` A ) C_ X )
67 66 3adant3 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) -> ( ( cls ` J ) ` A ) C_ X )
68 connsub 
 |-  ( ( J e. ( TopOn ` X ) /\ ( ( cls ` J ) ` A ) C_ X ) -> ( ( J |`t ( ( cls ` J ) ` A ) ) e. Conn <-> A. x e. J A. y e. J ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) -> -. ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) )
69 60 67 68 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) -> ( ( J |`t ( ( cls ` J ) ` A ) ) e. Conn <-> A. x e. J A. y e. J ( ( ( x i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( y i^i ( ( cls ` J ) ` A ) ) =/= (/) /\ ( x i^i y ) C_ ( X \ ( ( cls ` J ) ` A ) ) ) -> -. ( ( cls ` J ) ` A ) C_ ( x u. y ) ) ) )
70 59 69 mpbird 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X /\ ( J |`t A ) e. Conn ) -> ( J |`t ( ( cls ` J ) ` A ) ) e. Conn )