Theorem funcringcsetcALTV2lem3

Description: Lemma 3 for funcringcsetcALTV2 . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	funcringcsetcALTV2.r	$$⊢R=\mathrm{RingCat}\left(U\right)$$
	funcringcsetcALTV2.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
	funcringcsetcALTV2.b	$$⊢B={\mathrm{Base}}_R$$
	funcringcsetcALTV2.c	$$⊢C={\mathrm{Base}}_S$$
	funcringcsetcALTV2.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	funcringcsetcALTV2.f	$$⊢\phi \to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
Assertion	funcringcsetcALTV2lem3	$$⊢\phi \to F:B⟶C$$

Proof

Step	Hyp	Ref	Expression
1		funcringcsetcALTV2.r	$$⊢R=\mathrm{RingCat}\left(U\right)$$
2		funcringcsetcALTV2.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
3		funcringcsetcALTV2.b	$$⊢B={\mathrm{Base}}_R$$
4		funcringcsetcALTV2.c	$$⊢C={\mathrm{Base}}_S$$
5		funcringcsetcALTV2.u	$$⊢\phi \to U\in \mathrm{WUni}$$
6		funcringcsetcALTV2.f	$$⊢\phi \to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
7	1 3 5	ringcbasbas	$$⊢\left(\phi \wedge x\in B\right)\to {\mathrm{Base}}_x\in U$$
8	2 5	setcbas	$$⊢\phi \to U={\mathrm{Base}}_S$$
9	8	eqcomd	$$⊢\phi \to {\mathrm{Base}}_S=U$$
10	9	adantr	$$⊢\left(\phi \wedge x\in B\right)\to {\mathrm{Base}}_S=U$$
11	7 10	eleqtrrd	$$⊢\left(\phi \wedge x\in B\right)\to {\mathrm{Base}}_x\in {\mathrm{Base}}_S$$
12	11 4	eleqtrrdi	$$⊢\left(\phi \wedge x\in B\right)\to {\mathrm{Base}}_x\in C$$
13	12	fmpttd	$$⊢\phi \to \left(x\in B⟼{\mathrm{Base}}_x\right):B⟶C$$
14	6	feq1d	$$⊢\phi \to \left(F:B⟶C\leftrightarrow \left(x\in B⟼{\mathrm{Base}}_x\right):B⟶C\right)$$
15	13 14	mpbird	$$⊢\phi \to F:B⟶C$$