Theorem ptpjcn 19842

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 19825	. . . . 5 |- ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. J )
3	2	3adant3 1011	. . . 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 2522	. . 3 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> Y = X_ k e. A U. ( F ` k ) )
6	5	mpteq1d 4523	. 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 19813	. . . . . 6 |- ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) e. Top )
8	7	3adant3 1011	. . . . 5 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( Xt_ ` F ) e. Top )
9	1, 8	syl5eqel 2554	. . . 4 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> J e. Top )
10		ffvelrn 6012	. . . . 5 |- ( ( F : A --> Top /\ I e. A ) -> ( F ` I ) e. Top )
11	10	3adant1 1009	. . . 4 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( F ` I ) e. Top )
12	9, 11	jca 532	. . 3 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( J e. Top /\ ( F ` I ) e. Top ) )
13		vex 3111	. . . . . . . . . 10 |- x e. _V
14	13	elixp 7468	. . . . . . . . 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 464	. . . . . . . 8 |- ( x e. X_ k e. A U. ( F ` k ) -> A. k e. A ( x ` k ) e. U. ( F ` k ) )
16		fveq2 5859	. . . . . . . . . 10 |- ( k = I -> ( x ` k ) = ( x ` I ) )
17		fveq2 5859	. . . . . . . . . . 11 |- ( k = I -> ( F ` k ) = ( F ` I ) )
18	17	unieqd 4250	. . . . . . . . . 10 |- ( k = I -> U. ( F ` k ) = U. ( F ` I ) )
19	16, 18	eleq12d 2544	. . . . . . . . 9 |- ( k = I -> ( ( x ` k ) e. U. ( F ` k ) <-> ( x ` I ) e. U. ( F ` I ) ) )
20	19	rspcva 3207	. . . . . . . 8 |- ( ( I e. A /\ A. k e. A ( x ` k ) e. U. ( F ` k ) ) -> ( x ` I ) e. U. ( F ` I ) )
21	15, 20	sylan2 474	. . . . . . 7 |- ( ( I e. A /\ x e. X_ k e. A U. ( F ` k ) ) -> ( x ` I ) e. U. ( F ` I ) )
22	21	3ad2antl3 1155	. . . . . 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 2462	. . . . . 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 6038	. . . . 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 5711	. . . . 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 2462	. . . . . . . . . . . 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 19810	. . . . . . . . . . 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 19229	. . . . . . . . . . 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 5724	. . . . . . . . . . 11 |- ( F : A --> Top -> F Fn A )
32	27	ptval 19801	. . . . . . . . . . . 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 2515	. . . . . . . . . . 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 474	. . . . . . . . . 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 3536	. . . . . . . . 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 465	. . . . . . . 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 2462	. . . . . . . . 9 |- X_ k e. A U. ( F ` k ) = X_ k e. A U. ( F ` k )
38	27, 37	ptpjpre2 19811	. . . . . . . 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 3500	. . . . . . 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 615	. . . . . 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 2871	. . . . 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 1186	. . . 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 532	. . 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 2462	. . . 4 |- U. ( F ` I ) = U. ( F ` I )
45	4, 44	iscn2 19500	. . 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 664	. 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 2550	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 968   = wceq 1374   E.wex 1591   e. wcel 1762   {cab 2447   A.wral 2809   E.wrex 2810   \ cdif 3468   C_ wss 3471   U.cuni 4240   |-> cmpt 4500   `'ccnv 4993   "cima 4997   Fn wfn 5576   -->wf 5577   ` cfv 5581  (class class class)co 6277   X_cixp 7461   Fincfn 7508   topGenctg 14684   Xt_cpt 14685   Topctop 19156   TopBasesctb 19160   Cn ccn 19486

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 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-rep 4553  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681  ax-un 6569

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-ral 2814  df-rex 2815  df-reu 2816  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-tp 4027  df-op 4029  df-uni 4241  df-int 4278  df-iun 4322  df-br 4443  df-opab 4501  df-mpt 4502  df-tr 4536  df-eprel 4786  df-id 4790  df-po 4795  df-so 4796  df-fr 4833  df-we 4835  df-ord 4876  df-on 4877  df-lim 4878  df-suc 4879  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-iota 5544  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6674  df-recs 7034  df-rdg 7068  df-1o 7122  df-oadd 7126  df-er 7303  df-map 7414  df-ixp 7462  df-en 7509  df-fin 7512  df-fi 7862  df-topgen 14690  df-pt 14691  df-top 19161  df-bases 19163  df-topon 19164  df-cn 19489

This theorem is referenced by:  pthaus  19869  ptrescn  19870  xkopjcn  19887  pt1hmeo  20037  ptunhmeo  20039  tmdgsum  20324  symgtgp  20330  prdstmdd  20352  prdstgpd  20353