Theorem afv2co2

Description: Value of a function composition, analogous to fvco2 . (Contributed by AV, 8-Sep-2022)

	Ref	Expression
Assertion	afv2co2	$$⊢\left(G\mathrm{defAt}X\wedge F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)\to \left(\left(F\circ G\right)\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)=\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfatsnafv2	$$⊢G\mathrm{defAt}X\to \left\{\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right\}=G\left[\left\{X\right\}\right]$$
2	1	adantr	$$⊢\left(G\mathrm{defAt}X\wedge F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)\to \left\{\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right\}=G\left[\left\{X\right\}\right]$$
3	2	imaeq2d	$$⊢\left(G\mathrm{defAt}X\wedge F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)\to F\left[\left\{\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right\}\right]=F\left[G\left[\left\{X\right\}\right]\right]$$
4		imaco	$$⊢\left(F\circ G\right)\left[\left\{X\right\}\right]=F\left[G\left[\left\{X\right\}\right]\right]$$
5	3 4	syl6reqr	$$⊢\left(G\mathrm{defAt}X\wedge F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)\to \left(F\circ G\right)\left[\left\{X\right\}\right]=F\left[\left\{\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right\}\right]$$
6	5	eleq2d	$$⊢\left(G\mathrm{defAt}X\wedge F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)\to \left(x\in \left(F\circ G\right)\left[\left\{X\right\}\right]\leftrightarrow x\in F\left[\left\{\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right\}\right]\right)$$
7	6	iotabidv	$$⊢\left(G\mathrm{defAt}X\wedge F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)\to \left(\iota x|x\in \left(F\circ G\right)\left[\left\{X\right\}\right]\right)=\left(\iota x|x\in F\left[\left\{\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right\}\right]\right)$$
8		dfatco	$$⊢\left(G\mathrm{defAt}X\wedge F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)\to \left(F\circ G\right)\mathrm{defAt}X$$
9		dfafv23	$$⊢\left(F\circ G\right)\mathrm{defAt}X\to \left(\left(F\circ G\right)\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)=\left(\iota x|x\in \left(F\circ G\right)\left[\left\{X\right\}\right]\right)$$
10	8 9	syl	$$⊢\left(G\mathrm{defAt}X\wedge F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)\to \left(\left(F\circ G\right)\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)=\left(\iota x|x\in \left(F\circ G\right)\left[\left\{X\right\}\right]\right)$$
11		dfafv23	$$⊢F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)=\left(\iota x|x\in F\left[\left\{\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right\}\right]\right)$$
12	11	adantl	$$⊢\left(G\mathrm{defAt}X\wedge F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)=\left(\iota x|x\in F\left[\left\{\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right\}\right]\right)$$
13	7 10 12	3eqtr4d	$$⊢\left(G\mathrm{defAt}X\wedge F\mathrm{defAt}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)\to \left(\left(F\circ G\right)\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)=\left(F\mathrm{\text{'}\text{'}\text{'}\text{'}}\left(G\mathrm{\text{'}\text{'}\text{'}\text{'}}X\right)\right)$$