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

Metamath Proof Explorer

Theorem conncompclo

Description: The connected component containing A is a subset of any clopen set containing A . (Contributed by Mario Carneiro, 20-Sep-2015)

Ref Expression
Hypothesis conncomp.2 ⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
Assertion conncompclo ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝑆 ⊆ 𝑇 )

Proof

Step Hyp Ref Expression
1 conncomp.2 ⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
2 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
3 simp1 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 simp2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) )
5 4 elin1d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝑇 ∈ 𝐽 )
6 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ 𝐽 ) → 𝑇 ⊆ 𝑋 )
7 3 5 6 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝑇 ⊆ 𝑋 )
8 simp3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ∈ 𝑇 )
9 7 8 sseldd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ∈ 𝑋 )
10 1 conncompcld ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
11 3 9 10 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
12 2 cldss ⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → 𝑆 ⊆ ∪ 𝐽 )
13 11 12 syl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝑆 ⊆ ∪ 𝐽 )
14 1 conncompconn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t 𝑆 ) ∈ Conn )
15 3 9 14 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝐽 ↾t 𝑆 ) ∈ Conn )
16 1 conncompid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑆 )
17 3 9 16 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝐴 ∈ 𝑆 )
18 inelcm ⊢ ( ( 𝐴 ∈ 𝑇 ∧ 𝐴 ∈ 𝑆 ) → ( 𝑇 ∩ 𝑆 ) ≠ ∅ )
19 8 17 18 syl2anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → ( 𝑇 ∩ 𝑆 ) ≠ ∅ )
20 4 elin2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
21 2 13 15 5 19 20 connsubclo ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑇 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝑆 ⊆ 𝑇 )