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

Metamath Proof Explorer

Theorem conncompid

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

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

Proof

Step Hyp Ref Expression
1 conncomp.2 ⊢ 𝑆 = ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) }
2 simpr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
3 2 snssd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → { 𝐴 } ⊆ 𝑋 )
4 snex ⊢ { 𝐴 } ∈ V
5 4 elpw ⊢ ( { 𝐴 } ∈ 𝒫 𝑋 ↔ { 𝐴 } ⊆ 𝑋 )
6 3 5 sylibr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → { 𝐴 } ∈ 𝒫 𝑋 )
7 snidg ⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ { 𝐴 } )
8 7 adantl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ { 𝐴 } )
9 restsn2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t { 𝐴 } ) = 𝒫 { 𝐴 } )
10 pwsn ⊢ 𝒫 { 𝐴 } = { ∅ , { 𝐴 } }
11 indisconn ⊢ { ∅ , { 𝐴 } } ∈ Conn
12 10 11 eqeltri ⊢ 𝒫 { 𝐴 } ∈ Conn
13 9 12 eqeltrdi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐽 ↾t { 𝐴 } ) ∈ Conn )
14 8 13 jca ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐽 ↾t { 𝐴 } ) ∈ Conn ) )
15 eleq2 ⊢ ( 𝑥 = { 𝐴 } → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ { 𝐴 } ) )
16 oveq2 ⊢ ( 𝑥 = { 𝐴 } → ( 𝐽 ↾t 𝑥 ) = ( 𝐽 ↾t { 𝐴 } ) )
17 16 eleq1d ⊢ ( 𝑥 = { 𝐴 } → ( ( 𝐽 ↾t 𝑥 ) ∈ Conn ↔ ( 𝐽 ↾t { 𝐴 } ) ∈ Conn ) )
18 15 17 anbi12d ⊢ ( 𝑥 = { 𝐴 } → ( ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ↔ ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐽 ↾t { 𝐴 } ) ∈ Conn ) ) )
19 15 18 anbi12d ⊢ ( 𝑥 = { 𝐴 } → ( ( 𝐴 ∈ 𝑥 ∧ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ) ↔ ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐽 ↾t { 𝐴 } ) ∈ Conn ) ) ) )
20 19 rspcev ⊢ ( ( { 𝐴 } ∈ 𝒫 𝑋 ∧ ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐴 ∈ { 𝐴 } ∧ ( 𝐽 ↾t { 𝐴 } ) ∈ Conn ) ) ) → ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝐴 ∈ 𝑥 ∧ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ) )
21 6 8 14 20 syl12anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝐴 ∈ 𝑥 ∧ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ) )
22 elunirab ⊢ ( 𝐴 ∈ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } ↔ ∃ 𝑥 ∈ 𝒫 𝑋 ( 𝐴 ∈ 𝑥 ∧ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) ) )
23 21 22 sylibr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ ∪ { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐴 ∈ 𝑥 ∧ ( 𝐽 ↾t 𝑥 ) ∈ Conn ) } )
24 23 1 eleqtrrdi ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → 𝐴 ∈ 𝑆 )