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 ⊢ 𝑋 = ∪ 𝐽
connclo.1 ⊢ ( 𝜑 → 𝐽 ∈ Conn )
connclo.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
connclo.3 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
conndisj.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
conndisj.5 ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
conndisj.6 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
Assertion conndisj ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ≠ 𝑋 )

Proof

Step Hyp Ref Expression
1 isconn.1 ⊢ 𝑋 = ∪ 𝐽
2 connclo.1 ⊢ ( 𝜑 → 𝐽 ∈ Conn )
3 connclo.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
4 connclo.3 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
5 conndisj.4 ⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
6 conndisj.5 ⊢ ( 𝜑 → 𝐵 ≠ ∅ )
7 conndisj.6 ⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
8 elssuni ⊢ ( 𝐴 ∈ 𝐽 → 𝐴 ⊆ ∪ 𝐽 )
9 3 8 syl ⊢ ( 𝜑 → 𝐴 ⊆ ∪ 𝐽 )
10 9 1 sseqtrrdi ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
11 uneqdifeq ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) = 𝑋 ↔ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) )
12 10 7 11 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) = 𝑋 ↔ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) )
13 simpr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → ( 𝑋 ∖ 𝐴 ) = 𝐵 )
14 13 difeq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = ( 𝑋 ∖ 𝐵 ) )
15 dfss4 ⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 )
16 10 15 sylib ⊢ ( 𝜑 → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → ( 𝑋 ∖ ( 𝑋 ∖ 𝐴 ) ) = 𝐴 )
18 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → 𝐽 ∈ Conn )
19 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → 𝐵 ∈ 𝐽 )
20 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → 𝐵 ≠ ∅ )
21 1 isconn ⊢ ( 𝐽 ∈ Conn ↔ ( 𝐽 ∈ Top ∧ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) = { ∅ , 𝑋 } ) )
22 21 simplbi ⊢ ( 𝐽 ∈ Conn → 𝐽 ∈ Top )
23 2 22 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
24 1 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ) → ( 𝑋 ∖ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) )
25 23 3 24 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∖ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) )
26 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → ( 𝑋 ∖ 𝐴 ) ∈ ( Clsd ‘ 𝐽 ) )
27 13 26 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
28 1 18 19 20 27 connclo ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → 𝐵 = 𝑋 )
29 28 difeq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → ( 𝑋 ∖ 𝐵 ) = ( 𝑋 ∖ 𝑋 ) )
30 difid ⊢ ( 𝑋 ∖ 𝑋 ) = ∅
31 29 30 eqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → ( 𝑋 ∖ 𝐵 ) = ∅ )
32 14 17 31 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑋 ∖ 𝐴 ) = 𝐵 ) → 𝐴 = ∅ )
33 32 ex ⊢ ( 𝜑 → ( ( 𝑋 ∖ 𝐴 ) = 𝐵 → 𝐴 = ∅ ) )
34 12 33 sylbid ⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) = 𝑋 → 𝐴 = ∅ ) )
35 34 necon3d ⊢ ( 𝜑 → ( 𝐴 ≠ ∅ → ( 𝐴 ∪ 𝐵 ) ≠ 𝑋 ) )
36 4 35 mpd ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ≠ 𝑋 )