Metamath Proof Explorer

Theorem cnnei

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

Ref Expression
Hypotheses cnnei.x 
|- X = U. J
cnnei.y 
|- Y = U. K
Assertion cnnei 
|- ( ( J e. Top /\ K e. Top /\ F : X --> Y ) -> ( F e. ( J Cn K ) <-> A. p e. X A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) )

Proof

Step Hyp Ref Expression
1 cnnei.x 
 |-  X = U. J
2 cnnei.y 
 |-  Y = U. K
3 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
4 2 toptopon 
 |-  ( K e. Top <-> K e. ( TopOn ` Y ) )
5 3 4 anbi12i 
 |-  ( ( J e. Top /\ K e. Top ) <-> ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) )
6 cncnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. p e. X F e. ( ( J CnP K ) ` p ) ) ) )
7 6 baibd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) -> ( F e. ( J Cn K ) <-> A. p e. X F e. ( ( J CnP K ) ` p ) ) )
8 5 7 sylanb 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ F : X --> Y ) -> ( F e. ( J Cn K ) <-> A. p e. X F e. ( ( J CnP K ) ` p ) ) )
9 5 anbi1i 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ F : X --> Y ) <-> ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) )
10 iscnp4 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ p e. X ) -> ( F e. ( ( J CnP K ) ` p ) <-> ( F : X --> Y /\ A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) ) )
11 10 3expa 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ p e. X ) -> ( F e. ( ( J CnP K ) ` p ) <-> ( F : X --> Y /\ A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) ) )
12 11 baibd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ p e. X ) /\ F : X --> Y ) -> ( F e. ( ( J CnP K ) ` p ) <-> A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) )
13 12 an32s 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F : X --> Y ) /\ p e. X ) -> ( F e. ( ( J CnP K ) ` p ) <-> A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) )
14 9 13 sylanb 
 |-  ( ( ( ( J e. Top /\ K e. Top ) /\ F : X --> Y ) /\ p e. X ) -> ( F e. ( ( J CnP K ) ` p ) <-> A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) )
15 14 ralbidva 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ F : X --> Y ) -> ( A. p e. X F e. ( ( J CnP K ) ` p ) <-> A. p e. X A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) )
16 8 15 bitrd 
 |-  ( ( ( J e. Top /\ K e. Top ) /\ F : X --> Y ) -> ( F e. ( J Cn K ) <-> A. p e. X A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) )
17 16 3impa 
 |-  ( ( J e. Top /\ K e. Top /\ F : X --> Y ) -> ( F e. ( J Cn K ) <-> A. p e. X A. w e. ( ( nei ` K ) ` { ( F ` p ) } ) E. v e. ( ( nei ` J ) ` { p } ) ( F " v ) C_ w ) )