Metamath Proof Explorer

Theorem connsuba

Description: Connectedness for a subspace. See connsub . (Contributed by FL, 29-May-2014) (Proof shortened by Mario Carneiro, 10-Mar-2015)

Ref Expression
Assertion connsuba 
|- ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( ( J |`t A ) e. Conn <-> A. x e. J A. y e. J ( ( ( x i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( x i^i y ) i^i A ) = (/) ) -> ( ( x u. y ) i^i A ) =/= A ) ) )

Proof

Step Hyp Ref Expression
1 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( J |`t A ) e. ( TopOn ` A ) )
2 dfconn2 
 |-  ( ( J |`t A ) e. ( TopOn ` A ) -> ( ( J |`t A ) e. Conn <-> A. u e. ( J |`t A ) A. v e. ( J |`t A ) ( ( u =/= (/) /\ v =/= (/) /\ ( u i^i v ) = (/) ) -> ( u u. v ) =/= A ) ) )
3 1 2 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( ( J |`t A ) e. Conn <-> A. u e. ( J |`t A ) A. v e. ( J |`t A ) ( ( u =/= (/) /\ v =/= (/) /\ ( u i^i v ) = (/) ) -> ( u u. v ) =/= A ) ) )
4 vex 
 |-  x e. _V
5 4 inex1 
 |-  ( x i^i A ) e. _V
6 5 a1i 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ x e. J ) -> ( x i^i A ) e. _V )
7 toponmax 
 |-  ( J e. ( TopOn ` X ) -> X e. J )
8 7 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> X e. J )
9 simpr 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A C_ X )
10 8 9 ssexd 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> A e. _V )
11 elrest 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. _V ) -> ( u e. ( J |`t A ) <-> E. x e. J u = ( x i^i A ) ) )
12 10 11 syldan 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( u e. ( J |`t A ) <-> E. x e. J u = ( x i^i A ) ) )
13 vex 
 |-  y e. _V
14 13 inex1 
 |-  ( y i^i A ) e. _V
15 14 a1i 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ y e. J ) -> ( y i^i A ) e. _V )
16 elrest 
 |-  ( ( J e. ( TopOn ` X ) /\ A e. _V ) -> ( v e. ( J |`t A ) <-> E. y e. J v = ( y i^i A ) ) )
17 10 16 syldan 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( v e. ( J |`t A ) <-> E. y e. J v = ( y i^i A ) ) )
18 17 adantr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) -> ( v e. ( J |`t A ) <-> E. y e. J v = ( y i^i A ) ) )
19 simplr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> u = ( x i^i A ) )
20 19 neeq1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> ( u =/= (/) <-> ( x i^i A ) =/= (/) ) )
21 simpr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> v = ( y i^i A ) )
22 21 neeq1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> ( v =/= (/) <-> ( y i^i A ) =/= (/) ) )
23 19 21 ineq12d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> ( u i^i v ) = ( ( x i^i A ) i^i ( y i^i A ) ) )
24 inindir 
 |-  ( ( x i^i y ) i^i A ) = ( ( x i^i A ) i^i ( y i^i A ) )
25 23 24 eqtr4di 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> ( u i^i v ) = ( ( x i^i y ) i^i A ) )
26 25 eqeq1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> ( ( u i^i v ) = (/) <-> ( ( x i^i y ) i^i A ) = (/) ) )
27 20 22 26 3anbi123d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> ( ( u =/= (/) /\ v =/= (/) /\ ( u i^i v ) = (/) ) <-> ( ( x i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( x i^i y ) i^i A ) = (/) ) ) )
28 19 21 uneq12d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> ( u u. v ) = ( ( x i^i A ) u. ( y i^i A ) ) )
29 indir 
 |-  ( ( x u. y ) i^i A ) = ( ( x i^i A ) u. ( y i^i A ) )
30 28 29 eqtr4di 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> ( u u. v ) = ( ( x u. y ) i^i A ) )
31 30 neeq1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> ( ( u u. v ) =/= A <-> ( ( x u. y ) i^i A ) =/= A ) )
32 27 31 imbi12d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) /\ v = ( y i^i A ) ) -> ( ( ( u =/= (/) /\ v =/= (/) /\ ( u i^i v ) = (/) ) -> ( u u. v ) =/= A ) <-> ( ( ( x i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( x i^i y ) i^i A ) = (/) ) -> ( ( x u. y ) i^i A ) =/= A ) ) )
33 15 18 32 ralxfr2d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ A C_ X ) /\ u = ( x i^i A ) ) -> ( A. v e. ( J |`t A ) ( ( u =/= (/) /\ v =/= (/) /\ ( u i^i v ) = (/) ) -> ( u u. v ) =/= A ) <-> A. y e. J ( ( ( x i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( x i^i y ) i^i A ) = (/) ) -> ( ( x u. y ) i^i A ) =/= A ) ) )
34 6 12 33 ralxfr2d 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( A. u e. ( J |`t A ) A. v e. ( J |`t A ) ( ( u =/= (/) /\ v =/= (/) /\ ( u i^i v ) = (/) ) -> ( u u. v ) =/= A ) <-> A. x e. J A. y e. J ( ( ( x i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( x i^i y ) i^i A ) = (/) ) -> ( ( x u. y ) i^i A ) =/= A ) ) )
35 3 34 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ A C_ X ) -> ( ( J |`t A ) e. Conn <-> A. x e. J A. y e. J ( ( ( x i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( x i^i y ) i^i A ) = (/) ) -> ( ( x u. y ) i^i A ) =/= A ) ) )