Metamath Proof Explorer

Theorem cnnei

Description: Continuity in terms of neighborhoods. (Contributed by Thierry Arnoux, 3-Jan-2018)

Ref Expression
Hypotheses cnnei.x ⊢X=⋃J
cnnei.y ⊢Y=⋃K
Assertion cnnei ⊢J∈Top∧K∈Top∧F:X⟶Y→F∈JCnK↔∀p∈X∀w∈nei⁡K⁡F⁡p∃v∈nei⁡J⁡pFv⊆w

Proof

Step Hyp Ref Expression
1 cnnei.x ⊢X=⋃J
2 cnnei.y ⊢Y=⋃K
3 1 toptopon ⊢J∈Top↔J∈TopOn⁡X
4 2 toptopon ⊢K∈Top↔K∈TopOn⁡Y
5 3 4 anbi12i ⊢J∈Top∧K∈Top↔J∈TopOn⁡X∧K∈TopOn⁡Y
6 cncnp ⊢J∈TopOn⁡X∧K∈TopOn⁡Y→F∈JCnK↔F:X⟶Y∧∀p∈XF∈JCnPK⁡p
7 6 baibd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y→F∈JCnK↔∀p∈XF∈JCnPK⁡p
8 5 7 sylanb ⊢J∈Top∧K∈Top∧F:X⟶Y→F∈JCnK↔∀p∈XF∈JCnPK⁡p
9 5 anbi1i ⊢J∈Top∧K∈Top∧F:X⟶Y↔J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y
10 iscnp4 ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧p∈X→F∈JCnPK⁡p↔F:X⟶Y∧∀w∈nei⁡K⁡F⁡p∃v∈nei⁡J⁡pFv⊆w
11 10 3expa ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧p∈X→F∈JCnPK⁡p↔F:X⟶Y∧∀w∈nei⁡K⁡F⁡p∃v∈nei⁡J⁡pFv⊆w
12 11 baibd ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧p∈X∧F:X⟶Y→F∈JCnPK⁡p↔∀w∈nei⁡K⁡F⁡p∃v∈nei⁡J⁡pFv⊆w
13 12 an32s ⊢J∈TopOn⁡X∧K∈TopOn⁡Y∧F:X⟶Y∧p∈X→F∈JCnPK⁡p↔∀w∈nei⁡K⁡F⁡p∃v∈nei⁡J⁡pFv⊆w
14 9 13 sylanb ⊢J∈Top∧K∈Top∧F:X⟶Y∧p∈X→F∈JCnPK⁡p↔∀w∈nei⁡K⁡F⁡p∃v∈nei⁡J⁡pFv⊆w
15 14 ralbidva ⊢J∈Top∧K∈Top∧F:X⟶Y→∀p∈XF∈JCnPK⁡p↔∀p∈X∀w∈nei⁡K⁡F⁡p∃v∈nei⁡J⁡pFv⊆w
16 8 15 bitrd ⊢J∈Top∧K∈Top∧F:X⟶Y→F∈JCnK↔∀p∈X∀w∈nei⁡K⁡F⁡p∃v∈nei⁡J⁡pFv⊆w
17 16 3impa ⊢J∈Top∧K∈Top∧F:X⟶Y→F∈JCnK↔∀p∈X∀w∈nei⁡K⁡F⁡p∃v∈nei⁡J⁡pFv⊆w