# Metamath Proof Explorer

## Theorem funcringcsetclem8ALTV

Description: Lemma 8 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)$
funcringcsetcALTV.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({x}\mathrm{RingHom}{y}\right)}\right)$
Assertion funcringcsetclem8ALTV ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({X}{G}{Y}\right):{X}\mathrm{Hom}\left({R}\right){Y}⟶{F}\left({X}\right)\mathrm{Hom}\left({S}\right){F}\left({Y}\right)$

### 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 funcringcsetcALTV.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({x}\mathrm{RingHom}{y}\right)}\right)$
8 f1oi ${⊢}\left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}\right):{X}\mathrm{RingHom}{Y}\underset{1-1 onto}{⟶}{X}\mathrm{RingHom}{Y}$
9 f1of ${⊢}\left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}\right):{X}\mathrm{RingHom}{Y}\underset{1-1 onto}{⟶}{X}\mathrm{RingHom}{Y}\to \left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}\right):{X}\mathrm{RingHom}{Y}⟶{X}\mathrm{RingHom}{Y}$
10 8 9 mp1i ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}\right):{X}\mathrm{RingHom}{Y}⟶{X}\mathrm{RingHom}{Y}$
11 eqid ${⊢}{\mathrm{Base}}_{{X}}={\mathrm{Base}}_{{X}}$
12 eqid ${⊢}{\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{{Y}}$
13 11 12 rhmf ${⊢}{f}\in \left({X}\mathrm{RingHom}{Y}\right)\to {f}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}$
14 fvex ${⊢}{\mathrm{Base}}_{{Y}}\in \mathrm{V}$
15 fvex ${⊢}{\mathrm{Base}}_{{X}}\in \mathrm{V}$
16 14 15 pm3.2i ${⊢}\left({\mathrm{Base}}_{{Y}}\in \mathrm{V}\wedge {\mathrm{Base}}_{{X}}\in \mathrm{V}\right)$
17 elmapg ${⊢}\left({\mathrm{Base}}_{{Y}}\in \mathrm{V}\wedge {\mathrm{Base}}_{{X}}\in \mathrm{V}\right)\to \left({f}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)↔{f}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\right)$
18 17 bicomd ${⊢}\left({\mathrm{Base}}_{{Y}}\in \mathrm{V}\wedge {\mathrm{Base}}_{{X}}\in \mathrm{V}\right)\to \left({f}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}↔{f}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\right)$
19 16 18 mp1i ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({f}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}↔{f}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)\right)$
20 19 biimpa ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge {f}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\right)\to {f}\in \left({{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}\right)$
21 simpr ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {Y}\in {B}$
22 1 2 3 4 5 6 funcringcsetclem1ALTV ${⊢}\left({\phi }\wedge {Y}\in {B}\right)\to {F}\left({Y}\right)={\mathrm{Base}}_{{Y}}$
23 21 22 sylan2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {F}\left({Y}\right)={\mathrm{Base}}_{{Y}}$
24 simpl ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\right)\to {X}\in {B}$
25 1 2 3 4 5 6 funcringcsetclem1ALTV ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {F}\left({X}\right)={\mathrm{Base}}_{{X}}$
26 24 25 sylan2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {F}\left({X}\right)={\mathrm{Base}}_{{X}}$
27 23 26 oveq12d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {{F}\left({Y}\right)}^{{F}\left({X}\right)}={{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}$
28 27 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge {f}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\right)\to {{F}\left({Y}\right)}^{{F}\left({X}\right)}={{\mathrm{Base}}_{{Y}}}^{{\mathrm{Base}}_{{X}}}$
29 20 28 eleqtrrd ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\wedge {f}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\right)\to {f}\in \left({{F}\left({Y}\right)}^{{F}\left({X}\right)}\right)$
30 29 ex ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({f}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\to {f}\in \left({{F}\left({Y}\right)}^{{F}\left({X}\right)}\right)\right)$
31 13 30 syl5 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({f}\in \left({X}\mathrm{RingHom}{Y}\right)\to {f}\in \left({{F}\left({Y}\right)}^{{F}\left({X}\right)}\right)\right)$
32 31 ssrdv ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\mathrm{RingHom}{Y}\subseteq {{F}\left({Y}\right)}^{{F}\left({X}\right)}$
33 10 32 fssd ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}\right):{X}\mathrm{RingHom}{Y}⟶{{F}\left({Y}\right)}^{{F}\left({X}\right)}$
34 1 2 3 4 5 6 7 funcringcsetclem5ALTV ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}{G}{Y}={\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}$
35 5 adantr ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {U}\in \mathrm{WUni}$
36 eqid ${⊢}\mathrm{Hom}\left({R}\right)=\mathrm{Hom}\left({R}\right)$
37 24 adantl ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\in {B}$
38 21 adantl ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {Y}\in {B}$
39 1 3 35 36 37 38 ringchomALTV ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {X}\mathrm{Hom}\left({R}\right){Y}={X}\mathrm{RingHom}{Y}$
40 eqid ${⊢}\mathrm{Hom}\left({S}\right)=\mathrm{Hom}\left({S}\right)$
41 1 2 3 4 5 6 funcringcsetclem2ALTV ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {F}\left({X}\right)\in {U}$
42 24 41 sylan2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {F}\left({X}\right)\in {U}$
43 1 2 3 4 5 6 funcringcsetclem2ALTV ${⊢}\left({\phi }\wedge {Y}\in {B}\right)\to {F}\left({Y}\right)\in {U}$
44 21 43 sylan2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {F}\left({Y}\right)\in {U}$
45 2 35 40 42 44 setchom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to {F}\left({X}\right)\mathrm{Hom}\left({S}\right){F}\left({Y}\right)={{F}\left({Y}\right)}^{{F}\left({X}\right)}$
46 34 39 45 feq123d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left(\left({X}{G}{Y}\right):{X}\mathrm{Hom}\left({R}\right){Y}⟶{F}\left({X}\right)\mathrm{Hom}\left({S}\right){F}\left({Y}\right)↔\left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Y}\right)}\right):{X}\mathrm{RingHom}{Y}⟶{{F}\left({Y}\right)}^{{F}\left({X}\right)}\right)$
47 33 46 mpbird ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\right)\to \left({X}{G}{Y}\right):{X}\mathrm{Hom}\left({R}\right){Y}⟶{F}\left({X}\right)\mathrm{Hom}\left({S}\right){F}\left({Y}\right)$