This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fmptcos

Description: Composition of two functions expressed as mapping abstractions. (Contributed by NM, 22-May-2006) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Hypotheses	fmptcof.1	$⊢ φ \to \forall x \in A R \in B$
		fmptcof.2	$⊢ φ \to F = (x \in A ⟼ R)$
		fmptcof.3	$⊢ φ \to G = (y \in B ⟼ S)$
	Assertion	fmptcos	$⊢ φ \to G \circ F = (x \in A ⟼ ⦋ R / y ⦌ S)$

Proof

Step	Hyp	Ref	Expression
1		fmptcof.1	$⊢ φ \to \forall x \in A R \in B$
2		fmptcof.2	$⊢ φ \to F = (x \in A ⟼ R)$
3		fmptcof.3	$⊢ φ \to G = (y \in B ⟼ S)$
4		nfcv	$⊢ \underline{Ⅎ} z S$
5		nfcsb1v	$⊢ \underline{Ⅎ} y ⦋ z / y ⦌ S$
6		csbeq1a	$⊢ y = z \to S = ⦋ z / y ⦌ S$
7	4 5 6	cbvmpt	$⊢ (y \in B ⟼ S) = (z \in B ⟼ ⦋ z / y ⦌ S)$
8	3 7	eqtrdi	$⊢ φ \to G = (z \in B ⟼ ⦋ z / y ⦌ S)$
9		csbeq1	$⊢ z = R \to ⦋ z / y ⦌ S = ⦋ R / y ⦌ S$
10	1 2 8 9	fmptcof	$⊢ φ \to G \circ F = (x \in A ⟼ ⦋ R / y ⦌ S)$