Metamath Proof Explorer

Theorem connsub

Description: Two equivalent ways of saying that a subspace topology is connected. (Contributed by Jeff Hankins, 9-Jul-2009) (Proof shortened by Mario Carneiro, 10-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 connsuba 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X ) -> ( ( J |`t S ) e. Conn <-> A. x e. J A. y e. J ( ( ( x i^i S ) =/= (/) /\ ( y i^i S ) =/= (/) /\ ( ( x i^i y ) i^i S ) = (/) ) -> ( ( x u. y ) i^i S ) =/= S ) ) )
2 inss1 
 |-  ( x i^i y ) C_ x
3 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X )
4 3 ad2ant2r 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X ) /\ ( x e. J /\ y e. J ) ) -> x C_ X )
5 2 4 sstrid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X ) /\ ( x e. J /\ y e. J ) ) -> ( x i^i y ) C_ X )
6 reldisj 
 |-  ( ( x i^i y ) C_ X -> ( ( ( x i^i y ) i^i S ) = (/) <-> ( x i^i y ) C_ ( X \ S ) ) )
7 5 6 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X ) /\ ( x e. J /\ y e. J ) ) -> ( ( ( x i^i y ) i^i S ) = (/) <-> ( x i^i y ) C_ ( X \ S ) ) )
8 7 3anbi3d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X ) /\ ( x e. J /\ y e. J ) ) -> ( ( ( x i^i S ) =/= (/) /\ ( y i^i S ) =/= (/) /\ ( ( x i^i y ) i^i S ) = (/) ) <-> ( ( x i^i S ) =/= (/) /\ ( y i^i S ) =/= (/) /\ ( x i^i y ) C_ ( X \ S ) ) ) )
9 sseqin2 
 |-  ( S C_ ( x u. y ) <-> ( ( x u. y ) i^i S ) = S )
10 9 a1i 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X ) /\ ( x e. J /\ y e. J ) ) -> ( S C_ ( x u. y ) <-> ( ( x u. y ) i^i S ) = S ) )
11 10 bicomd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X ) /\ ( x e. J /\ y e. J ) ) -> ( ( ( x u. y ) i^i S ) = S <-> S C_ ( x u. y ) ) )
12 11 necon3abid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X ) /\ ( x e. J /\ y e. J ) ) -> ( ( ( x u. y ) i^i S ) =/= S <-> -. S C_ ( x u. y ) ) )
13 8 12 imbi12d 
 |-  ( ( ( J e. ( TopOn ` X ) /\ S C_ X ) /\ ( x e. J /\ y e. J ) ) -> ( ( ( ( x i^i S ) =/= (/) /\ ( y i^i S ) =/= (/) /\ ( ( x i^i y ) i^i S ) = (/) ) -> ( ( x u. y ) i^i S ) =/= S ) <-> ( ( ( x i^i S ) =/= (/) /\ ( y i^i S ) =/= (/) /\ ( x i^i y ) C_ ( X \ S ) ) -> -. S C_ ( x u. y ) ) ) )
14 13 2ralbidva 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X ) -> ( A. x e. J A. y e. J ( ( ( x i^i S ) =/= (/) /\ ( y i^i S ) =/= (/) /\ ( ( x i^i y ) i^i S ) = (/) ) -> ( ( x u. y ) i^i S ) =/= S ) <-> A. x e. J A. y e. J ( ( ( x i^i S ) =/= (/) /\ ( y i^i S ) =/= (/) /\ ( x i^i y ) C_ ( X \ S ) ) -> -. S C_ ( x u. y ) ) ) )
15 1 14 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ S C_ X ) -> ( ( J |`t S ) e. Conn <-> A. x e. J A. y e. J ( ( ( x i^i S ) =/= (/) /\ ( y i^i S ) =/= (/) /\ ( x i^i y ) C_ ( X \ S ) ) -> -. S C_ ( x u. y ) ) ) )