Metamath Proof Explorer

Theorem iscn

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 NM, 17-Oct-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion iscn ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J

Proof

Step Hyp Ref Expression
1 cnfval ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → J Cn K = f ∈ Y X | ∀ y ∈ K f -1 y ∈ J
2 1 eleq2d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F ∈ f ∈ Y X | ∀ y ∈ K f -1 y ∈ J
3 cnveq ⊢ f = F → f -1 = F -1
4 3 imaeq1d ⊢ f = F → f -1 y = F -1 y
5 4 eleq1d ⊢ f = F → f -1 y ∈ J ↔ F -1 y ∈ J
6 5 ralbidv ⊢ f = F → ∀ y ∈ K f -1 y ∈ J ↔ ∀ y ∈ K F -1 y ∈ J
7 6 elrab ⊢ F ∈ f ∈ Y X | ∀ y ∈ K f -1 y ∈ J ↔ F ∈ Y X ∧ ∀ y ∈ K F -1 y ∈ J
8 toponmax ⊢ K ∈ TopOn ⁡ Y → Y ∈ K
9 toponmax ⊢ J ∈ TopOn ⁡ X → X ∈ J
10 elmapg ⊢ Y ∈ K ∧ X ∈ J → F ∈ Y X ↔ F : X ⟶ Y
11 8 9 10 syl2anr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ Y X ↔ F : X ⟶ Y
12 11 anbi1d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ Y X ∧ ∀ y ∈ K F -1 y ∈ J ↔ F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J
13 7 12 bitrid ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ f ∈ Y X | ∀ y ∈ K f -1 y ∈ J ↔ F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J
14 2 13 bitrd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J