Metamath Proof Explorer

Theorem cnprcl2

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

Ref Expression
Assertion cnprcl2 ⊢ J ∈ TopOn ⁡ X ∧ F ∈ J CnP K ⁡ P → P ∈ X

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ J = ⋃ J
2 1 cnprcl ⊢ F ∈ J CnP K ⁡ P → P ∈ ⋃ J
3 2 adantl ⊢ J ∈ TopOn ⁡ X ∧ F ∈ J CnP K ⁡ P → P ∈ ⋃ J
4 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
5 4 adantr ⊢ J ∈ TopOn ⁡ X ∧ F ∈ J CnP K ⁡ P → X = ⋃ J
6 3 5 eleqtrrd ⊢ J ∈ TopOn ⁡ X ∧ F ∈ J CnP K ⁡ P → P ∈ X