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

Metamath Proof Explorer

Theorem fcompt

Description: Express composition of two functions as a maps-to applying both in sequence. (Contributed by Stefan O'Rear, 5-Oct-2014) (Proof shortened by Mario Carneiro, 27-Dec-2014)

		Ref	Expression
	Assertion	fcompt	$⊢ (A : D ⟶ E \land B : C ⟶ D) \to A \circ B = (x \in C ⟼ A (B (x)))$

Proof

Step	Hyp	Ref	Expression
1		ffvelcdm	$⊢ (B : C ⟶ D \land x \in C) \to B (x) \in D$
2	1	adantll	$⊢ ((A : D ⟶ E \land B : C ⟶ D) \land x \in C) \to B (x) \in D$
3		ffn	$⊢ B : C ⟶ D \to B Fn C$
4	3	adantl	$⊢ (A : D ⟶ E \land B : C ⟶ D) \to B Fn C$
5		dffn5	$⊢ B Fn C \leftrightarrow B = (x \in C ⟼ B (x))$
6	4 5	sylib	$⊢ (A : D ⟶ E \land B : C ⟶ D) \to B = (x \in C ⟼ B (x))$
7		ffn	$⊢ A : D ⟶ E \to A Fn D$
8	7	adantr	$⊢ (A : D ⟶ E \land B : C ⟶ D) \to A Fn D$
9		dffn5	$⊢ A Fn D \leftrightarrow A = (y \in D ⟼ A (y))$
10	8 9	sylib	$⊢ (A : D ⟶ E \land B : C ⟶ D) \to A = (y \in D ⟼ A (y))$
11		fveq2	$⊢ y = B (x) \to A (y) = A (B (x))$
12	2 6 10 11	fmptco	$⊢ (A : D ⟶ E \land B : C ⟶ D) \to A \circ B = (x \in C ⟼ A (B (x)))$