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

Proof

Step Hyp Ref Expression
1 conncomp.2 ⊢ S = ⋃ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn
2 uniiun ⊢ ⋃ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn = ⋃ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn y
3 1 2 eqtri ⊢ S = ⋃ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn y
4 3 oveq2i ⊢ J ↾ 𝑡 S = J ↾ 𝑡 ⋃ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn y
5 simpl ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → J ∈ TopOn ⁡ X
6 eleq2w ⊢ x = y → A ∈ x ↔ A ∈ y
7 oveq2 ⊢ x = y → J ↾ 𝑡 x = J ↾ 𝑡 y
8 7 eleq1d ⊢ x = y → J ↾ 𝑡 x ∈ Conn ↔ J ↾ 𝑡 y ∈ Conn
9 6 8 anbi12d ⊢ x = y → A ∈ x ∧ J ↾ 𝑡 x ∈ Conn ↔ A ∈ y ∧ J ↾ 𝑡 y ∈ Conn
10 9 elrab ⊢ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn ↔ y ∈ 𝒫 X ∧ A ∈ y ∧ J ↾ 𝑡 y ∈ Conn
11 10 bilani ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X ∧ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn → y ∈ 𝒫 X ∧ A ∈ y ∧ J ↾ 𝑡 y ∈ Conn
12 11 simpld ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X ∧ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn → y ∈ 𝒫 X
13 12 elpwid ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X ∧ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn → y ⊆ X
14 11 simprd ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X ∧ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn → A ∈ y ∧ J ↾ 𝑡 y ∈ Conn
15 14 simpld ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X ∧ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn → A ∈ y
16 14 simprd ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X ∧ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn → J ↾ 𝑡 y ∈ Conn
17 5 13 15 16 iunconn ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → J ↾ 𝑡 ⋃ y ∈ x ∈ 𝒫 X | A ∈ x ∧ J ↾ 𝑡 x ∈ Conn y ∈ Conn
18 4 17 eqeltrid ⊢ J ∈ TopOn ⁡ X ∧ A ∈ X → J ↾ 𝑡 S ∈ Conn