Metamath Proof Explorer

Theorem ptcn

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

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

Proof

Step Hyp Ref Expression
1 ptcn.2 
 |-  K = ( Xt_ ` F )
2 ptcn.3 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 ptcn.4 
 |-  ( ph -> I e. V )
4 ptcn.5 
 |-  ( ph -> F : I --> Top )
5 ptcn.6 
 |-  ( ( ph /\ k e. I ) -> ( x e. X |-> A ) e. ( J Cn ( F ` k ) ) )
6 2 adantr 
 |-  ( ( ph /\ k e. I ) -> J e. ( TopOn ` X ) )
7 4 ffvelrnda 
 |-  ( ( ph /\ k e. I ) -> ( F ` k ) e. Top )
8 toptopon2 
 |-  ( ( F ` k ) e. Top <-> ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) )
9 7 8 sylib 
 |-  ( ( ph /\ k e. I ) -> ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) )
10 cnf2 
 |-  ( ( J e. ( TopOn ` X ) /\ ( F ` k ) e. ( TopOn ` U. ( F ` k ) ) /\ ( x e. X |-> A ) e. ( J Cn ( F ` k ) ) ) -> ( x e. X |-> A ) : X --> U. ( F ` k ) )
11 6 9 5 10 syl3anc 
 |-  ( ( ph /\ k e. I ) -> ( x e. X |-> A ) : X --> U. ( F ` k ) )
12 11 fvmptelrn 
 |-  ( ( ( ph /\ k e. I ) /\ x e. X ) -> A e. U. ( F ` k ) )
13 12 an32s 
 |-  ( ( ( ph /\ x e. X ) /\ k e. I ) -> A e. U. ( F ` k ) )
14 13 ralrimiva 
 |-  ( ( ph /\ x e. X ) -> A. k e. I A e. U. ( F ` k ) )
15 3 adantr 
 |-  ( ( ph /\ x e. X ) -> I e. V )
16 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 ) ) )
17 15 16 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 ) ) )
18 14 17 mpbird 
 |-  ( ( ph /\ x e. X ) -> ( k e. I |-> A ) e. X_ k e. I U. ( F ` k ) )
19 1 ptuni 
 |-  ( ( I e. V /\ F : I --> Top ) -> X_ k e. I U. ( F ` k ) = U. K )
20 3 4 19 syl2anc 
 |-  ( ph -> X_ k e. I U. ( F ` k ) = U. K )
21 20 adantr 
 |-  ( ( ph /\ x e. X ) -> X_ k e. I U. ( F ` k ) = U. K )
22 18 21 eleqtrd 
 |-  ( ( ph /\ x e. X ) -> ( k e. I |-> A ) e. U. K )
23 22 fmpttd 
 |-  ( ph -> ( x e. X |-> ( k e. I |-> A ) ) : X --> U. K )
24 2 adantr 
 |-  ( ( ph /\ z e. X ) -> J e. ( TopOn ` X ) )
25 3 adantr 
 |-  ( ( ph /\ z e. X ) -> I e. V )
26 4 adantr 
 |-  ( ( ph /\ z e. X ) -> F : I --> Top )
27 simpr 
 |-  ( ( ph /\ z e. X ) -> z e. X )
28 5 adantlr 
 |-  ( ( ( ph /\ z e. X ) /\ k e. I ) -> ( x e. X |-> A ) e. ( J Cn ( F ` k ) ) )
29 simplr 
 |-  ( ( ( ph /\ z e. X ) /\ k e. I ) -> z e. X )
30 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
31 2 30 syl 
 |-  ( ph -> X = U. J )
32 31 ad2antrr 
 |-  ( ( ( ph /\ z e. X ) /\ k e. I ) -> X = U. J )
33 29 32 eleqtrd 
 |-  ( ( ( ph /\ z e. X ) /\ k e. I ) -> z e. U. J )
34 eqid 
 |-  U. J = U. J
35 34 cncnpi 
 |-  ( ( ( x e. X |-> A ) e. ( J Cn ( F ` k ) ) /\ z e. U. J ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` z ) )
36 28 33 35 syl2anc 
 |-  ( ( ( ph /\ z e. X ) /\ k e. I ) -> ( x e. X |-> A ) e. ( ( J CnP ( F ` k ) ) ` z ) )
37 1 24 25 26 27 36 ptcnp 
 |-  ( ( ph /\ z e. X ) -> ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` z ) )
38 37 ralrimiva 
 |-  ( ph -> A. z e. X ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` z ) )
39 pttop 
 |-  ( ( I e. V /\ F : I --> Top ) -> ( Xt_ ` F ) e. Top )
40 3 4 39 syl2anc 
 |-  ( ph -> ( Xt_ ` F ) e. Top )
41 1 40 eqeltrid 
 |-  ( ph -> K e. Top )
42 toptopon2 
 |-  ( K e. Top <-> K e. ( TopOn ` U. K ) )
43 41 42 sylib 
 |-  ( ph -> K e. ( TopOn ` U. K ) )
44 cncnp 
 |-  ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` U. K ) ) -> ( ( x e. X |-> ( k e. I |-> A ) ) e. ( J Cn K ) <-> ( ( x e. X |-> ( k e. I |-> A ) ) : X --> U. K /\ A. z e. X ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` z ) ) ) )
45 2 43 44 syl2anc 
 |-  ( ph -> ( ( x e. X |-> ( k e. I |-> A ) ) e. ( J Cn K ) <-> ( ( x e. X |-> ( k e. I |-> A ) ) : X --> U. K /\ A. z e. X ( x e. X |-> ( k e. I |-> A ) ) e. ( ( J CnP K ) ` z ) ) ) )
46 23 38 45 mpbir2and 
 |-  ( ph -> ( x e. X |-> ( k e. I |-> A ) ) e. ( J Cn K ) )