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	⊢ 𝐺 = ( 𝐹 ∘ ^◡ ( 1^st ↾ ( V × { 𝐶 } ) ) )
	Assertion	curry2ima	⊢ ( ( 𝐹 Fn ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ⊆ 𝐴 ) → ( 𝐺 “ 𝐷 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐷 𝑦 = ( 𝑥 𝐹 𝐶 ) } )

Proof

Step	Hyp	Ref	Expression
1		curry2ima.1	⊢ 𝐺 = ( 𝐹 ∘ ^◡ ( 1^st ↾ ( 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 ( 𝐴 × 𝐵 ) ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ⊆ 𝐴 ) → ( 𝐺 “ 𝐷 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐷 𝑦 = ( 𝑥 𝐹 𝐶 ) } )

Metamath Proof Explorer

Theorem curry2ima

Proof