Metamath Proof Explorer

Theorem 1stccn

Description: A mapping X --> Y , where X is first-countable, is continuous iff it is sequentially continuous, meaning that for any sequence f ( n ) converging to x , its image under F converges to F ( x ) . (Contributed by Mario Carneiro, 7-Sep-2015)

Ref Expression
Hypotheses 1stccnp.1 
|- ( ph -> J e. 1stc )
1stccnp.2 
|- ( ph -> J e. ( TopOn ` X ) )
1stccnp.3 
|- ( ph -> K e. ( TopOn ` Y ) )
1stccn.7 
|- ( ph -> F : X --> Y )
Assertion 1stccn 
|- ( ph -> ( F e. ( J Cn K ) <-> A. f ( f : NN --> X -> A. x ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 1stccnp.1 
 |-  ( ph -> J e. 1stc )
2 1stccnp.2 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 1stccnp.3 
 |-  ( ph -> K e. ( TopOn ` Y ) )
4 1stccn.7 
 |-  ( ph -> F : X --> Y )
5 cncnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) )
6 2 3 5 syl2anc 
 |-  ( ph -> ( F e. ( J Cn K ) <-> ( F : X --> Y /\ A. x e. X F e. ( ( J CnP K ) ` x ) ) ) )
7 4 6 mpbirand 
 |-  ( ph -> ( F e. ( J Cn K ) <-> A. x e. X F e. ( ( J CnP K ) ` x ) ) )
8 4 adantr 
 |-  ( ( ph /\ x e. X ) -> F : X --> Y )
9 1 adantr 
 |-  ( ( ph /\ x e. X ) -> J e. 1stc )
10 2 adantr 
 |-  ( ( ph /\ x e. X ) -> J e. ( TopOn ` X ) )
11 3 adantr 
 |-  ( ( ph /\ x e. X ) -> K e. ( TopOn ` Y ) )
12 simpr 
 |-  ( ( ph /\ x e. X ) -> x e. X )
13 9 10 11 12 1stccnp 
 |-  ( ( ph /\ x e. X ) -> ( F e. ( ( J CnP K ) ` x ) <-> ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) ) )
14 8 13 mpbirand 
 |-  ( ( ph /\ x e. X ) -> ( F e. ( ( J CnP K ) ` x ) <-> A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
15 14 ralbidva 
 |-  ( ph -> ( A. x e. X F e. ( ( J CnP K ) ` x ) <-> A. x e. X A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
16 ralcom4 
 |-  ( A. x e. X A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> A. f A. x e. X ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) )
17 impexp 
 |-  ( ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> ( f : NN --> X -> ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
18 17 ralbii 
 |-  ( A. x e. X ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> A. x e. X ( f : NN --> X -> ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
19 r19.21v 
 |-  ( A. x e. X ( f : NN --> X -> ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) <-> ( f : NN --> X -> A. x e. X ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
20 18 19 bitri 
 |-  ( A. x e. X ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> ( f : NN --> X -> A. x e. X ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
21 df-ral 
 |-  ( A. x e. X ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> A. x ( x e. X -> ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
22 lmcl 
 |-  ( ( J e. ( TopOn ` X ) /\ f ( ~~>t ` J ) x ) -> x e. X )
23 2 22 sylan 
 |-  ( ( ph /\ f ( ~~>t ` J ) x ) -> x e. X )
24 23 ex 
 |-  ( ph -> ( f ( ~~>t ` J ) x -> x e. X ) )
25 24 pm4.71rd 
 |-  ( ph -> ( f ( ~~>t ` J ) x <-> ( x e. X /\ f ( ~~>t ` J ) x ) ) )
26 25 imbi1d 
 |-  ( ph -> ( ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> ( ( x e. X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
27 impexp 
 |-  ( ( ( x e. X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> ( x e. X -> ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
28 26 27 bitr2di 
 |-  ( ph -> ( ( x e. X -> ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) <-> ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
29 28 albidv 
 |-  ( ph -> ( A. x ( x e. X -> ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) <-> A. x ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
30 21 29 syl5bb 
 |-  ( ph -> ( A. x e. X ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> A. x ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) )
31 30 imbi2d 
 |-  ( ph -> ( ( f : NN --> X -> A. x e. X ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) <-> ( f : NN --> X -> A. x ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) ) )
32 20 31 syl5bb 
 |-  ( ph -> ( A. x e. X ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> ( f : NN --> X -> A. x ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) ) )
33 32 albidv 
 |-  ( ph -> ( A. f A. x e. X ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> A. f ( f : NN --> X -> A. x ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) ) )
34 16 33 syl5bb 
 |-  ( ph -> ( A. x e. X A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) x ) -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) <-> A. f ( f : NN --> X -> A. x ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) ) )
35 7 15 34 3bitrd 
 |-  ( ph -> ( F e. ( J Cn K ) <-> A. f ( f : NN --> X -> A. x ( f ( ~~>t ` J ) x -> ( F o. f ) ( ~~>t ` K ) ( F ` x ) ) ) ) )