Metamath Proof Explorer

Theorem cnflf

Description: A function is continuous iff it respects filter limits. (Contributed by Jeff Hankins, 6-Sep-2009) (Revised by Stefan O'Rear, 7-Aug-2015)

Ref Expression
Assertion 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

Proof

Step Hyp Ref Expression
1 cncnp ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ x ∈ X F ∈ J CnP K ⁡ x
2 simplr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ X → F : X ⟶ Y
3 cnpflf ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ x ∈ X → F ∈ J CnP K ⁡ x ↔ F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
4 3 ad4ant124 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ X → F ∈ J CnP K ⁡ x ↔ F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
5 2 4 mpbirand ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y ∧ x ∈ X → F ∈ J CnP K ⁡ x ↔ ∀ f ∈ Fil ⁡ X x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
6 5 ralbidva ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ x ∈ X F ∈ J CnP K ⁡ x ↔ ∀ x ∈ X ∀ f ∈ Fil ⁡ X x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
7 eqid ⊢ ⋃ J = ⋃ J
8 7 flimelbas ⊢ x ∈ J fLim f → x ∈ ⋃ J
9 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
10 9 ad2antrr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → X = ⋃ J
11 10 eleq2d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ X ↔ x ∈ ⋃ J
12 8 11 syl5ibr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ J fLim f → x ∈ X
13 12 pm4.71rd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ J fLim f ↔ x ∈ X ∧ x ∈ J fLim f
14 13 imbi1d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F ↔ x ∈ X ∧ x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
15 impexp ⊢ x ∈ X ∧ x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F ↔ x ∈ X → x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
16 14 15 bitrdi ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F ↔ x ∈ X → x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
17 16 ralbidv2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ x ∈ J fLim f F ⁡ x ∈ K fLimf f ⁡ F ↔ ∀ x ∈ X x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
18 17 ralbidv ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ f ∈ Fil ⁡ X ∀ x ∈ J fLim f F ⁡ x ∈ K fLimf f ⁡ F ↔ ∀ f ∈ Fil ⁡ X ∀ x ∈ X x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
19 ralcom ⊢ ∀ f ∈ Fil ⁡ X ∀ x ∈ X x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F ↔ ∀ x ∈ X ∀ f ∈ Fil ⁡ X x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
20 18 19 bitrdi ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ f ∈ Fil ⁡ X ∀ x ∈ J fLim f F ⁡ x ∈ K fLimf f ⁡ F ↔ ∀ x ∈ X ∀ f ∈ Fil ⁡ X x ∈ J fLim f → F ⁡ x ∈ K fLimf f ⁡ F
21 6 20 bitr4d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ x ∈ X F ∈ J CnP K ⁡ x ↔ ∀ f ∈ Fil ⁡ X ∀ x ∈ J fLim f F ⁡ x ∈ K fLimf f ⁡ F
22 21 pm5.32da ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F : X ⟶ Y ∧ ∀ x ∈ X F ∈ J CnP K ⁡ x ↔ F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X ∀ x ∈ J fLim f F ⁡ x ∈ K fLimf f ⁡ F
23 1 22 bitrd ⊢ 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