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 ⊢ G = F ∘ 1 st ↾ V × C -1
Assertion curry2ima ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → G D = y | ∃ x ∈ D y = x F C

Proof

Step Hyp Ref Expression
1 curry2ima.1 ⊢ G = F ∘ 1 st ↾ V × C -1
2 simp1 ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → F Fn A × B
3 dffn2 ⊢ F Fn A × B ↔ F : A × B ⟶ V
4 2 3 sylib ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → F : A × B ⟶ V
5 simp2 ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → C ∈ B
6 1 curry2f ⊢ F : A × B ⟶ V ∧ C ∈ B → G : A ⟶ V
7 4 5 6 syl2anc ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → G : A ⟶ V
8 7 ffund ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → Fun ⁡ G
9 simp3 ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → D ⊆ A
10 7 fdmd ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → dom ⁡ G = A
11 9 10 sseqtrrd ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → D ⊆ dom ⁡ G
12 dfimafn ⊢ Fun ⁡ G ∧ D ⊆ dom ⁡ G → G D = y | ∃ x ∈ D G ⁡ x = y
13 8 11 12 syl2anc ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → G D = y | ∃ x ∈ D G ⁡ x = y
14 1 curry2val ⊢ F Fn A × B ∧ C ∈ B → G ⁡ x = x F C
15 14 3adant3 ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → G ⁡ x = x F C
16 15 eqeq1d ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → G ⁡ x = y ↔ x F C = y
17 eqcom ⊢ x F C = y ↔ y = x F C
18 16 17 bitrdi ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → G ⁡ x = y ↔ y = x F C
19 18 rexbidv ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → ∃ x ∈ D G ⁡ x = y ↔ ∃ x ∈ D y = x F C
20 19 abbidv ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → y | ∃ x ∈ D G ⁡ x = y = y | ∃ x ∈ D y = x F C
21 13 20 eqtrd ⊢ F Fn A × B ∧ C ∈ B ∧ D ⊆ A → G D = y | ∃ x ∈ D y = x F C