Metamath Proof Explorer


Theorem curry2ima

Description: The image of a curried function with a constant second argument. (Contributed by Thierry Arnoux, 25-Sep-2017)

Ref Expression
Hypothesis curry2ima.1 𝐺 = ( 𝐹 ( 1st ↾ ( V × { 𝐶 } ) ) )
Assertion curry2ima ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → ( 𝐺𝐷 ) = { 𝑦 ∣ ∃ 𝑥𝐷 𝑦 = ( 𝑥 𝐹 𝐶 ) } )

Proof

Step Hyp Ref Expression
1 curry2ima.1 𝐺 = ( 𝐹 ( 1st ↾ ( V × { 𝐶 } ) ) )
2 simp1 ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → 𝐹 Fn ( 𝐴 × 𝐵 ) )
3 dffn2 ( 𝐹 Fn ( 𝐴 × 𝐵 ) ↔ 𝐹 : ( 𝐴 × 𝐵 ) ⟶ V )
4 2 3 sylib ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → 𝐹 : ( 𝐴 × 𝐵 ) ⟶ V )
5 simp2 ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → 𝐶𝐵 )
6 1 curry2f ( ( 𝐹 : ( 𝐴 × 𝐵 ) ⟶ V ∧ 𝐶𝐵 ) → 𝐺 : 𝐴 ⟶ V )
7 4 5 6 syl2anc ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → 𝐺 : 𝐴 ⟶ V )
8 7 ffund ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → Fun 𝐺 )
9 simp3 ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → 𝐷𝐴 )
10 7 fdmd ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → dom 𝐺 = 𝐴 )
11 9 10 sseqtrrd ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → 𝐷 ⊆ dom 𝐺 )
12 dfimafn ( ( Fun 𝐺𝐷 ⊆ dom 𝐺 ) → ( 𝐺𝐷 ) = { 𝑦 ∣ ∃ 𝑥𝐷 ( 𝐺𝑥 ) = 𝑦 } )
13 8 11 12 syl2anc ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → ( 𝐺𝐷 ) = { 𝑦 ∣ ∃ 𝑥𝐷 ( 𝐺𝑥 ) = 𝑦 } )
14 1 curry2val ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵 ) → ( 𝐺𝑥 ) = ( 𝑥 𝐹 𝐶 ) )
15 14 3adant3 ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → ( 𝐺𝑥 ) = ( 𝑥 𝐹 𝐶 ) )
16 15 eqeq1d ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → ( ( 𝐺𝑥 ) = 𝑦 ↔ ( 𝑥 𝐹 𝐶 ) = 𝑦 ) )
17 eqcom ( ( 𝑥 𝐹 𝐶 ) = 𝑦𝑦 = ( 𝑥 𝐹 𝐶 ) )
18 16 17 bitrdi ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → ( ( 𝐺𝑥 ) = 𝑦𝑦 = ( 𝑥 𝐹 𝐶 ) ) )
19 18 rexbidv ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → ( ∃ 𝑥𝐷 ( 𝐺𝑥 ) = 𝑦 ↔ ∃ 𝑥𝐷 𝑦 = ( 𝑥 𝐹 𝐶 ) ) )
20 19 abbidv ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → { 𝑦 ∣ ∃ 𝑥𝐷 ( 𝐺𝑥 ) = 𝑦 } = { 𝑦 ∣ ∃ 𝑥𝐷 𝑦 = ( 𝑥 𝐹 𝐶 ) } )
21 13 20 eqtrd ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶𝐵𝐷𝐴 ) → ( 𝐺𝐷 ) = { 𝑦 ∣ ∃ 𝑥𝐷 𝑦 = ( 𝑥 𝐹 𝐶 ) } )