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∈JCnK↔F:X⟶Y∧∀f∈Fil⁡X∀x∈JfClusfF⁡x∈KfClusff⁡F

Proof

Step Hyp Ref Expression
1 cncnp ⊢J∈TopOn⁡X∧K∈TopOn⁡Y→F∈JCnK↔F:X⟶Y∧∀x∈XF∈JCnPK⁡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∈JCnPK⁡x↔F:X⟶Y∧∀f∈Fil⁡Xx∈JfClusf→F⁡x∈KfClusff⁡F
4 3 ad4ant124 ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧x∈X→F∈JCnPK⁡x↔F:X⟶Y∧∀f∈Fil⁡Xx∈JfClusf→F⁡x∈KfClusff⁡F
5 2 4 mpbirand ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧x∈X→F∈JCnPK⁡x↔∀f∈Fil⁡Xx∈JfClusf→F⁡x∈KfClusff⁡F
6 5 ralbidva ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→∀x∈XF∈JCnPK⁡x↔∀x∈X∀f∈Fil⁡Xx∈JfClusf→F⁡x∈KfClusff⁡F
7 ralcom ⊢∀x∈X∀f∈Fil⁡Xx∈JfClusf→F⁡x∈KfClusff⁡F↔∀f∈Fil⁡X∀x∈Xx∈JfClusf→F⁡x∈KfClusff⁡F
8 eqid ⊢⋃J=⋃J
9 8 fclselbas ⊢x∈JfClusf→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∈JfClusf→x∈X
14 13 pm4.71rd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→x∈JfClusf↔x∈X∧x∈JfClusf
15 14 imbi1d ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→x∈JfClusf→F⁡x∈KfClusff⁡F↔x∈X∧x∈JfClusf→F⁡x∈KfClusff⁡F
16 impexp ⊢x∈X∧x∈JfClusf→F⁡x∈KfClusff⁡F↔x∈X→x∈JfClusf→F⁡x∈KfClusff⁡F
17 15 16 bitrdi ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→x∈JfClusf→F⁡x∈KfClusff⁡F↔x∈X→x∈JfClusf→F⁡x∈KfClusff⁡F
18 17 ralbidv2 ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→∀x∈JfClusfF⁡x∈KfClusff⁡F↔∀x∈Xx∈JfClusf→F⁡x∈KfClusff⁡F
19 18 ralbidv ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→∀f∈Fil⁡X∀x∈JfClusfF⁡x∈KfClusff⁡F↔∀f∈Fil⁡X∀x∈Xx∈JfClusf→F⁡x∈KfClusff⁡F
20 7 19 bitr4id ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→∀x∈X∀f∈Fil⁡Xx∈JfClusf→F⁡x∈KfClusff⁡F↔∀f∈Fil⁡X∀x∈JfClusfF⁡x∈KfClusff⁡F
21 6 20 bitrd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→∀x∈XF∈JCnPK⁡x↔∀f∈Fil⁡X∀x∈JfClusfF⁡x∈KfClusff⁡F
22 21 pm5.32da ⊢J∈TopOn⁡X∧K∈TopOn⁡Y→F:X⟶Y∧∀x∈XF∈JCnPK⁡x↔F:X⟶Y∧∀f∈Fil⁡X∀x∈JfClusfF⁡x∈KfClusff⁡F
23 1 22 bitrd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y→F∈JCnK↔F:X⟶Y∧∀f∈Fil⁡X∀x∈JfClusfF⁡x∈KfClusff⁡F