Metamath Proof Explorer

Theorem conndisj

Description: If a topology is connected, its underlying set can't be partitioned into two nonempty non-overlapping open sets. (Contributed by FL, 16-Nov-2008) (Proof shortened by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypotheses isconn.1 
|- X = U. J
connclo.1 
|- ( ph -> J e. Conn )
connclo.2 
|- ( ph -> A e. J )
connclo.3 
|- ( ph -> A =/= (/) )
conndisj.4 
|- ( ph -> B e. J )
conndisj.5 
|- ( ph -> B =/= (/) )
conndisj.6 
|- ( ph -> ( A i^i B ) = (/) )
Assertion conndisj 
|- ( ph -> ( A u. B ) =/= X )

Proof

Step Hyp Ref Expression
1 isconn.1 
 |-  X = U. J
2 connclo.1 
 |-  ( ph -> J e. Conn )
3 connclo.2 
 |-  ( ph -> A e. J )
4 connclo.3 
 |-  ( ph -> A =/= (/) )
5 conndisj.4 
 |-  ( ph -> B e. J )
6 conndisj.5 
 |-  ( ph -> B =/= (/) )
7 conndisj.6 
 |-  ( ph -> ( A i^i B ) = (/) )
8 elssuni 
 |-  ( A e. J -> A C_ U. J )
9 3 8 syl 
 |-  ( ph -> A C_ U. J )
10 9 1 sseqtrrdi 
 |-  ( ph -> A C_ X )
11 uneqdifeq 
 |-  ( ( A C_ X /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = X <-> ( X \ A ) = B ) )
12 10 7 11 syl2anc 
 |-  ( ph -> ( ( A u. B ) = X <-> ( X \ A ) = B ) )
13 simpr 
 |-  ( ( ph /\ ( X \ A ) = B ) -> ( X \ A ) = B )
14 13 difeq2d 
 |-  ( ( ph /\ ( X \ A ) = B ) -> ( X \ ( X \ A ) ) = ( X \ B ) )
15 dfss4 
 |-  ( A C_ X <-> ( X \ ( X \ A ) ) = A )
16 10 15 sylib 
 |-  ( ph -> ( X \ ( X \ A ) ) = A )
17 16 adantr 
 |-  ( ( ph /\ ( X \ A ) = B ) -> ( X \ ( X \ A ) ) = A )
18 2 adantr 
 |-  ( ( ph /\ ( X \ A ) = B ) -> J e. Conn )
19 5 adantr 
 |-  ( ( ph /\ ( X \ A ) = B ) -> B e. J )
20 6 adantr 
 |-  ( ( ph /\ ( X \ A ) = B ) -> B =/= (/) )
21 1 isconn 
 |-  ( J e. Conn <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) = { (/) , X } ) )
22 21 simplbi 
 |-  ( J e. Conn -> J e. Top )
23 2 22 syl 
 |-  ( ph -> J e. Top )
24 1 opncld 
 |-  ( ( J e. Top /\ A e. J ) -> ( X \ A ) e. ( Clsd ` J ) )
25 23 3 24 syl2anc 
 |-  ( ph -> ( X \ A ) e. ( Clsd ` J ) )
26 25 adantr 
 |-  ( ( ph /\ ( X \ A ) = B ) -> ( X \ A ) e. ( Clsd ` J ) )
27 13 26 eqeltrrd 
 |-  ( ( ph /\ ( X \ A ) = B ) -> B e. ( Clsd ` J ) )
28 1 18 19 20 27 connclo 
 |-  ( ( ph /\ ( X \ A ) = B ) -> B = X )
29 28 difeq2d 
 |-  ( ( ph /\ ( X \ A ) = B ) -> ( X \ B ) = ( X \ X ) )
30 difid 
 |-  ( X \ X ) = (/)
31 29 30 eqtrdi 
 |-  ( ( ph /\ ( X \ A ) = B ) -> ( X \ B ) = (/) )
32 14 17 31 3eqtr3d 
 |-  ( ( ph /\ ( X \ A ) = B ) -> A = (/) )
33 32 ex 
 |-  ( ph -> ( ( X \ A ) = B -> A = (/) ) )
34 12 33 sylbid 
 |-  ( ph -> ( ( A u. B ) = X -> A = (/) ) )
35 34 necon3d 
 |-  ( ph -> ( A =/= (/) -> ( A u. B ) =/= X ) )
36 4 35 mpd 
 |-  ( ph -> ( A u. B ) =/= X )