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 ⊢ 𝑋 = ∪ 𝐽
connsubclo.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
connsubclo.4 ⊢ ( 𝜑 → ( 𝐽 ↾t 𝐴 ) ∈ Conn )
connsubclo.5 ⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
connsubclo.6 ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) ≠ ∅ )
connsubclo.7 ⊢ ( 𝜑 → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
Assertion connsubclo ( 𝜑 → 𝐴 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 connsubclo.1 ⊢ 𝑋 = ∪ 𝐽
2 connsubclo.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
3 connsubclo.4 ⊢ ( 𝜑 → ( 𝐽 ↾t 𝐴 ) ∈ Conn )
4 connsubclo.5 ⊢ ( 𝜑 → 𝐵 ∈ 𝐽 )
5 connsubclo.6 ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) ≠ ∅ )
6 connsubclo.7 ⊢ ( 𝜑 → 𝐵 ∈ ( Clsd ‘ 𝐽 ) )
7 eqid ⊢ ∪ ( 𝐽 ↾t 𝐴 ) = ∪ ( 𝐽 ↾t 𝐴 )
8 cldrcl ⊢ ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) → 𝐽 ∈ Top )
9 6 8 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
10 1 topopn ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ 𝐽 )
11 9 10 syl ⊢ ( 𝜑 → 𝑋 ∈ 𝐽 )
12 11 2 ssexd ⊢ ( 𝜑 → 𝐴 ∈ V )
13 elrestr ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ V ∧ 𝐵 ∈ 𝐽 ) → ( 𝐵 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
14 9 12 4 13 syl3anc ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) ∈ ( 𝐽 ↾t 𝐴 ) )
15 eqid ⊢ ( 𝐵 ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 )
16 ineq1 ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 ) )
17 16 rspceeqv ⊢ ( ( 𝐵 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝐵 ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 ) ) → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐵 ∩ 𝐴 ) = ( 𝑥 ∩ 𝐴 ) )
18 6 15 17 sylancl ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐵 ∩ 𝐴 ) = ( 𝑥 ∩ 𝐴 ) )
19 1 restcld ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → ( ( 𝐵 ∩ 𝐴 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐵 ∩ 𝐴 ) = ( 𝑥 ∩ 𝐴 ) ) )
20 9 2 19 syl2anc ⊢ ( 𝜑 → ( ( 𝐵 ∩ 𝐴 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) ↔ ∃ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ( 𝐵 ∩ 𝐴 ) = ( 𝑥 ∩ 𝐴 ) ) )
21 18 20 mpbird ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) ∈ ( Clsd ‘ ( 𝐽 ↾t 𝐴 ) ) )
22 7 3 14 5 21 connclo ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) = ∪ ( 𝐽 ↾t 𝐴 ) )
23 1 restuni ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ) → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
24 9 2 23 syl2anc ⊢ ( 𝜑 → 𝐴 = ∪ ( 𝐽 ↾t 𝐴 ) )
25 22 24 eqtr4d ⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) = 𝐴 )
26 sseqin2 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐵 ∩ 𝐴 ) = 𝐴 )
27 25 26 sylibr ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )