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

Metamath Proof Explorer

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 simpr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
7 eleq2w ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
8 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐽 ↾t 𝑥 ) = ( 𝐽 ↾t 𝑦 ) )
9 8 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐽 ↾t 𝑥 ) ∈ Conn ↔ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) )
10 7 9 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ↔ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) )
11 10 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ↔ ( 𝑦 ∈ 𝒫 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) )
12 6 11 sylib ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → ( 𝑦 ∈ 𝒫 𝑋 ∧ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) )
13 12 simpld ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → 𝑦 ∈ 𝒫 𝑋 )
14 13 elpwid ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → 𝑦 ⊆ 𝑋 )
15 12 simprd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) )
16 15 simpld ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → 𝐴 ∈ 𝑦 )
17 15 simprd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ) → ( 𝐽 ↾t 𝑦 ) ∈ Conn )
18 5 14 16 17 iunconn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t ∪ 𝑦 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } 𝑦 ) ∈ Conn )
19 4 18 eqeltrid ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t 𝑆 ) ∈ Conn )