Theorem fvco4i

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

	Ref	Expression
Hypotheses	fvco4i.a	$$⊢\varnothing =F\left(\varnothing \right)$$
	fvco4i.b	$$⊢\mathrm{Fun}G$$
Assertion	fvco4i	$$⊢\left(F\circ G\right)\left(X\right)=F\left(G\left(X\right)\right)$$

Proof

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