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 ‘ 𝐽 ) ) ∧ 𝐴 ∈ 𝑇 ) → 𝑆 ⊆ 𝑇 )