Metamath Proof Explorer

Theorem oprabco

Description: Composition of a function with an operator abstraction. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 26-Sep-2015)

		Ref	Expression
	Hypotheses	oprabco.1	$⊢ (x \in A \land y \in B) \to C \in D$
		oprabco.2	$⊢ F = (x \in A, y \in B ⟼ C)$
		oprabco.3	$⊢ G = (x \in A, y \in B ⟼ H (C))$
	Assertion	oprabco	$⊢ H Fn D \to G = H \circ F$

Proof

Step	Hyp	Ref	Expression
1		oprabco.1	$⊢ (x \in A \land y \in B) \to C \in D$
2		oprabco.2	$⊢ F = (x \in A, y \in B ⟼ C)$
3		oprabco.3	$⊢ G = (x \in A, y \in B ⟼ H (C))$
4	1	adantl	$⊢ (H Fn D \land (x \in A \land y \in B)) \to C \in D$
5	2	a1i	$⊢ H Fn D \to F = (x \in A, y \in B ⟼ C)$
6		dffn5	$⊢ H Fn D \leftrightarrow H = (z \in D ⟼ H (z))$
7	6	biimpi	$⊢ H Fn D \to H = (z \in D ⟼ H (z))$
8		fveq2	$⊢ z = C \to H (z) = H (C)$
9	4 5 7 8	fmpoco	$⊢ H Fn D \to H \circ F = (x \in A, y \in B ⟼ H (C))$
10	3 9	eqtr4id	$⊢ H Fn D \to G = H \circ F$