Theorem cnmpt21f 19245

Description: The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.)

Hypotheses

Ref	Expression
cnmpt21.j	|- ( ph -> J e. (TopOn ` X ) )
cnmpt21.k	|- ( ph -> K e. (TopOn ` Y ) )
cnmpt21.a	|- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
cnmpt21f.f	|- ( ph -> F e. ( L Cn M ) )

Assertion

Ref	Expression
cnmpt21f	|- ( ph -> ( x e. X , y e. Y |-> ( F ` A ) ) e. ( ( J tX K ) Cn M ) )

Distinct variable groups:   x, y, F   x, L, y   ph, x, y   x, X, y   x, M, y   x, Y, y

Allowed substitution hints:   A( x, y)   J( x, y)   K( x, y)

Proof of Theorem cnmpt21f

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cnmpt21.j	. 2 |- ( ph -> J e. (TopOn ` X ) )
2		cnmpt21.k	. 2 |- ( ph -> K e. (TopOn ` Y ) )
3		cnmpt21.a	. 2 |- ( ph -> ( x e. X , y e. Y |-> A ) e. ( ( J tX K ) Cn L ) )
4		cnmpt21f.f	. . . 4 |- ( ph -> F e. ( L Cn M ) )
5		cntop1 18844	. . . 4 |- ( F e. ( L Cn M ) -> L e. Top )
6	4, 5	syl 16	. . 3 |- ( ph -> L e. Top )
7		eqid 2443	. . . 4 |- U. L = U. L
8	7	toptopon 18538	. . 3 |- ( L e. Top <-> L e. (TopOn ` U. L ) )
9	6, 8	sylib 196	. 2 |- ( ph -> L e. (TopOn ` U. L ) )
10		eqid 2443	. . . . . 6 |- U. M = U. M
11	7, 10	cnf 18850	. . . . 5 |- ( F e. ( L Cn M ) -> F : U. L --> U. M )
12	4, 11	syl 16	. . . 4 |- ( ph -> F : U. L --> U. M )
13	12	feqmptd 5744	. . 3 |- ( ph -> F = ( z e. U. L |-> ( F ` z ) ) )
14	13, 4	eqeltrrd 2518	. 2 |- ( ph -> ( z e. U. L |-> ( F ` z ) ) e. ( L Cn M ) )
15		fveq2 5691	. 2 |- ( z = A -> ( F ` z ) = ( F ` A ) )
16	1, 2, 3, 9, 14, 15	cnmpt21 19244	1 |- ( ph -> ( x e. X , y e. Y |-> ( F ` A ) ) e. ( ( J tX K ) Cn M ) )

Syntax hints:   -> wi 4   e. wcel 1756   U.cuni 4091   e. cmpt 4350   -->wf 5414   ` cfv 5418  (class class class)co 6091   e. cmpt2 6093   Topctop 18498  TopOnctopon 18499   Cn ccn 18828   tX ctx 19133

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-1st 6577  df-2nd 6578  df-map 7216  df-topgen 14382  df-top 18503  df-bases 18505  df-topon 18506  df-cn 18831  df-tx 19135

This theorem is referenced by:  cnmpt22  19247  cnmptk2  19259  txhmeo  19376  tgpsubcn  19661  istgp2  19662  dvrcn  19758  htpyid  20549  htpyco1  20550  reparphti  20569  pcocn  20589  pcorevlem  20598  cxpcn  22183  dipcn  24118  mndpluscn  26356  cvxscon  27132  cvmlift2lem6  27197  cvmlift2lem12  27203