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∈JCnK↔F:X⟶Y∧∀f∈Fil⁡X∀x∈JfLimfF⁡x∈KfLimff⁡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 cnpflf ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧x∈X→F∈JCnPK⁡x↔F:X⟶Y∧∀f∈Fil⁡Xx∈JfLimf→F⁡x∈KfLimff⁡F
4 3 ad4ant124 ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧x∈X→F∈JCnPK⁡x↔F:X⟶Y∧∀f∈Fil⁡Xx∈JfLimf→F⁡x∈KfLimff⁡F
5 2 4 mpbirand ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧x∈X→F∈JCnPK⁡x↔∀f∈Fil⁡Xx∈JfLimf→F⁡x∈KfLimff⁡F
6 5 ralbidva ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→∀x∈XF∈JCnPK⁡x↔∀x∈X∀f∈Fil⁡Xx∈JfLimf→F⁡x∈KfLimff⁡F
7 eqid ⊢⋃J=⋃J
8 7 flimelbas ⊢x∈JfLimf→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 imbitrrid ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→x∈JfLimf→x∈X
13 12 pm4.71rd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→x∈JfLimf↔x∈X∧x∈JfLimf
14 13 imbi1d ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→x∈JfLimf→F⁡x∈KfLimff⁡F↔x∈X∧x∈JfLimf→F⁡x∈KfLimff⁡F
15 impexp ⊢x∈X∧x∈JfLimf→F⁡x∈KfLimff⁡F↔x∈X→x∈JfLimf→F⁡x∈KfLimff⁡F
16 14 15 bitrdi ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→x∈JfLimf→F⁡x∈KfLimff⁡F↔x∈X→x∈JfLimf→F⁡x∈KfLimff⁡F
17 16 ralbidv2 ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→∀x∈JfLimfF⁡x∈KfLimff⁡F↔∀x∈Xx∈JfLimf→F⁡x∈KfLimff⁡F
18 17 ralbidv ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→∀f∈Fil⁡X∀x∈JfLimfF⁡x∈KfLimff⁡F↔∀f∈Fil⁡X∀x∈Xx∈JfLimf→F⁡x∈KfLimff⁡F
19 ralcom ⊢∀f∈Fil⁡X∀x∈Xx∈JfLimf→F⁡x∈KfLimff⁡F↔∀x∈X∀f∈Fil⁡Xx∈JfLimf→F⁡x∈KfLimff⁡F
20 18 19 bitrdi ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→∀f∈Fil⁡X∀x∈JfLimfF⁡x∈KfLimff⁡F↔∀x∈X∀f∈Fil⁡Xx∈JfLimf→F⁡x∈KfLimff⁡F
21 6 20 bitr4d ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→∀x∈XF∈JCnPK⁡x↔∀f∈Fil⁡X∀x∈JfLimfF⁡x∈KfLimff⁡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∈JfLimfF⁡x∈KfLimff⁡F
23 1 22 bitrd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y→F∈JCnK↔F:X⟶Y∧∀f∈Fil⁡X∀x∈JfLimfF⁡x∈KfLimff⁡F