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 \circ {({1^{st} ↾}_{(V \times \{C\})})}^{-1}$
	Assertion	curry2ima	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to G [D] = \{y \| \exists x \in D y = x F C\}$

Proof

Step	Hyp	Ref	Expression
1		curry2ima.1	$⊢ G = F \circ {({1^{st} ↾}_{(V \times \{C\})})}^{-1}$
2		simp1	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to F Fn (A \times B)$
3		dffn2	$⊢ F Fn (A \times B) \leftrightarrow F : A \times B ⟶ V$
4	2 3	sylib	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to F : A \times B ⟶ V$
5		simp2	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to C \in B$
6	1	curry2f	$⊢ (F : A \times B ⟶ V \land C \in B) \to G : A ⟶ V$
7	4 5 6	syl2anc	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to G : A ⟶ V$
8	7	ffund	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to Fun G$
9		simp3	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to D \subseteq A$
10	7	fdmd	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to dom G = A$
11	9 10	sseqtrrd	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to D \subseteq dom G$
12		dfimafn	$⊢ (Fun G \land D \subseteq dom G) \to G [D] = \{y \| \exists x \in D G (x) = y\}$
13	8 11 12	syl2anc	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to G [D] = \{y \| \exists x \in D G (x) = y\}$
14	1	curry2val	$⊢ (F Fn (A \times B) \land C \in B) \to G (x) = x F C$
15	14	3adant3	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to G (x) = x F C$
16	15	eqeq1d	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to (G (x) = y \leftrightarrow x F C = y)$
17		eqcom	$⊢ x F C = y \leftrightarrow y = x F C$
18	16 17	bitrdi	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to (G (x) = y \leftrightarrow y = x F C)$
19	18	rexbidv	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to (\exists x \in D G (x) = y \leftrightarrow \exists x \in D y = x F C)$
20	19	abbidv	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to \{y \| \exists x \in D G (x) = y\} = \{y \| \exists x \in D y = x F C\}$
21	13 20	eqtrd	$⊢ (F Fn (A \times B) \land C \in B \land D \subseteq A) \to G [D] = \{y \| \exists x \in D y = x F C\}$

Metamath Proof Explorer

Theorem curry2ima

Proof