Metamath Proof Explorer

Theorem conncompss

Description: The connected component containing A is a superset of any other connected set containing A . (Contributed by Mario Carneiro, 19-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 conncomp.2 ⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
2 simp1 ⊢ ( ( 𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) → 𝑇 ⊆ 𝑋 )
3 conntop ⊢ ( ( 𝐽 ↾t 𝑇 ) ∈ Conn → ( 𝐽 ↾t 𝑇 ) ∈ Top )
4 3 3ad2ant3 ⊢ ( ( 𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) → ( 𝐽 ↾t 𝑇 ) ∈ Top )
5 restrcl ⊢ ( ( 𝐽 ↾t 𝑇 ) ∈ Top → ( 𝐽 ∈ V ∧ 𝑇 ∈ V ) )
6 5 simprd ⊢ ( ( 𝐽 ↾t 𝑇 ) ∈ Top → 𝑇 ∈ V )
7 elpwg ⊢ ( 𝑇 ∈ V → ( 𝑇 ∈ 𝒫 𝑋 ↔ 𝑇 ⊆ 𝑋 ) )
8 4 6 7 3syl ⊢ ( ( 𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) → ( 𝑇 ∈ 𝒫 𝑋 ↔ 𝑇 ⊆ 𝑋 ) )
9 2 8 mpbird ⊢ ( ( 𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) → 𝑇 ∈ 𝒫 𝑋 )
10 3simpc ⊢ ( ( 𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) → ( 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) )
11 eleq2 ⊢ ( 𝑦 = 𝑇 → ( 𝐴 ∈ 𝑦 ↔ 𝐴 ∈ 𝑇 ) )
12 oveq2 ⊢ ( 𝑦 = 𝑇 → ( 𝐽 ↾t 𝑦 ) = ( 𝐽 ↾t 𝑇 ) )
13 12 eleq1d ⊢ ( 𝑦 = 𝑇 → ( ( 𝐽 ↾t 𝑦 ) ∈ Conn ↔ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) )
14 11 13 anbi12d ⊢ ( 𝑦 = 𝑇 → ( ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ↔ ( 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) ) )
15 eleq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
16 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐽 ↾t 𝑥 ) = ( 𝐽 ↾t 𝑦 ) )
17 16 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐽 ↾t 𝑥 ) ∈ Conn ↔ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) )
18 15 17 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ↔ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) ) )
19 18 cbvrabv ⊢ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } = { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑦 ∧ ( 𝐽 ↾t 𝑦 ) ∈ Conn ) }
20 14 19 elrab2 ⊢ ( 𝑇 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ↔ ( 𝑇 ∈ 𝒫 𝑋 ∧ ( 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) ) )
21 9 10 20 sylanbrc ⊢ ( ( 𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) → 𝑇 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
22 elssuni ⊢ ( 𝑇 ∈ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } → 𝑇 ⊆ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
23 21 22 syl ⊢ ( ( 𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) → 𝑇 ⊆ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
24 23 1 sseqtrrdi ⊢ ( ( 𝑇 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑇 ∧ ( 𝐽 ↾t 𝑇 ) ∈ Conn ) → 𝑇 ⊆ 𝑆 )