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

Metamath Proof Explorer

Theorem nconnsubb

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

Ref Expression
Hypotheses nconnsubb.2 
|- ( ph -> J e. ( TopOn ` X ) )
nconnsubb.3 
|- ( ph -> A C_ X )
nconnsubb.4 
|- ( ph -> U e. J )
nconnsubb.5 
|- ( ph -> V e. J )
nconnsubb.6 
|- ( ph -> ( U i^i A ) =/= (/) )
nconnsubb.7 
|- ( ph -> ( V i^i A ) =/= (/) )
nconnsubb.8 
|- ( ph -> ( ( U i^i V ) i^i A ) = (/) )
nconnsubb.9 
|- ( ph -> A C_ ( U u. V ) )
Assertion nconnsubb 
|- ( ph -> -. ( J |`t A ) e. Conn )

Proof

Step Hyp Ref Expression
1 nconnsubb.2 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 nconnsubb.3 
 |-  ( ph -> A C_ X )
3 nconnsubb.4 
 |-  ( ph -> U e. J )
4 nconnsubb.5 
 |-  ( ph -> V e. J )
5 nconnsubb.6 
 |-  ( ph -> ( U i^i A ) =/= (/) )
6 nconnsubb.7 
 |-  ( ph -> ( V i^i A ) =/= (/) )
7 nconnsubb.8 
 |-  ( ph -> ( ( U i^i V ) i^i A ) = (/) )
8 nconnsubb.9 
 |-  ( ph -> A C_ ( U u. V ) )
9 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 ) ) )
10 1 2 9 syl2anc 
 |-  ( ph -> ( ( 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 ) ) )
11 5 6 7 3jca 
 |-  ( ph -> ( ( U i^i A ) =/= (/) /\ ( V i^i A ) =/= (/) /\ ( ( U i^i V ) i^i A ) = (/) ) )
12 ineq1 
 |-  ( x = U -> ( x i^i A ) = ( U i^i A ) )
13 12 neeq1d 
 |-  ( x = U -> ( ( x i^i A ) =/= (/) <-> ( U i^i A ) =/= (/) ) )
14 ineq1 
 |-  ( x = U -> ( x i^i y ) = ( U i^i y ) )
15 14 ineq1d 
 |-  ( x = U -> ( ( x i^i y ) i^i A ) = ( ( U i^i y ) i^i A ) )
16 15 eqeq1d 
 |-  ( x = U -> ( ( ( x i^i y ) i^i A ) = (/) <-> ( ( U i^i y ) i^i A ) = (/) ) )
17 13 16 3anbi13d 
 |-  ( x = U -> ( ( ( x i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( x i^i y ) i^i A ) = (/) ) <-> ( ( U i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( U i^i y ) i^i A ) = (/) ) ) )
18 uneq1 
 |-  ( x = U -> ( x u. y ) = ( U u. y ) )
19 18 ineq1d 
 |-  ( x = U -> ( ( x u. y ) i^i A ) = ( ( U u. y ) i^i A ) )
20 19 neeq1d 
 |-  ( x = U -> ( ( ( x u. y ) i^i A ) =/= A <-> ( ( U u. y ) i^i A ) =/= A ) )
21 17 20 imbi12d 
 |-  ( x = U -> ( ( ( ( x i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( x i^i y ) i^i A ) = (/) ) -> ( ( x u. y ) i^i A ) =/= A ) <-> ( ( ( U i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( U i^i y ) i^i A ) = (/) ) -> ( ( U u. y ) i^i A ) =/= A ) ) )
22 ineq1 
 |-  ( y = V -> ( y i^i A ) = ( V i^i A ) )
23 22 neeq1d 
 |-  ( y = V -> ( ( y i^i A ) =/= (/) <-> ( V i^i A ) =/= (/) ) )
24 ineq2 
 |-  ( y = V -> ( U i^i y ) = ( U i^i V ) )
25 24 ineq1d 
 |-  ( y = V -> ( ( U i^i y ) i^i A ) = ( ( U i^i V ) i^i A ) )
26 25 eqeq1d 
 |-  ( y = V -> ( ( ( U i^i y ) i^i A ) = (/) <-> ( ( U i^i V ) i^i A ) = (/) ) )
27 23 26 3anbi23d 
 |-  ( y = V -> ( ( ( U i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( U i^i y ) i^i A ) = (/) ) <-> ( ( U i^i A ) =/= (/) /\ ( V i^i A ) =/= (/) /\ ( ( U i^i V ) i^i A ) = (/) ) ) )
28 sseqin2 
 |-  ( A C_ ( U u. y ) <-> ( ( U u. y ) i^i A ) = A )
29 28 necon3bbii 
 |-  ( -. A C_ ( U u. y ) <-> ( ( U u. y ) i^i A ) =/= A )
30 uneq2 
 |-  ( y = V -> ( U u. y ) = ( U u. V ) )
31 30 sseq2d 
 |-  ( y = V -> ( A C_ ( U u. y ) <-> A C_ ( U u. V ) ) )
32 31 notbid 
 |-  ( y = V -> ( -. A C_ ( U u. y ) <-> -. A C_ ( U u. V ) ) )
33 29 32 bitr3id 
 |-  ( y = V -> ( ( ( U u. y ) i^i A ) =/= A <-> -. A C_ ( U u. V ) ) )
34 27 33 imbi12d 
 |-  ( y = V -> ( ( ( ( U i^i A ) =/= (/) /\ ( y i^i A ) =/= (/) /\ ( ( U i^i y ) i^i A ) = (/) ) -> ( ( U u. y ) i^i A ) =/= A ) <-> ( ( ( U i^i A ) =/= (/) /\ ( V i^i A ) =/= (/) /\ ( ( U i^i V ) i^i A ) = (/) ) -> -. A C_ ( U u. V ) ) ) )
35 21 34 rspc2v 
 |-  ( ( U e. J /\ V e. J ) -> ( 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 ) -> ( ( ( U i^i A ) =/= (/) /\ ( V i^i A ) =/= (/) /\ ( ( U i^i V ) i^i A ) = (/) ) -> -. A C_ ( U u. V ) ) ) )
36 3 4 35 syl2anc 
 |-  ( ph -> ( 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 ) -> ( ( ( U i^i A ) =/= (/) /\ ( V i^i A ) =/= (/) /\ ( ( U i^i V ) i^i A ) = (/) ) -> -. A C_ ( U u. V ) ) ) )
37 11 36 mpid 
 |-  ( ph -> ( 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 ) -> -. A C_ ( U u. V ) ) )
38 10 37 sylbid 
 |-  ( ph -> ( ( J |`t A ) e. Conn -> -. A C_ ( U u. V ) ) )
39 8 38 mt2d 
 |-  ( ph -> -. ( J |`t A ) e. Conn )