Metamath Proof Explorer

Theorem 1stccnp

Description: A mapping is continuous at P in a first-countable space X iff it is sequentially continuous at P , meaning that the image under F of every sequence converging at P converges to F ( P ) . This proof uses ax-cc , but only via 1stcelcls , so it could be refactored into a proof that continuity and sequential continuity are the same in sequential spaces. (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 ) )
1stccnp.4 
|- ( ph -> P e. X )
Assertion 1stccnp 
|- ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) )

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 1stccnp.4 
 |-  ( ph -> P e. X )
5 2 3 jca 
 |-  ( ph -> ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) )
6 cnpf2 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
7 6 3expa 
 |-  ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) ) /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
8 5 7 sylan 
 |-  ( ( ph /\ F e. ( ( J CnP K ) ` P ) ) -> F : X --> Y )
9 simprr 
 |-  ( ( ( ph /\ F e. ( ( J CnP K ) ` P ) ) /\ ( f : NN --> X /\ f ( ~~>t ` J ) P ) ) -> f ( ~~>t ` J ) P )
10 simplr 
 |-  ( ( ( ph /\ F e. ( ( J CnP K ) ` P ) ) /\ ( f : NN --> X /\ f ( ~~>t ` J ) P ) ) -> F e. ( ( J CnP K ) ` P ) )
11 9 10 lmcnp 
 |-  ( ( ( ph /\ F e. ( ( J CnP K ) ` P ) ) /\ ( f : NN --> X /\ f ( ~~>t ` J ) P ) ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) )
12 11 ex 
 |-  ( ( ph /\ F e. ( ( J CnP K ) ` P ) ) -> ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) )
13 12 alrimiv 
 |-  ( ( ph /\ F e. ( ( J CnP K ) ` P ) ) -> A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) )
14 8 13 jca 
 |-  ( ( ph /\ F e. ( ( J CnP K ) ` P ) ) -> ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) )
15 simprl 
 |-  ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) -> F : X --> Y )
16 fal 
 |-  -. F.
17 19.29 
 |-  ( ( A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) /\ E. f ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) -> E. f ( ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) /\ ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) )
18 simprl 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) -> f : NN --> ( X \ ( `' F " u ) ) )
19 difss 
 |-  ( X \ ( `' F " u ) ) C_ X
20 fss 
 |-  ( ( f : NN --> ( X \ ( `' F " u ) ) /\ ( X \ ( `' F " u ) ) C_ X ) -> f : NN --> X )
21 18 19 20 sylancl 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) -> f : NN --> X )
22 simprr 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) -> f ( ~~>t ` J ) P )
23 21 22 jca 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) -> ( f : NN --> X /\ f ( ~~>t ` J ) P ) )
24 nnuz 
 |-  NN = ( ZZ>= ` 1 )
25 simplrr 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) -> ( F ` P ) e. u )
26 1zzd 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) -> 1 e. ZZ )
27 simprr 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) )
28 simplrl 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) -> u e. K )
29 24 25 26 27 28 lmcvg 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F o. f ) ` k ) e. u )
30 24 r19.2uz 
 |-  ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F o. f ) ` k ) e. u -> E. k e. NN ( ( F o. f ) ` k ) e. u )
31 simprll 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) -> f : NN --> ( X \ ( `' F " u ) ) )
32 31 ffnd 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) -> f Fn NN )
33 fvco2 
 |-  ( ( f Fn NN /\ k e. NN ) -> ( ( F o. f ) ` k ) = ( F ` ( f ` k ) ) )
34 32 33 sylan 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> ( ( F o. f ) ` k ) = ( F ` ( f ` k ) ) )
35 34 eleq1d 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> ( ( ( F o. f ) ` k ) e. u <-> ( F ` ( f ` k ) ) e. u ) )
36 31 ffvelcdmda 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> ( f ` k ) e. ( X \ ( `' F " u ) ) )
37 36 eldifad 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> ( f ` k ) e. X )
38 simplr 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> F : X --> Y )
39 38 ad2antrr 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> F : X --> Y )
40 ffn 
 |-  ( F : X --> Y -> F Fn X )
41 elpreima 
 |-  ( F Fn X -> ( ( f ` k ) e. ( `' F " u ) <-> ( ( f ` k ) e. X /\ ( F ` ( f ` k ) ) e. u ) ) )
42 39 40 41 3syl 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> ( ( f ` k ) e. ( `' F " u ) <-> ( ( f ` k ) e. X /\ ( F ` ( f ` k ) ) e. u ) ) )
43 36 eldifbd 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> -. ( f ` k ) e. ( `' F " u ) )
44 43 pm2.21d 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> ( ( f ` k ) e. ( `' F " u ) -> F. ) )
45 42 44 sylbird 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> ( ( ( f ` k ) e. X /\ ( F ` ( f ` k ) ) e. u ) -> F. ) )
46 37 45 mpand 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> ( ( F ` ( f ` k ) ) e. u -> F. ) )
47 35 46 sylbid 
 |-  ( ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) /\ k e. NN ) -> ( ( ( F o. f ) ` k ) e. u -> F. ) )
48 47 rexlimdva 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) -> ( E. k e. NN ( ( F o. f ) ` k ) e. u -> F. ) )
49 30 48 syl5 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( F o. f ) ` k ) e. u -> F. ) )
50 29 49 mpd 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) /\ ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) -> F. )
51 50 expr 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) -> ( ( F o. f ) ( ~~>t ` K ) ( F ` P ) -> F. ) )
52 23 51 embantd 
 |-  ( ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) -> ( ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) -> F. ) )
53 52 ex 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> ( ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) -> ( ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) -> F. ) ) )
54 53 impcomd 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> ( ( ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) /\ ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) -> F. ) )
55 54 exlimdv 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> ( E. f ( ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) /\ ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) -> F. ) )
56 17 55 syl5 
 |-  ( ( ( ph /\ F : X --> Y ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> ( ( A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) /\ E. f ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) -> F. ) )
57 56 exp4b 
 |-  ( ( ph /\ F : X --> Y ) -> ( ( u e. K /\ ( F ` P ) e. u ) -> ( A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) -> ( E. f ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) -> F. ) ) ) )
58 57 com23 
 |-  ( ( ph /\ F : X --> Y ) -> ( A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) -> ( ( u e. K /\ ( F ` P ) e. u ) -> ( E. f ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) -> F. ) ) ) )
59 58 impr 
 |-  ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) -> ( ( u e. K /\ ( F ` P ) e. u ) -> ( E. f ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) -> F. ) ) )
60 59 imp 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> ( E. f ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) -> F. ) )
61 16 60 mtoi 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> -. E. f ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) )
62 1 ad2antrr 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> J e. 1stc )
63 2 ad2antrr 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> J e. ( TopOn ` X ) )
64 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
65 63 64 syl 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> X = U. J )
66 19 65 sseqtrid 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> ( X \ ( `' F " u ) ) C_ U. J )
67 eqid 
 |-  U. J = U. J
68 67 1stcelcls 
 |-  ( ( J e. 1stc /\ ( X \ ( `' F " u ) ) C_ U. J ) -> ( P e. ( ( cls ` J ) ` ( X \ ( `' F " u ) ) ) <-> E. f ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) )
69 62 66 68 syl2anc 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> ( P e. ( ( cls ` J ) ` ( X \ ( `' F " u ) ) ) <-> E. f ( f : NN --> ( X \ ( `' F " u ) ) /\ f ( ~~>t ` J ) P ) ) )
70 61 69 mtbird 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> -. P e. ( ( cls ` J ) ` ( X \ ( `' F " u ) ) ) )
71 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
72 63 71 syl 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> J e. Top )
73 4 ad2antrr 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> P e. X )
74 73 65 eleqtrd 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> P e. U. J )
75 67 elcls 
 |-  ( ( J e. Top /\ ( X \ ( `' F " u ) ) C_ U. J /\ P e. U. J ) -> ( P e. ( ( cls ` J ) ` ( X \ ( `' F " u ) ) ) <-> A. v e. J ( P e. v -> ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) ) ) )
76 72 66 74 75 syl3anc 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> ( P e. ( ( cls ` J ) ` ( X \ ( `' F " u ) ) ) <-> A. v e. J ( P e. v -> ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) ) ) )
77 70 76 mtbid 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> -. A. v e. J ( P e. v -> ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) ) )
78 15 ad2antrr 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> F : X --> Y )
79 78 ffund 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> Fun F )
80 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ v e. J ) -> v C_ X )
81 63 80 sylan 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> v C_ X )
82 78 fdmd 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> dom F = X )
83 81 82 sseqtrrd 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> v C_ dom F )
84 funimass3 
 |-  ( ( Fun F /\ v C_ dom F ) -> ( ( F " v ) C_ u <-> v C_ ( `' F " u ) ) )
85 79 83 84 syl2anc 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> ( ( F " v ) C_ u <-> v C_ ( `' F " u ) ) )
86 dfss2 
 |-  ( v C_ X <-> ( v i^i X ) = v )
87 81 86 sylib 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> ( v i^i X ) = v )
88 87 sseq1d 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> ( ( v i^i X ) C_ ( `' F " u ) <-> v C_ ( `' F " u ) ) )
89 85 88 bitr4d 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> ( ( F " v ) C_ u <-> ( v i^i X ) C_ ( `' F " u ) ) )
90 nne 
 |-  ( -. ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) <-> ( v i^i ( X \ ( `' F " u ) ) ) = (/) )
91 inssdif0 
 |-  ( ( v i^i X ) C_ ( `' F " u ) <-> ( v i^i ( X \ ( `' F " u ) ) ) = (/) )
92 90 91 bitr4i 
 |-  ( -. ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) <-> ( v i^i X ) C_ ( `' F " u ) )
93 89 92 bitr4di 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> ( ( F " v ) C_ u <-> -. ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) ) )
94 93 anbi2d 
 |-  ( ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) /\ v e. J ) -> ( ( P e. v /\ ( F " v ) C_ u ) <-> ( P e. v /\ -. ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) ) ) )
95 94 rexbidva 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> ( E. v e. J ( P e. v /\ ( F " v ) C_ u ) <-> E. v e. J ( P e. v /\ -. ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) ) ) )
96 rexanali 
 |-  ( E. v e. J ( P e. v /\ -. ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) ) <-> -. A. v e. J ( P e. v -> ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) ) )
97 95 96 bitrdi 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> ( E. v e. J ( P e. v /\ ( F " v ) C_ u ) <-> -. A. v e. J ( P e. v -> ( v i^i ( X \ ( `' F " u ) ) ) =/= (/) ) ) )
98 77 97 mpbird 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ ( u e. K /\ ( F ` P ) e. u ) ) -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) )
99 98 expr 
 |-  ( ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) /\ u e. K ) -> ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) )
100 99 ralrimiva 
 |-  ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) -> A. u e. K ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) )
101 iscnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` Y ) /\ P e. X ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. u e. K ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) ) )
102 2 3 4 101 syl3anc 
 |-  ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. u e. K ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) ) )
103 102 adantr 
 |-  ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. u e. K ( ( F ` P ) e. u -> E. v e. J ( P e. v /\ ( F " v ) C_ u ) ) ) ) )
104 15 100 103 mpbir2and 
 |-  ( ( ph /\ ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) -> F e. ( ( J CnP K ) ` P ) )
105 14 104 impbida 
 |-  ( ph -> ( F e. ( ( J CnP K ) ` P ) <-> ( F : X --> Y /\ A. f ( ( f : NN --> X /\ f ( ~~>t ` J ) P ) -> ( F o. f ) ( ~~>t ` K ) ( F ` P ) ) ) ) )