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 )