Theorem algrflem

Description: Lemma for algrf and related theorems. (Contributed by Mario Carneiro, 28-May-2014) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	algrflem.1	$$⊢B\in \mathrm{V}$$
	algrflem.2	$$⊢C\in \mathrm{V}$$
Assertion	algrflem	$$⊢B\left(F\circ 1^{st}\right)C=F\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		algrflem.1	$$⊢B\in \mathrm{V}$$
2		algrflem.2	$$⊢C\in \mathrm{V}$$
3		df-ov	$$⊢B\left(F\circ 1^{st}\right)C=\left(F\circ 1^{st}\right)\left(⟨B,C⟩\right)$$
4		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
5		fof	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}:\mathrm{V}⟶\mathrm{V}$$
6	4 5	ax-mp	$$⊢1^{st}:\mathrm{V}⟶\mathrm{V}$$
7		opex	$$⊢⟨B,C⟩\in \mathrm{V}$$
8		fvco3	$$⊢\left(1^{st}:\mathrm{V}⟶\mathrm{V}\wedge ⟨B,C⟩\in \mathrm{V}\right)\to \left(F\circ 1^{st}\right)\left(⟨B,C⟩\right)=F\left(1^{st}\left(⟨B,C⟩\right)\right)$$
9	6 7 8	mp2an	$$⊢\left(F\circ 1^{st}\right)\left(⟨B,C⟩\right)=F\left(1^{st}\left(⟨B,C⟩\right)\right)$$
10	1 2	op1st	$$⊢1^{st}\left(⟨B,C⟩\right)=B$$
11	10	fveq2i	$$⊢F\left(1^{st}\left(⟨B,C⟩\right)\right)=F\left(B\right)$$
12	3 9 11	3eqtri	$$⊢B\left(F\circ 1^{st}\right)C=F\left(B\right)$$