funcringcsetclem8ALTV

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

	Ref	Expression
Hypotheses	funcringcsetcALTV.r	$⊢ R = RingCatALTV (U)$
	funcringcsetcALTV.s	$⊢ S = SetCat (U)$
	funcringcsetcALTV.b	$⊢ B = {Base}_{R}$
	funcringcsetcALTV.c	$⊢ C = {Base}_{S}$
	funcringcsetcALTV.u	$⊢ φ \to U \in WUni$
	funcringcsetcALTV.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
	funcringcsetcALTV.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
Assertion	funcringcsetclem8ALTV	$⊢ (φ \land (X \in B \land Y \in B)) \to (X G Y) : X Hom (R) Y ⟶ F (X) Hom (S) F (Y)$

Proof

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

Metamath Proof Explorer

Theorem funcringcsetclem8ALTV

Proof