Metamath Proof Explorer

Theorem ptpjcn

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

Ref Expression
Hypotheses ptpjcn.1 
|- Y = U. J
ptpjcn.2 
|- J = ( Xt_ ` F )
Assertion ptpjcn 
|- ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( x e. Y |-> ( x ` I ) ) e. ( J Cn ( F ` I ) ) )

Proof

Step Hyp Ref Expression
1 ptpjcn.1 
 |-  Y = U. J
2 ptpjcn.2 
 |-  J = ( Xt_ ` F )
3 2 ptuni 
 |-  ( ( A e. V /\ F : A --> Top ) -> X_ k e. A U. ( F ` k ) = U. J )
4 3 3adant3 
 |-  ( ( A e. V /\ F : A --> Top /\ I e. A ) -> X_ k e. A U. ( F ` k ) = U. J )
5 1 4 eqtr4id 
 |-  ( ( A e. V /\ F : A --> Top /\ I e. A ) -> Y = X_ k e. A U. ( F ` k ) )
6 5 mpteq1d 
 |-  ( ( 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 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) e. Top )
8 7 3adant3 
 |-  ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( Xt_ ` F ) e. Top )
9 2 8 eqeltrid 
 |-  ( ( A e. V /\ F : A --> Top /\ I e. A ) -> J e. Top )
10 ffvelcdm 
 |-  ( ( F : A --> Top /\ I e. A ) -> ( F ` I ) e. Top )
11 10 3adant1 
 |-  ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( F ` I ) e. Top )
12 vex 
 |-  x e. _V
13 12 elixp 
 |-  ( x e. X_ k e. A U. ( F ` k ) <-> ( x Fn A /\ A. k e. A ( x ` k ) e. U. ( F ` k ) ) )
14 13 simprbi 
 |-  ( x e. X_ k e. A U. ( F ` k ) -> A. k e. A ( x ` k ) e. U. ( F ` k ) )
15 fveq2 
 |-  ( k = I -> ( x ` k ) = ( x ` I ) )
16 fveq2 
 |-  ( k = I -> ( F ` k ) = ( F ` I ) )
17 16 unieqd 
 |-  ( k = I -> U. ( F ` k ) = U. ( F ` I ) )
18 15 17 eleq12d 
 |-  ( k = I -> ( ( x ` k ) e. U. ( F ` k ) <-> ( x ` I ) e. U. ( F ` I ) ) )
19 18 rspcva 
 |-  ( ( I e. A /\ A. k e. A ( x ` k ) e. U. ( F ` k ) ) -> ( x ` I ) e. U. ( F ` I ) )
20 14 19 sylan2 
 |-  ( ( I e. A /\ x e. X_ k e. A U. ( F ` k ) ) -> ( x ` I ) e. U. ( F ` I ) )
21 20 3ad2antl3 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ x e. X_ k e. A U. ( F ` k ) ) -> ( x ` I ) e. U. ( F ` I ) )
22 21 fmpttd 
 |-  ( ( 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 ) )
23 5 feq2d 
 |-  ( ( 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 ) ) )
24 22 23 mpbird 
 |-  ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( x e. X_ k e. A U. ( F ` k ) |-> ( x ` I ) ) : Y --> U. ( F ` I ) )
25 eqid 
 |-  { 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 ) ) }
26 25 ptbas 
 |-  ( ( 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 )
27 bastg 
 |-  ( { 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 ) ) } ) )
28 26 27 syl 
 |-  ( ( 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 ) ) } ) )
29 ffn 
 |-  ( F : A --> Top -> F Fn A )
30 25 ptval 
 |-  ( ( 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 ) ) } ) )
31 2 30 eqtrid 
 |-  ( ( 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 ) ) } ) )
32 29 31 sylan2 
 |-  ( ( 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 ) ) } ) )
33 28 32 sseqtrrd 
 |-  ( ( 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 )
34 33 adantr 
 |-  ( ( ( 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 )
35 eqid 
 |-  X_ k e. A U. ( F ` k ) = X_ k e. A U. ( F ` k )
36 25 35 ptpjpre2 
 |-  ( ( ( 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 ) ) } )
37 34 36 sseldd 
 |-  ( ( ( 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 )
38 37 expr 
 |-  ( ( ( 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 ) )
39 38 ralrimiv 
 |-  ( ( ( 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 )
40 39 3impa 
 |-  ( ( 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 )
41 24 40 jca 
 |-  ( ( 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 ) )
42 eqid 
 |-  U. ( F ` I ) = U. ( F ` I )
43 1 42 iscn2 
 |-  ( ( 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 ) ) )
44 9 11 41 43 syl21anbrc 
 |-  ( ( 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 ) ) )
45 6 44 eqeltrd 
 |-  ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( x e. Y |-> ( x ` I ) ) e. ( J Cn ( F ` I ) ) )