fvco4i

Description: Conditions for a composition to be expandable without conditions on the argument. (Contributed by Stefan O'Rear, 31-Mar-2015)

Step	Hyp	Ref	Expression
1		fvco4i.a	$⊢ \emptyset = F (\emptyset)$
2		fvco4i.b	$⊢ Fun G$
3		funfn	$⊢ Fun G \leftrightarrow G Fn dom G$
4	2 3	mpbi	$⊢ G Fn dom G$
5		fvco2	$⊢ (G Fn dom G \land X \in dom G) \to (F \circ G) (X) = F (G (X))$
6	4 5	mpan	$⊢ X \in dom G \to (F \circ G) (X) = F (G (X))$
7		dmcoss	$⊢ dom (F \circ G) \subseteq dom G$
8	7	sseli	$⊢ X \in dom (F \circ G) \to X \in dom G$
9		ndmfv	$⊢ \neg X \in dom (F \circ G) \to (F \circ G) (X) = \emptyset$
10	8 9	nsyl5	$⊢ \neg X \in dom G \to (F \circ G) (X) = \emptyset$
11		ndmfv	$⊢ \neg X \in dom G \to G (X) = \emptyset$
12	11	fveq2d	$⊢ \neg X \in dom G \to F (G (X)) = F (\emptyset)$
13	1 10 12	3eqtr4a	$⊢ \neg X \in dom G \to (F \circ G) (X) = F (G (X))$
14	6 13	pm2.61i	$⊢ (F \circ G) (X) = F (G (X))$

Metamath Proof Explorer