This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm ⊢ ( ( 𝐹 : 𝐴 ⟶ 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 eqtrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐹 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 ( 𝐹 ‘ 𝐼 ) ) )