Metamath Proof Explorer

Theorem cnflf2

Description: A function is continuous iff it respects filter limits. (Contributed by Mario Carneiro, 9-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion cnflf2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X F J fLim f ⊆ K fLimf f ⁡ F

Proof

Step Hyp Ref Expression
1 cnflf ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X ∀ x ∈ J fLim f F ⁡ x ∈ K fLimf f ⁡ F
2 ffun ⊢ F : X ⟶ Y → Fun ⁡ F
3 eqid ⊢ ⋃ J = ⋃ J
4 3 flimelbas ⊢ x ∈ J fLim f → x ∈ ⋃ J
5 4 ssriv ⊢ J fLim f ⊆ ⋃ J
6 fdm ⊢ F : X ⟶ Y → dom ⁡ F = X
7 6 adantl ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → dom ⁡ F = X
8 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
9 8 ad2antrr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → X = ⋃ J
10 7 9 eqtrd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → dom ⁡ F = ⋃ J
11 5 10 sseqtrrid ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → J fLim f ⊆ dom ⁡ F
12 funimass4 ⊢ Fun ⁡ F ∧ J fLim f ⊆ dom ⁡ F → F J fLim f ⊆ K fLimf f ⁡ F ↔ ∀ x ∈ J fLim f F ⁡ x ∈ K fLimf f ⁡ F
13 2 11 12 syl2an2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → F J fLim f ⊆ K fLimf f ⁡ F ↔ ∀ x ∈ J fLim f F ⁡ x ∈ K fLimf f ⁡ F
14 13 ralbidv ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ f ∈ Fil ⁡ X F J fLim f ⊆ K fLimf f ⁡ F ↔ ∀ f ∈ Fil ⁡ X ∀ x ∈ J fLim f F ⁡ x ∈ K fLimf f ⁡ F
15 14 pm5.32da ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X F J fLim f ⊆ K fLimf f ⁡ F ↔ F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X ∀ x ∈ J fLim f F ⁡ x ∈ K fLimf f ⁡ F
16 1 15 bitr4d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X F J fLim f ⊆ K fLimf f ⁡ F