Metamath Proof Explorer

Theorem cnfcf

Description: Continuity of a function in terms of cluster points of a function. (Contributed by Jeff Hankins, 28-Nov-2009) (Revised by Stefan O'Rear, 9-Aug-2015)

Ref Expression
Assertion cnfcf ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X ∀ x ∈ J fClus f F ⁡ x ∈ K fClusf 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 cnpfcf ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ x ∈ X → F ∈ J CnP K ⁡ x ↔ F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X x ∈ J fClus f → F ⁡ x ∈ K fClusf 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 fClus f → F ⁡ x ∈ K fClusf 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 fClus f → F ⁡ x ∈ K fClusf 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 fClus f → F ⁡ x ∈ K fClusf f ⁡ F
7 ralcom ⊢ ∀ x ∈ X ∀ f ∈ Fil ⁡ X x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F ↔ ∀ f ∈ Fil ⁡ X ∀ x ∈ X x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F
8 eqid ⊢ ⋃ J = ⋃ J
9 8 fclselbas ⊢ x ∈ J fClus f → x ∈ ⋃ J
10 toponuni ⊢ J ∈ TopOn ⁡ X → X = ⋃ J
11 10 ad2antrr ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → X = ⋃ J
12 11 eleq2d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ X ↔ x ∈ ⋃ J
13 9 12 imbitrrid ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ J fClus f → x ∈ X
14 13 pm4.71rd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ J fClus f ↔ x ∈ X ∧ x ∈ J fClus f
15 14 imbi1d ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F ↔ x ∈ X ∧ x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F
16 impexp ⊢ x ∈ X ∧ x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F ↔ x ∈ X → x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F
17 15 16 bitrdi ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F ↔ x ∈ X → x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F
18 17 ralbidv2 ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ x ∈ J fClus f F ⁡ x ∈ K fClusf f ⁡ F ↔ ∀ x ∈ X x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F
19 18 ralbidv ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ f ∈ Fil ⁡ X ∀ x ∈ J fClus f F ⁡ x ∈ K fClusf f ⁡ F ↔ ∀ f ∈ Fil ⁡ X ∀ x ∈ X x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F
20 7 19 bitr4id ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ x ∈ X ∀ f ∈ Fil ⁡ X x ∈ J fClus f → F ⁡ x ∈ K fClusf f ⁡ F ↔ ∀ f ∈ Fil ⁡ X ∀ x ∈ J fClus f F ⁡ x ∈ K fClusf f ⁡ F
21 6 20 bitrd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ F : X ⟶ Y → ∀ x ∈ X F ∈ J CnP K ⁡ x ↔ ∀ f ∈ Fil ⁡ X ∀ x ∈ J fClus f F ⁡ x ∈ K fClusf 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 fClus f F ⁡ x ∈ K fClusf f ⁡ F
23 1 22 bitrd ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ f ∈ Fil ⁡ X ∀ x ∈ J fClus f F ⁡ x ∈ K fClusf f ⁡ F