Theorem funcringcsetclem1ALTV

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

	Ref	Expression
Hypotheses	funcringcsetcALTV.r	$$⊢R=\mathrm{RingCatALTV}\left(U\right)$$
	funcringcsetcALTV.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
	funcringcsetcALTV.b	$$⊢B={\mathrm{Base}}_R$$
	funcringcsetcALTV.c	$$⊢C={\mathrm{Base}}_S$$
	funcringcsetcALTV.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	funcringcsetcALTV.f	$$⊢\phi \to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
Assertion	funcringcsetclem1ALTV	$$⊢\left(\phi \wedge X\in B\right)\to F\left(X\right)={\mathrm{Base}}_X$$

Proof

Step	Hyp	Ref	Expression
1		funcringcsetcALTV.r	$$⊢R=\mathrm{RingCatALTV}\left(U\right)$$
2		funcringcsetcALTV.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
3		funcringcsetcALTV.b	$$⊢B={\mathrm{Base}}_R$$
4		funcringcsetcALTV.c	$$⊢C={\mathrm{Base}}_S$$
5		funcringcsetcALTV.u	$$⊢\phi \to U\in \mathrm{WUni}$$
6		funcringcsetcALTV.f	$$⊢\phi \to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
7	6	adantr	$$⊢\left(\phi \wedge X\in B\right)\to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
8		fveq2	$$⊢x=X\to {\mathrm{Base}}_x={\mathrm{Base}}_X$$
9	8	adantl	$$⊢\left(\left(\phi \wedge X\in B\right)\wedge x=X\right)\to {\mathrm{Base}}_x={\mathrm{Base}}_X$$
10		simpr	$$⊢\left(\phi \wedge X\in B\right)\to X\in B$$
11		fvexd	$$⊢\left(\phi \wedge X\in B\right)\to {\mathrm{Base}}_X\in \mathrm{V}$$
12	7 9 10 11	fvmptd	$$⊢\left(\phi \wedge X\in B\right)\to F\left(X\right)={\mathrm{Base}}_X$$