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 𝑌 = 𝐽
ptpjcn.2 𝐽 = ( ∏t𝐹 )
Assertion ptpjcn ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( 𝑥𝑌 ↦ ( 𝑥𝐼 ) ) ∈ ( 𝐽 Cn ( 𝐹𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 ptpjcn.1 𝑌 = 𝐽
2 ptpjcn.2 𝐽 = ( ∏t𝐹 )
3 2 ptuni ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → X 𝑘𝐴 ( 𝐹𝑘 ) = 𝐽 )
4 3 3adant3 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → X 𝑘𝐴 ( 𝐹𝑘 ) = 𝐽 )
5 1 4 eqtr4id ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → 𝑌 = X 𝑘𝐴 ( 𝐹𝑘 ) )
6 5 mpteq1d ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( 𝑥𝑌 ↦ ( 𝑥𝐼 ) ) = ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) )
7 pttop ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( ∏t𝐹 ) ∈ Top )
8 7 3adant3 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( ∏t𝐹 ) ∈ Top )
9 2 8 eqeltrid ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → 𝐽 ∈ Top )
10 ffvelrn ( ( 𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( 𝐹𝐼 ) ∈ Top )
11 10 3adant1 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( 𝐹𝐼 ) ∈ Top )
12 vex 𝑥 ∈ V
13 12 elixp ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↔ ( 𝑥 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑥𝑘 ) ∈ ( 𝐹𝑘 ) ) )
14 13 simprbi ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) → ∀ 𝑘𝐴 ( 𝑥𝑘 ) ∈ ( 𝐹𝑘 ) )
15 fveq2 ( 𝑘 = 𝐼 → ( 𝑥𝑘 ) = ( 𝑥𝐼 ) )
16 fveq2 ( 𝑘 = 𝐼 → ( 𝐹𝑘 ) = ( 𝐹𝐼 ) )
17 16 unieqd ( 𝑘 = 𝐼 ( 𝐹𝑘 ) = ( 𝐹𝐼 ) )
18 15 17 eleq12d ( 𝑘 = 𝐼 → ( ( 𝑥𝑘 ) ∈ ( 𝐹𝑘 ) ↔ ( 𝑥𝐼 ) ∈ ( 𝐹𝐼 ) ) )
19 18 rspcva ( ( 𝐼𝐴 ∧ ∀ 𝑘𝐴 ( 𝑥𝑘 ) ∈ ( 𝐹𝑘 ) ) → ( 𝑥𝐼 ) ∈ ( 𝐹𝐼 ) )
20 14 19 sylan2 ( ( 𝐼𝐴𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ) → ( 𝑥𝐼 ) ∈ ( 𝐹𝐼 ) )
21 20 3ad2antl3 ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) ∧ 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ) → ( 𝑥𝐼 ) ∈ ( 𝐹𝐼 ) )
22 21 fmpttd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) : X 𝑘𝐴 ( 𝐹𝑘 ) ⟶ ( 𝐹𝐼 ) )
23 5 feq2d ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) : 𝑌 ( 𝐹𝐼 ) ↔ ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) : X 𝑘𝐴 ( 𝐹𝑘 ) ⟶ ( 𝐹𝐼 ) ) )
24 22 23 mpbird ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) : 𝑌 ( 𝐹𝐼 ) )
25 eqid { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } = { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) }
26 25 ptbas ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ∈ TopBases )
27 bastg ( { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ∈ TopBases → { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ⊆ ( topGen ‘ { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
28 26 27 syl ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ⊆ ( topGen ‘ { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
29 ffn ( 𝐹 : 𝐴 ⟶ Top → 𝐹 Fn 𝐴 )
30 25 ptval ( ( 𝐴𝑉𝐹 Fn 𝐴 ) → ( ∏t𝐹 ) = ( topGen ‘ { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
31 2 30 syl5eq ( ( 𝐴𝑉𝐹 Fn 𝐴 ) → 𝐽 = ( topGen ‘ { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
32 29 31 sylan2 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → 𝐽 = ( topGen ‘ { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ) )
33 28 32 sseqtrrd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ⊆ 𝐽 )
34 33 adantr ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼𝐴𝑢 ∈ ( 𝐹𝐼 ) ) ) → { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } ⊆ 𝐽 )
35 eqid X 𝑘𝐴 ( 𝐹𝑘 ) = X 𝑘𝐴 ( 𝐹𝑘 )
36 25 35 ptpjpre2 ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼𝐴𝑢 ∈ ( 𝐹𝐼 ) ) ) → ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) “ 𝑢 ) ∈ { 𝑤 ∣ ∃ 𝑔 ( ( 𝑔 Fn 𝐴 ∧ ∀ 𝑦𝐴 ( 𝑔𝑦 ) ∈ ( 𝐹𝑦 ) ∧ ∃ 𝑧 ∈ Fin ∀ 𝑦 ∈ ( 𝐴𝑧 ) ( 𝑔𝑦 ) = ( 𝐹𝑦 ) ) ∧ 𝑤 = X 𝑦𝐴 ( 𝑔𝑦 ) ) } )
37 34 36 sseldd ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ ( 𝐼𝐴𝑢 ∈ ( 𝐹𝐼 ) ) ) → ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) “ 𝑢 ) ∈ 𝐽 )
38 37 expr ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ 𝐼𝐴 ) → ( 𝑢 ∈ ( 𝐹𝐼 ) → ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) “ 𝑢 ) ∈ 𝐽 ) )
39 38 ralrimiv ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) ∧ 𝐼𝐴 ) → ∀ 𝑢 ∈ ( 𝐹𝐼 ) ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) “ 𝑢 ) ∈ 𝐽 )
40 39 3impa ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ∀ 𝑢 ∈ ( 𝐹𝐼 ) ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) “ 𝑢 ) ∈ 𝐽 )
41 24 40 jca ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) : 𝑌 ( 𝐹𝐼 ) ∧ ∀ 𝑢 ∈ ( 𝐹𝐼 ) ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) “ 𝑢 ) ∈ 𝐽 ) )
42 eqid ( 𝐹𝐼 ) = ( 𝐹𝐼 )
43 1 42 iscn2 ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) ∈ ( 𝐽 Cn ( 𝐹𝐼 ) ) ↔ ( ( 𝐽 ∈ Top ∧ ( 𝐹𝐼 ) ∈ Top ) ∧ ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) : 𝑌 ( 𝐹𝐼 ) ∧ ∀ 𝑢 ∈ ( 𝐹𝐼 ) ( ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) “ 𝑢 ) ∈ 𝐽 ) ) )
44 9 11 41 43 syl21anbrc ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑥𝐼 ) ) ∈ ( 𝐽 Cn ( 𝐹𝐼 ) ) )
45 6 44 eqeltrd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐼𝐴 ) → ( 𝑥𝑌 ↦ ( 𝑥𝐼 ) ) ∈ ( 𝐽 Cn ( 𝐹𝐼 ) ) )