Metamath Proof Explorer

Theorem iscnp3

Description: The predicate "the class F is a continuous function from topology J to topology K at point P ". (Contributed by NM, 15-May-2007)

Ref Expression
Assertion iscnp3 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ P ∈ X → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ x ⊆ F -1 y

Proof

Step Hyp Ref Expression
1 iscnp ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ P ∈ X → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y
2 ffun ⊢ F : X ⟶ Y → Fun ⁡ F
3 2 ad2antlr ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ Y ∧ x ∈ J → Fun ⁡ F
4 toponss ⊢ J ∈ TopOn ⁡ X ∧ x ∈ J → x ⊆ X
5 4 adantlr ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ Y ∧ x ∈ J → x ⊆ X
6 fdm ⊢ F : X ⟶ Y → dom ⁡ F = X
7 6 ad2antlr ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ Y ∧ x ∈ J → dom ⁡ F = X
8 5 7 sseqtrrd ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ Y ∧ x ∈ J → x ⊆ dom ⁡ F
9 funimass3 ⊢ Fun ⁡ F ∧ x ⊆ dom ⁡ F → F x ⊆ y ↔ x ⊆ F -1 y
10 3 8 9 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ Y ∧ x ∈ J → F x ⊆ y ↔ x ⊆ F -1 y
11 10 anbi2d ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ Y ∧ x ∈ J → P ∈ x ∧ F x ⊆ y ↔ P ∈ x ∧ x ⊆ F -1 y
12 11 rexbidva ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ Y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ↔ ∃ x ∈ J P ∈ x ∧ x ⊆ F -1 y
13 12 imbi2d ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ Y → F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ↔ F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ x ⊆ F -1 y
14 13 ralbidv ⊢ J ∈ TopOn ⁡ X ∧ F : X ⟶ Y → ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ↔ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ x ⊆ F -1 y
15 14 pm5.32da ⊢ J ∈ TopOn ⁡ X → F : X ⟶ Y ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ↔ F : X ⟶ Y ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ x ⊆ F -1 y
16 15 3ad2ant1 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ P ∈ X → F : X ⟶ Y ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ↔ F : X ⟶ Y ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ x ⊆ F -1 y
17 1 16 bitrd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ P ∈ X → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ x ⊆ F -1 y