Theorem ptpjcn 19143

Description: Continuity of a projection map into a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Feb-2015.)

Hypotheses

Ref	Expression
ptpjcn.1	|- Y = U. J
ptpjcn.2	|- J = ( Xt_ ` F )

Assertion

Ref	Expression
ptpjcn	|- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( x e. Y |-> ( x ` I ) ) e. ( J Cn ( F ` I ) ) )

Distinct variable groups:   x, A   x, F   x, I   x, V   x, Y

Allowed substitution hint:   J( x)

Proof of Theorem ptpjcn

Dummy variables g k u w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptpjcn.2	. . . . . 6 |- J = ( Xt_ ` F )
2	1	ptuni 19126	. . . . 5 |- ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. J )
3	2	3adant3 1003	. . . 4 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> X_ k e. A U. ( F ` k ) = U. J )
4		ptpjcn.1	. . . 4 |- Y = U. J
5	3, 4	syl6reqr 2492	. . 3 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> Y = X_ k e. A U. ( F ` k ) )
6	5	mpteq1d 4370	. 2 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( x e. Y |-> ( x ` I ) ) = ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) )
7		pttop 19114	. . . . . 6 |- ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) e. Top )
8	7	3adant3 1003	. . . . 5 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( Xt_ ` F ) e. Top )
9	1, 8	syl5eqel 2525	. . . 4 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> J e. Top )
10		ffvelrn 5838	. . . . 5 |- ( ( F : A --> Top /\ I e. A ) -> ( F ` I ) e. Top )
11	10	3adant1 1001	. . . 4 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( F ` I ) e. Top )
12	9, 11	jca 529	. . 3 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( J e. Top /\ ( F ` I ) e. Top ) )
13		vex 2973	. . . . . . . . . 10 |- x e. _V
14	13	elixp 7266	. . . . . . . . 9 |- ( x e. X_ k e. A U. ( F ` k ) <-> ( x Fn A /\ A. k e. A ( x ` k ) e. U. ( F ` k ) ) )
15	14	simprbi 461	. . . . . . . 8 |- ( x e. X_ k e. A U. ( F ` k ) -> A. k e. A ( x ` k ) e. U. ( F ` k ) )
16		fveq2 5688	. . . . . . . . . 10 |- ( k = I -> ( x ` k ) = ( x ` I ) )
17		fveq2 5688	. . . . . . . . . . 11 |- ( k = I -> ( F ` k ) = ( F ` I ) )
18	17	unieqd 4098	. . . . . . . . . 10 |- ( k = I -> U. ( F ` k ) = U. ( F ` I ) )
19	16, 18	eleq12d 2509	. . . . . . . . 9 |- ( k = I -> ( ( x ` k ) e. U. ( F ` k ) <-> ( x ` I ) e. U. ( F ` I ) ) )
20	19	rspcva 3068	. . . . . . . 8 |- ( ( I e. A /\ A. k e. A ( x ` k ) e. U. ( F ` k ) ) -> ( x ` I ) e. U. ( F ` I ) )
21	15, 20	sylan2 471	. . . . . . 7 |- ( ( I e. A /\ x e. X_ k e. A U. ( F ` k ) ) -> ( x ` I ) e. U. ( F ` I ) )
22	21	3ad2antl3 1147	. . . . . 6 |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ x e. X_ k e. A U. ( F ` k ) ) -> ( x ` I ) e. U. ( F ` I ) )
23		eqid 2441	. . . . . 6 |- ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) = ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) )
24	22, 23	fmptd 5864	. . . . 5 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) : X_ k e. A U. ( F ` k ) --> U. ( F ` I ) )
25	5	feq2d 5544	. . . . 5 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) : Y --> U. ( F ` I ) <-> ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) : X_ k e. A U. ( F ` k ) --> U. ( F ` I ) ) )
26	24, 25	mpbird 232	. . . 4 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) : Y --> U. ( F ` I ) )
27		eqid 2441	. . . . . . . . . . . 12 |- { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } = { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) }
28	27	ptbas 19111	. . . . . . . . . . 11 |- ( ( A e. V /\ F : A --> Top ) -> { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } e. TopBases )
29		bastg 18530	. . . . . . . . . . 11 |- ( { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } e. TopBases -> { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } C_ ( topGen ` { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } ) )
30	28, 29	syl 16	. . . . . . . . . 10 |- ( ( A e. V /\ F : A --> Top ) -> { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } C_ ( topGen ` { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } ) )
31		ffn 5556	. . . . . . . . . . 11 |- ( F : A --> Top -> F Fn A )
32	27	ptval 19102	. . . . . . . . . . . 12 |- ( ( A e. V /\ F Fn A ) -> ( Xt_ ` F ) = ( topGen ` { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } ) )
33	1, 32	syl5eq 2485	. . . . . . . . . . 11 |- ( ( A e. V /\ F Fn A ) -> J = ( topGen ` { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } ) )
34	31, 33	sylan2 471	. . . . . . . . . 10 |- ( ( A e. V /\ F : A --> Top ) -> J = ( topGen ` { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } ) )
35	30, 34	sseqtr4d 3390	. . . . . . . . 9 |- ( ( A e. V /\ F : A --> Top ) -> { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } C_ J )
36	35	adantr 462	. . . . . . . 8 |- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ u e. ( F ` I ) ) ) -> { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } C_ J )
37		eqid 2441	. . . . . . . . 9 |- X_ k e. A U. ( F ` k ) = X_ k e. A U. ( F ` k )
38	27, 37	ptpjpre2 19112	. . . . . . . 8 |- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ u e. ( F ` I ) ) ) -> ( `' ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) " u ) e. { w | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) } )
39	36, 38	sseldd 3354	. . . . . . 7 |- ( ( ( A e. V /\ F : A --> Top ) /\ ( I e. A /\ u e. ( F ` I ) ) ) -> ( `' ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) " u ) e. J )
40	39	expr 612	. . . . . 6 |- ( ( ( A e. V /\ F : A --> Top ) /\ I e. A ) -> ( u e. ( F ` I ) -> ( `' ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) " u ) e. J ) )
41	40	ralrimiv 2796	. . . . 5 |- ( ( ( A e. V /\ F : A --> Top ) /\ I e. A ) -> A. u e. ( F ` I ) ( `' ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) " u ) e. J )
42	41	3impa 1177	. . . 4 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> A. u e. ( F ` I ) ( `' ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) " u ) e. J )
43	26, 42	jca 529	. . 3 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) : Y --> U. ( F ` I ) /\ A. u e. ( F ` I ) ( `' ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) " u ) e. J ) )
44		eqid 2441	. . . 4 |- U. ( F ` I ) = U. ( F ` I )
45	4, 44	iscn2 18801	. . 3 |- ( ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) e. ( J Cn ( F ` I ) ) <-> ( ( J e. Top /\ ( F ` I ) e. Top ) /\ ( ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) : Y --> U. ( F ` I ) /\ A. u e. ( F ` I ) ( `' ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) " u ) e. J ) ) )
46	12, 43, 45	sylanbrc 659	. 2 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) e. ( J Cn ( F ` I ) ) )
47	6, 46	eqeltrd 2515	1 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( x e. Y |-> ( x ` I ) ) e. ( J Cn ( F ` I ) ) )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 960   = wceq 1364   E.wex 1591   e. wcel 1761   {cab 2427   A.wral 2713   E.wrex 2714   \ cdif 3322   C_ wss 3325   U.cuni 4088   e. cmpt 4347   `'ccnv 4835   "cima 4839   Fn wfn 5410   -->wf 5411   ` cfv 5415  (class class class)co 6090   X_cixp 7259   Fincfn 7306   topGenctg 14372   Xt_cpt 14373   Topctop 18457   TopBasesctb 18461   Cn ccn 18787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-recs 6828  df-rdg 6862  df-1o 6916  df-oadd 6920  df-er 7097  df-map 7212  df-ixp 7260  df-en 7307  df-fin 7310  df-fi 7657  df-topgen 14378  df-pt 14379  df-top 18462  df-bases 18464  df-topon 18465  df-cn 18790

This theorem is referenced by:  pthaus  19170  ptrescn  19171  xkopjcn  19188  pt1hmeo  19338  ptunhmeo  19340  tmdgsum  19625  symgtgp  19631  prdstmdd  19653  prdstgpd  19654