Theorem ptpjcn 20703

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 20686	. . . . 5 |- ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. J )
3	2	3adant3 1050	. . . 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 2524	. . 3 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> Y = X_ k e. A U. ( F ` k ) )
6	5	mpteq1d 4477	. 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 20674	. . . . . 6 |- ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) e. Top )
8	7	3adant3 1050	. . . . 5 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( Xt_ ` F ) e. Top )
9	1, 8	syl5eqel 2553	. . . 4 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> J e. Top )
10		ffvelrn 6035	. . . . 5 |- ( ( F : A --> Top /\ I e. A ) -> ( F ` I ) e. Top )
11	10	3adant1 1048	. . . 4 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( F ` I ) e. Top )
12	9, 11	jca 541	. . 3 |- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( J e. Top /\ ( F ` I ) e. Top ) )
13		vex 3034	. . . . . . . . . 10 |- x e. _V
14	13	elixp 7547	. . . . . . . . 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 471	. . . . . . . 8 |- ( x e. X_ k e. A U. ( F ` k ) -> A. k e. A ( x ` k ) e. U. ( F ` k ) )
16		fveq2 5879	. . . . . . . . . 10 |- ( k = I -> ( x ` k ) = ( x ` I ) )
17		fveq2 5879	. . . . . . . . . . 11 |- ( k = I -> ( F ` k ) = ( F ` I ) )
18	17	unieqd 4200	. . . . . . . . . 10 |- ( k = I -> U. ( F ` k ) = U. ( F ` I ) )
19	16, 18	eleq12d 2543	. . . . . . . . 9 |- ( k = I -> ( ( x ` k ) e. U. ( F ` k ) <-> ( x ` I ) e. U. ( F ` I ) ) )
20	19	rspcva 3134	. . . . . . . 8 |- ( ( I e. A /\ A. k e. A ( x ` k ) e. U. ( F ` k ) ) -> ( x ` I ) e. U. ( F ` I ) )
21	15, 20	sylan2 482	. . . . . . 7 |- ( ( I e. A /\ x e. X_ k e. A U. ( F ` k ) ) -> ( x ` I ) e. U. ( F ` I ) )
22	21	3ad2antl3 1194	. . . . . 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 2471	. . . . . 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 6061	. . . . 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 5725	. . . . 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 240	. . . 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 2471	. . . . . . . . . . . 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 20671	. . . . . . . . . . 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 20058	. . . . . . . . . . 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 17	. . . . . . . . . 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 5739	. . . . . . . . . . 11 |- ( F : A --> Top -> F Fn A )
32	27	ptval 20662	. . . . . . . . . . . 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 2517	. . . . . . . . . . 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 482	. . . . . . . . . 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 3455	. . . . . . . . 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 472	. . . . . . . 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 2471	. . . . . . . . 9 |- X_ k e. A U. ( F ` k ) = X_ k e. A U. ( F ` k )
38	27, 37	ptpjpre2 20672	. . . . . . . 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 3419	. . . . . . 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 626	. . . . . 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 2808	. . . . 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 1226	. . . 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 541	. . 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 2471	. . . 4 |- U. ( F ` I ) = U. ( F ` I )
45	4, 44	iscn2 20331	. . 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 677	. 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 2549	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 376   /\ w3a 1007   = wceq 1452   E.wex 1671   e. wcel 1904   {cab 2457   A.wral 2756   E.wrex 2757   \ cdif 3387   C_ wss 3390   U.cuni 4190   |-> cmpt 4454   `'ccnv 4838   "cima 4842   Fn wfn 5584   -->wf 5585   ` cfv 5589  (class class class)co 6308   X_cixp 7540   Fincfn 7587   topGenctg 15414   Xt_cpt 15415   Topctop 19994   TopBasesctb 19997   Cn ccn 20317

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-reu 2763  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-ixp 7541  df-en 7588  df-fin 7591  df-fi 7943  df-topgen 15420  df-pt 15421  df-top 19998  df-bases 19999  df-topon 20000  df-cn 20320

This theorem is referenced by:  pthaus  20730  ptrescn  20731  xkopjcn  20748  pt1hmeo  20898  ptunhmeo  20900  tmdgsum  21188  symgtgp  21194  prdstmdd  21216  prdstgpd  21217  poimir  32037  broucube  32038