mapcod

Step	Hyp	Ref	Expression
1		mapcod.1	$⊢ φ \to F \in (A^{B})$
2		mapcod.2	$⊢ φ \to G \in (B^{C})$
3		elmapex	$⊢ F \in (A^{B}) \to (A \in V \land B \in V)$
4	1 3	syl	$⊢ φ \to (A \in V \land B \in V)$
5	4	simpld	$⊢ φ \to A \in V$
6		elmapex	$⊢ G \in (B^{C}) \to (B \in V \land C \in V)$
7	2 6	syl	$⊢ φ \to (B \in V \land C \in V)$
8	7	simprd	$⊢ φ \to C \in V$
9		elmapi	$⊢ F \in (A^{B}) \to F : B ⟶ A$
10	1 9	syl	$⊢ φ \to F : B ⟶ A$
11		elmapi	$⊢ G \in (B^{C}) \to G : C ⟶ B$
12	2 11	syl	$⊢ φ \to G : C ⟶ B$
13	10 12	fcod	$⊢ φ \to (F \circ G) : C ⟶ A$
14	5 8 13	elmapdd	$⊢ φ \to F \circ G \in (A^{C})$

Metamath Proof Explorer