Theorem conncompconn

Description: The connected component containing A is connected. (Contributed by Mario Carneiro, 19-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		conncomp.2	⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
2		uniiun	⊢ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } = ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } 𝑦
3	1 2	eqtri	⊢ 𝑆 = ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } 𝑦
4	3	oveq2i	⊢ ( 𝐽 ↾t 𝑆 ) = ( 𝐽 ↾t ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } 𝑦 )
5		simpl	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
6		eleq2w	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
7		oveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐽 ↾t 𝑥 ) = ( 𝐽 ↾t 𝑦 ) )
8	7	eleq1d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐽 ↾t 𝑥 ) ∈ Conn ↔ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) )
9	6 8	anbi12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ↔ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) )
10	9	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) )
11	10	bilani	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → ( 𝑦 ∈ 𝒫 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) )
12	11	simpld	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → 𝑦 ∈ 𝒫 𝑋 )
13	12	elpwid	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → 𝑦 ⊆ 𝑋 )
14	11	simprd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) )
15	14	simpld	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → 𝐴 ∈ 𝑦 )
16	14	simprd	⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → ( 𝐽 ↾t 𝑦 ) ∈ Conn )
17	5 13 15 16	iunconn	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } 𝑦 ) ∈ Conn )
18	4 17	eqeltrid	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t 𝑆 ) ∈ Conn )