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 ) )