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 ⊢S=⋃x∈𝒫X|A∈x∧J↾𝑡x∈Conn
Assertion conncompid ⊢J∈TopOn⁡X∧A∈X→A∈S

Proof

Step Hyp Ref Expression
1 conncomp.2 ⊢S=⋃x∈𝒫X|A∈x∧J↾𝑡x∈Conn
2 simpr ⊢J∈TopOn⁡X∧A∈X→A∈X
3 2 snssd ⊢J∈TopOn⁡X∧A∈X→A⊆X
4 snex ⊢A∈V
5 4 elpw ⊢A∈𝒫X↔A⊆X
6 3 5 sylibr ⊢J∈TopOn⁡X∧A∈X→A∈𝒫X
7 snidg ⊢A∈X→A∈A
8 7 adantl ⊢J∈TopOn⁡X∧A∈X→A∈A
9 restsn2 ⊢J∈TopOn⁡X∧A∈X→J↾𝑡A=𝒫A
10 pwsn ⊢𝒫A=∅A
11 indisconn ⊢∅A∈Conn
12 10 11 eqeltri ⊢𝒫A∈Conn
13 9 12 eqeltrdi ⊢J∈TopOn⁡X∧A∈X→J↾𝑡A∈Conn
14 8 13 jca ⊢J∈TopOn⁡X∧A∈X→A∈A∧J↾𝑡A∈Conn
15 eleq2 ⊢x=A→A∈x↔A∈A
16 oveq2 ⊢x=A→J↾𝑡x=J↾𝑡A
17 16 eleq1d ⊢x=A→J↾𝑡x∈Conn↔J↾𝑡A∈Conn
18 15 17 anbi12d ⊢x=A→A∈x∧J↾𝑡x∈Conn↔A∈A∧J↾𝑡A∈Conn
19 15 18 anbi12d ⊢x=A→A∈x∧A∈x∧J↾𝑡x∈Conn↔A∈A∧A∈A∧J↾𝑡A∈Conn
20 19 rspcev ⊢A∈𝒫X∧A∈A∧A∈A∧J↾𝑡A∈Conn→∃x∈𝒫XA∈x∧A∈x∧J↾𝑡x∈Conn
21 6 8 14 20 syl12anc ⊢J∈TopOn⁡X∧A∈X→∃x∈𝒫XA∈x∧A∈x∧J↾𝑡x∈Conn
22 elunirab ⊢A∈⋃x∈𝒫X|A∈x∧J↾𝑡x∈Conn↔∃x∈𝒫XA∈x∧A∈x∧J↾𝑡x∈Conn
23 21 22 sylibr ⊢J∈TopOn⁡X∧A∈X→A∈⋃x∈𝒫X|A∈x∧J↾𝑡x∈Conn
24 23 1 eleqtrrdi ⊢J∈TopOn⁡X∧A∈X→A∈S