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

Metamath Proof Explorer

Theorem connsubclo

Description: If a clopen set meets a connected subspace, it must contain the entire subspace. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypotheses connsubclo.1 ⊢ X = ⋃ J
connsubclo.3 ⊢ φ → A ⊆ X
connsubclo.4 ⊢ φ → J ↾ 𝑡 A ∈ Conn
connsubclo.5 ⊢ φ → B ∈ J
connsubclo.6 ⊢ φ → B ∩ A ≠ ∅
connsubclo.7 ⊢ φ → B ∈ Clsd ⁡ J
Assertion connsubclo ⊢ φ → A ⊆ B

Proof

Step Hyp Ref Expression
1 connsubclo.1 ⊢ X = ⋃ J
2 connsubclo.3 ⊢ φ → A ⊆ X
3 connsubclo.4 ⊢ φ → J ↾ 𝑡 A ∈ Conn
4 connsubclo.5 ⊢ φ → B ∈ J
5 connsubclo.6 ⊢ φ → B ∩ A ≠ ∅
6 connsubclo.7 ⊢ φ → B ∈ Clsd ⁡ J
7 eqid ⊢ ⋃ J ↾ 𝑡 A = ⋃ J ↾ 𝑡 A
8 cldrcl ⊢ B ∈ Clsd ⁡ J → J ∈ Top
9 6 8 syl ⊢ φ → J ∈ Top
10 1 topopn ⊢ J ∈ Top → X ∈ J
11 9 10 syl ⊢ φ → X ∈ J
12 11 2 ssexd ⊢ φ → A ∈ V
13 elrestr ⊢ J ∈ Top ∧ A ∈ V ∧ B ∈ J → B ∩ A ∈ J ↾ 𝑡 A
14 9 12 4 13 syl3anc ⊢ φ → B ∩ A ∈ J ↾ 𝑡 A
15 eqid ⊢ B ∩ A = B ∩ A
16 ineq1 ⊢ x = B → x ∩ A = B ∩ A
17 16 rspceeqv ⊢ B ∈ Clsd ⁡ J ∧ B ∩ A = B ∩ A → ∃ x ∈ Clsd ⁡ J B ∩ A = x ∩ A
18 6 15 17 sylancl ⊢ φ → ∃ x ∈ Clsd ⁡ J B ∩ A = x ∩ A
19 1 restcld ⊢ J ∈ Top ∧ A ⊆ X → B ∩ A ∈ Clsd ⁡ J ↾ 𝑡 A ↔ ∃ x ∈ Clsd ⁡ J B ∩ A = x ∩ A
20 9 2 19 syl2anc ⊢ φ → B ∩ A ∈ Clsd ⁡ J ↾ 𝑡 A ↔ ∃ x ∈ Clsd ⁡ J B ∩ A = x ∩ A
21 18 20 mpbird ⊢ φ → B ∩ A ∈ Clsd ⁡ J ↾ 𝑡 A
22 7 3 14 5 21 connclo ⊢ φ → B ∩ A = ⋃ J ↾ 𝑡 A
23 1 restuni ⊢ J ∈ Top ∧ A ⊆ X → A = ⋃ J ↾ 𝑡 A
24 9 2 23 syl2anc ⊢ φ → A = ⋃ J ↾ 𝑡 A
25 22 24 eqtr4d ⊢ φ → B ∩ A = A
26 sseqin2 ⊢ A ⊆ B ↔ B ∩ A = A
27 25 26 sylibr ⊢ φ → A ⊆ B