# Metamath Proof Explorer

## Theorem funcringcsetcALTV2lem1

Description: Lemma 1 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 funcringcsetcALTV2lem1 ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {F}\left({X}\right)={\mathrm{Base}}_{{X}}$

### 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 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}}$