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

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 = ⋃ J
connclo.1 ⊢ φ → J ∈ Conn
connclo.2 ⊢ φ → A ∈ J
connclo.3 ⊢ φ → A ≠ ∅
conndisj.4 ⊢ φ → B ∈ J
conndisj.5 ⊢ φ → B ≠ ∅
conndisj.6 ⊢ φ → A ∩ B = ∅
Assertion conndisj ⊢ φ → A ∪ B ≠ X

Proof

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