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 ffvelrn
 |-  ( ( 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 ) ) )