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 ∈ 𝒫 X A ∈ x ∧ A ∈ x ∧ J ↾ 𝑡 x ∈ Conn
21 6 8 14 20 syl12anc ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → ∃ x ∈ 𝒫 X A ∈ x ∧ A ∈ x ∧ J ↾ 𝑡 x ∈ Conn
22 elunirab ⊢ A ∈ ⋃ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn ↔ ∃ x ∈ 𝒫 X A ∈ 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