funcringcsetcALTV2lem8

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

	Ref	Expression
Hypotheses	funcringcsetcALTV2.r	$⊢ R = RingCat (U)$
	funcringcsetcALTV2.s	$⊢ S = SetCat (U)$
	funcringcsetcALTV2.b	$⊢ B = {Base}_{R}$
	funcringcsetcALTV2.c	$⊢ C = {Base}_{S}$
	funcringcsetcALTV2.u	$⊢ φ \to U \in WUni$
	funcringcsetcALTV2.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
	funcringcsetcALTV2.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
Assertion	funcringcsetcALTV2lem8	$⊢ (φ \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		funcringcsetcALTV2.r	$⊢ R = RingCat (U)$
2		funcringcsetcALTV2.s	$⊢ S = SetCat (U)$
3		funcringcsetcALTV2.b	$⊢ B = {Base}_{R}$
4		funcringcsetcALTV2.c	$⊢ C = {Base}_{S}$
5		funcringcsetcALTV2.u	$⊢ φ \to U \in WUni$
6		funcringcsetcALTV2.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
7		funcringcsetcALTV2.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	funcringcsetcALTV2lem1	$⊢ (φ \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	funcringcsetcALTV2lem1	$⊢ (φ \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	funcringcsetcALTV2lem5	$⊢ (φ \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	ringchom	$⊢ (φ \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	funcringcsetcALTV2lem2	$⊢ (φ \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	funcringcsetcALTV2lem2	$⊢ (φ \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 funcringcsetcALTV2lem8

Proof