Theorem caofid0l

Description: Transfer a left identity law to the function operation. (Contributed by NM, 21-Oct-2014)

	Ref	Expression
Hypotheses	caofref.1	$$⊢\phi \to A\in V$$
	caofref.2	$$⊢\phi \to F:A⟶S$$
	caofid0.3	$$⊢\phi \to B\in W$$
	caofid0l.5	$$⊢\left(\phi \wedge x\in S\right)\to BRx=x$$
Assertion	caofid0l	$$⊢\phi \to \left(A\times \left\{B\right\}\right)R_{f}F=F$$

Proof

Step	Hyp	Ref	Expression
1		caofref.1	$$⊢\phi \to A\in V$$
2		caofref.2	$$⊢\phi \to F:A⟶S$$
3		caofid0.3	$$⊢\phi \to B\in W$$
4		caofid0l.5	$$⊢\left(\phi \wedge x\in S\right)\to BRx=x$$
5		fnconstg	$$⊢B\in W\to \left(A\times \left\{B\right\}\right)FnA$$
6	3 5	syl	$$⊢\phi \to \left(A\times \left\{B\right\}\right)FnA$$
7	2	ffnd	$$⊢\phi \to FFnA$$
8		fvconst2g	$$⊢\left(B\in W\wedge w\in A\right)\to \left(A\times \left\{B\right\}\right)\left(w\right)=B$$
9	3 8	sylan	$$⊢\left(\phi \wedge w\in A\right)\to \left(A\times \left\{B\right\}\right)\left(w\right)=B$$
10		eqidd	$$⊢\left(\phi \wedge w\in A\right)\to F\left(w\right)=F\left(w\right)$$
11	4	ralrimiva	$$⊢\phi \to \forall x\in SBRx=x$$
12	2	ffvelcdmda	$$⊢\left(\phi \wedge w\in A\right)\to F\left(w\right)\in S$$
13		oveq2	$$⊢x=F\left(w\right)\to BRx=BRF\left(w\right)$$
14		id	$$⊢x=F\left(w\right)\to x=F\left(w\right)$$
15	13 14	eqeq12d	$$⊢x=F\left(w\right)\to \left(BRx=x\leftrightarrow BRF\left(w\right)=F\left(w\right)\right)$$
16	15	rspccva	$$⊢\left(\forall x\in SBRx=x\wedge F\left(w\right)\in S\right)\to BRF\left(w\right)=F\left(w\right)$$
17	11 12 16	syl2an2r	$$⊢\left(\phi \wedge w\in A\right)\to BRF\left(w\right)=F\left(w\right)$$
18	1 6 7 7 9 10 17	offveq	$$⊢\phi \to \left(A\times \left\{B\right\}\right)R_{f}F=F$$