Metamath Proof Explorer

Theorem iscn2

Description: The predicate "the class F is a continuous function from topology J to topology K ". Definition of continuous function in Munkres p. 102. (Contributed by Mario Carneiro, 21-Aug-2015)

Ref Expression
Hypotheses iscn.1 ⊢ X = ⋃ J
iscn.2 ⊢ Y = ⋃ K
Assertion iscn2 ⊢ F ∈ J Cn K ↔ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J

Proof

Step Hyp Ref Expression
1 iscn.1 ⊢ X = ⋃ J
2 iscn.2 ⊢ Y = ⋃ K
3 df-cn ⊢ Cn = j ∈ Top , k ∈ Top ⟼ f ∈ ⋃ k ⋃ j | ∀ y ∈ k f -1 y ∈ j
4 3 elmpocl ⊢ F ∈ J Cn K → J ∈ Top ∧ K ∈ Top
5 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
6 2 toptopon ⊢ K ∈ Top ↔ K ∈ TopOn ⁡ Y
7 iscn ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J
8 5 6 7 syl2anb ⊢ J ∈ Top ∧ K ∈ Top → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J
9 4 8 biadanii ⊢ F ∈ J Cn K ↔ J ∈ Top ∧ K ∈ Top ∧ F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J