Theorem funcringcsetcALTV2lem4

Description: Lemma 4 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)$$
	funcringcsetcALTV2.g	$$⊢\phi \to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\right)$$
Assertion	funcringcsetcALTV2lem4	$$⊢\phi \to GFn\left(B\times B\right)$$

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		funcringcsetcALTV2.g	$$⊢\phi \to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\right)$$
8		eqid	$$⊢\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\right)=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\right)$$
9		ovex	$$⊢x\mathrm{RingHom}y\in \mathrm{V}$$
10		id	$$⊢x\mathrm{RingHom}y\in \mathrm{V}\to x\mathrm{RingHom}y\in \mathrm{V}$$
11	10	resiexd	$$⊢x\mathrm{RingHom}y\in \mathrm{V}\to {\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\in \mathrm{V}$$
12	9 11	ax-mp	$$⊢{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\in \mathrm{V}$$
13	8 12	fnmpoi	$$⊢\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\right)Fn\left(B\times B\right)$$
14	7	fneq1d	$$⊢\phi \to \left(GFn\left(B\times B\right)\leftrightarrow \left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\right)Fn\left(B\times B\right)\right)$$
15	13 14	mpbiri	$$⊢\phi \to GFn\left(B\times B\right)$$