Metamath Proof Explorer

Theorem cnptop1

Description: Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion cnptop1 ⊢ F ∈ J CnP K ⁡ P → J ∈ Top

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 eqid ⊢ ⋃ K = ⋃ K
3 1 2 iscnp2 ⊢ F ∈ J CnP K ⁡ P ↔ J ∈ Top ∧ K ∈ Top ∧ P ∈ ⋃ J ∧ F : ⋃ J ⟶ ⋃ K ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y
4 3 simplbi ⊢ F ∈ J CnP K ⁡ P → J ∈ Top ∧ K ∈ Top ∧ P ∈ ⋃ J
5 4 simp1d ⊢ F ∈ J CnP K ⁡ P → J ∈ Top