Metamath Proof Explorer

Theorem ptcnp

Description: If every projection of a function is continuous at D , then the function itself is continuous at D into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses ptcnp.2 
|- K = ( Xt_ ` F )
ptcnp.3 
|- ( ph -> J e. ( TopOn ` X ) )
ptcnp.4 
|- ( ph -> I e. V )
ptcnp.5 
|- ( ph -> F : I --> Top )
ptcnp.6 
|- ( ph -> D e. X )
ptcnp.7 
|- ( ( ph /\ k e. I ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` D ) )
Assertion ptcnp 
|- ( ph -> ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` D ) )

Proof

Step Hyp Ref Expression
1 ptcnp.2 
 |-  K = ( Xt_ ` F )
2 ptcnp.3 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 ptcnp.4 
 |-  ( ph -> I e. V )
4 ptcnp.5 
 |-  ( ph -> F : I --> Top )
5 ptcnp.6 
 |-  ( ph -> D e. X )
6 ptcnp.7 
 |-  ( ( ph /\ k e. I ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` D ) )
7 2 adantr 
 |-  ( ( ph /\ k e. I ) -> J e. ( TopOn ` X ) )
8 4 ffvelrnda 
 |-  ( ( ph /\ k e. I ) -> ( F ` k ) e. Top )
9 toptopon2 
 |-  ( ( F ` k ) e. Top <-> ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) )
10 8 9 sylib 
 |-  ( ( ph /\ k e. I ) -> ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) )
11 cnpf2 
 |-  ( ( J e. ( TopOn ` X ) /\ ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) /\ ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` D ) ) -> ( x e. X |-> A ) : X --> U. ( F ` k ) )
12 7 10 6 11 syl3anc 
 |-  ( ( ph /\ k e. I ) -> ( x e. X |-> A ) : X --> U. ( F ` k ) )
13 12 fvmptelrn 
 |-  ( ( ( ph /\ k e. I ) /\ x e. X ) -> A e. U. ( F ` k ) )
14 13 an32s 
 |-  ( ( ( ph /\ x e. X ) /\ k e. I ) -> A e. U. ( F ` k ) )
15 14 ralrimiva 
 |-  ( ( ph /\ x e. X ) -> A. k e. I A e. U. ( F ` k ) )
16 3 adantr 
 |-  ( ( ph /\ x e. X ) -> I e. V )
17 mptelixpg 
 |-  ( I e. V -> ( ( k e. I |-> A ) e. X_ k e. I U. ( F ` k ) <-> A. k e. I A e. U. ( F ` k ) ) )
18 16 17 syl 
 |-  ( ( ph /\ x e. X ) -> ( ( k e. I |-> A ) e. X_ k e. I U. ( F ` k ) <-> A. k e. I A e. U. ( F ` k ) ) )
19 15 18 mpbird 
 |-  ( ( ph /\ x e. X ) -> ( k e. I |-> A ) e. X_ k e. I U. ( F ` k ) )
20 19 fmpttd 
 |-  ( ph -> ( x e. X |-> ( k e. I |-> A ) ) : X --> X_ k e. I U. ( F ` k ) )
21 df-3an 
 |-  ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) <-> ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) )
22 nfv 
 |-  F/ k ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) )
23 nfv 
 |-  F/ k ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) )
24 nfcv 
 |-  F/_ k X
25 nfmpt1 
 |-  F/_ k ( k e. I |-> A )
26 24 25 nfmpt 
 |-  F/_ k ( x e. X |-> ( k e. I |-> A ) )
27 nfcv 
 |-  F/_ k D
28 26 27 nffv 
 |-  F/_ k ( ( x e. X |-> ( k e. I |-> A ) ) ` D )
29 28 nfel1 
 |-  F/ k ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n )
30 23 29 nfan 
 |-  F/ k ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) )
31 22 30 nfan 
 |-  F/ k ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) )
32 simprll 
 |-  ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) ) -> g Fn I )
33 simprlr 
 |-  ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) ) -> A. n e. I ( g ` n ) e. ( F ` n ) )
34 fveq2 
 |-  ( n = k -> ( g ` n ) = ( g ` k ) )
35 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
36 34 35 eleq12d 
 |-  ( n = k -> ( ( g ` n ) e. ( F ` n ) <-> ( g ` k ) e. ( F ` k ) ) )
37 36 rspccva 
 |-  ( ( A. n e. I ( g ` n ) e. ( F ` n ) /\ k e. I ) -> ( g ` k ) e. ( F ` k ) )
38 33 37 sylan 
 |-  ( ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) ) /\ k e. I ) -> ( g ` k ) e. ( F ` k ) )
39 simprrl 
 |-  ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) ) -> ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) )
40 39 simpld 
 |-  ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) ) -> w e. Fin )
41 39 simprd 
 |-  ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) ) -> A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) )
42 35 unieqd 
 |-  ( n = k -> U. ( F ` n ) = U. ( F ` k ) )
43 34 42 eqeq12d 
 |-  ( n = k -> ( ( g ` n ) = U. ( F ` n ) <-> ( g ` k ) = U. ( F ` k ) ) )
44 43 rspccva 
 |-  ( ( A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) /\ k e. ( I \ w ) ) -> ( g ` k ) = U. ( F ` k ) )
45 41 44 sylan 
 |-  ( ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) ) /\ k e. ( I \ w ) ) -> ( g ` k ) = U. ( F ` k ) )
46 simprrr 
 |-  ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) ) -> ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) )
47 34 cbvixpv 
 |-  X_ n e. I ( g ` n ) = X_ k e. I ( g ` k )
48 46 47 eleqtrdi 
 |-  ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) ) -> ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ k e. I ( g ` k ) )
49 1 2 3 4 5 6 31 32 38 40 45 48 ptcnplem 
 |-  ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( g ` k ) ) )
50 49 anassrs 
 |-  ( ( ( ph /\ ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) ) /\ ( ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( g ` k ) ) )
51 50 expr 
 |-  ( ( ( ph /\ ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) ) /\ ( w e. Fin /\ A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( g ` k ) ) ) )
52 51 rexlimdvaa 
 |-  ( ( ph /\ ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) ) -> ( E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( g ` k ) ) ) ) )
53 52 impr 
 |-  ( ( ph /\ ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( g ` k ) ) ) )
54 21 53 sylan2b 
 |-  ( ( ph /\ ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( g ` k ) ) ) )
55 eleq2 
 |-  ( f = X_ n e. I ( g ` n ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. f <-> ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) ) )
56 47 eqeq2i 
 |-  ( f = X_ n e. I ( g ` n ) <-> f = X_ k e. I ( g ` k ) )
57 56 biimpi 
 |-  ( f = X_ n e. I ( g ` n ) -> f = X_ k e. I ( g ` k ) )
58 57 sseq2d 
 |-  ( f = X_ n e. I ( g ` n ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f <-> ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( g ` k ) ) )
59 58 anbi2d 
 |-  ( f = X_ n e. I ( g ` n ) -> ( ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) <-> ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( g ` k ) ) ) )
60 59 rexbidv 
 |-  ( f = X_ n e. I ( g ` n ) -> ( E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) <-> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( g ` k ) ) ) )
61 55 60 imbi12d 
 |-  ( f = X_ n e. I ( g ` n ) -> ( ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. f -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) ) <-> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. X_ n e. I ( g ` n ) -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ X_ k e. I ( g ` k ) ) ) ) )
62 54 61 syl5ibrcom 
 |-  ( ( ph /\ ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) ) -> ( f = X_ n e. I ( g ` n ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. f -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) ) ) )
63 62 expimpd 
 |-  ( ph -> ( ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ f = X_ n e. I ( g ` n ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. f -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) ) ) )
64 63 exlimdv 
 |-  ( ph -> ( E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ f = X_ n e. I ( g ` n ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. f -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) ) ) )
65 64 alrimiv 
 |-  ( ph -> A. f ( E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ f = X_ n e. I ( g ` n ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. f -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) ) ) )
66 eqeq1 
 |-  ( a = f -> ( a = X_ n e. I ( g ` n ) <-> f = X_ n e. I ( g ` n ) ) )
67 66 anbi2d 
 |-  ( a = f -> ( ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ a = X_ n e. I ( g ` n ) ) <-> ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ f = X_ n e. I ( g ` n ) ) ) )
68 67 exbidv 
 |-  ( a = f -> ( E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ a = X_ n e. I ( g ` n ) ) <-> E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ f = X_ n e. I ( g ` n ) ) ) )
69 68 ralab 
 |-  ( A. f e. { a | E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ a = X_ n e. I ( g ` n ) ) } ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. f -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) ) <-> A. f ( E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ f = X_ n e. I ( g ` n ) ) -> ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. f -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) ) ) )
70 65 69 sylibr 
 |-  ( ph -> A. f e. { a | E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ a = X_ n e. I ( g ` n ) ) } ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. f -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) ) )
71 4 ffnd 
 |-  ( ph -> F Fn I )
72 eqid 
 |-  { a | E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ a = X_ n e. I ( g ` n ) ) } = { a | E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ a = X_ n e. I ( g ` n ) ) }
73 72 ptval 
 |-  ( ( I e. V /\ F Fn I ) -> ( Xt_ ` F ) = ( topGen ` { a | E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ a = X_ n e. I ( g ` n ) ) } ) )
74 3 71 73 syl2anc 
 |-  ( ph -> ( Xt_ ` F ) = ( topGen ` { a | E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ a = X_ n e. I ( g ` n ) ) } ) )
75 1 74 syl5eq 
 |-  ( ph -> K = ( topGen ` { a | E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ a = X_ n e. I ( g ` n ) ) } ) )
76 4 feqmptd 
 |-  ( ph -> F = ( k e. I |-> ( F ` k ) ) )
77 76 fveq2d 
 |-  ( ph -> ( Xt_ ` F ) = ( Xt_ ` ( k e. I |-> ( F ` k ) ) ) )
78 1 77 syl5eq 
 |-  ( ph -> K = ( Xt_ ` ( k e. I |-> ( F ` k ) ) ) )
79 10 ralrimiva 
 |-  ( ph -> A. k e. I ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) )
80 eqid 
 |-  ( Xt_ ` ( k e. I |-> ( F ` k ) ) ) = ( Xt_ ` ( k e. I |-> ( F ` k ) ) )
81 80 pttopon 
 |-  ( ( I e. V /\ A. k e. I ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) ) -> ( Xt_ ` ( k e. I |-> ( F ` k ) ) ) e. ( TopOn ` X_ k e. I U. ( F ` k ) ) )
82 3 79 81 syl2anc 
 |-  ( ph -> ( Xt_ ` ( k e. I |-> ( F ` k ) ) ) e. ( TopOn ` X_ k e. I U. ( F ` k ) ) )
83 78 82 eqeltrd 
 |-  ( ph -> K e. ( TopOn ` X_ k e. I U. ( F ` k ) ) )
84 2 75 83 5 tgcnp 
 |-  ( ph -> ( ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` D ) <-> ( ( x e. X |-> ( k e. I |-> A ) ) : X --> X_ k e. I U. ( F ` k ) /\ A. f e. { a | E. g ( ( g Fn I /\ A. n e. I ( g ` n ) e. ( F ` n ) /\ E. w e. Fin A. n e. ( I \ w ) ( g ` n ) = U. ( F ` n ) ) /\ a = X_ n e. I ( g ` n ) ) } ( ( ( x e. X |-> ( k e. I |-> A ) ) ` D ) e. f -> E. z e. J ( D e. z /\ ( ( x e. X |-> ( k e. I |-> A ) ) " z ) C_ f ) ) ) ) )
85 20 70 84 mpbir2and 
 |-  ( ph -> ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` D ) )