funcrngcsetc

Description: The "natural forgetful functor" from the category of non-unital rings into the category of sets which sends each non-unital ring to its underlying set (base set) and the morphisms (non-unital ring homomorphisms) to mappings of the corresponding base sets. An alternate proof is provided in funcrngcsetcALT , using cofuval2 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc , and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc . (Contributed by AV, 26-Mar-2020)

	Ref	Expression
Hypotheses	funcrngcsetc.r	⊢ 𝑅 = ( RngCat ‘ 𝑈 )
	funcrngcsetc.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	funcrngcsetc.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	funcrngcsetc.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	funcrngcsetc.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
	funcrngcsetc.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) )
Assertion	funcrngcsetc	⊢ ( 𝜑 → 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		funcrngcsetc.r	⊢ 𝑅 = ( RngCat ‘ 𝑈 )
2		funcrngcsetc.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
3		funcrngcsetc.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		funcrngcsetc.u	⊢ ( 𝜑 → 𝑈 ∈ WUni )
5		funcrngcsetc.f	⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
6		funcrngcsetc.g	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) )
7		eqid	⊢ ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
8		eqid	⊢ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( Base ‘ ( ExtStrCat ‘ 𝑈 ) )
9		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
10	7 4	estrcbas	⊢ ( 𝜑 → 𝑈 = ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) )
11	10	mpteq1d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ↦ ( Base ‘ 𝑥 ) ) )
12		mpoeq12	⊢ ( ( 𝑈 = ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ∧ 𝑈 = ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ) → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) , 𝑦 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) )
13	10 10 12	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) , 𝑦 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) )
14	7 2 8 9 4 11 13	funcestrcsetc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) )
15		df-br	⊢ ( ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) ↔ ⟨ ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) ⟩ ∈ ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) )
16	14 15	sylib	⊢ ( 𝜑 → ⟨ ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) ⟩ ∈ ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) )
17		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18	1 17 4	rngcbas	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( 𝑈 ∩ Rng ) )
19		incom	⊢ ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 )
20	18 19	eqtrdi	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Rng ∩ 𝑈 ) )
21		eqid	⊢ ( Hom ‘ 𝑅 ) = ( Hom ‘ 𝑅 )
22	1 17 4 21	rngchomfval	⊢ ( 𝜑 → ( Hom ‘ 𝑅 ) = ( RngHom ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) )
23	7 4 20 22	rnghmsubcsetc	⊢ ( 𝜑 → ( Hom ‘ 𝑅 ) ∈ ( Subcat ‘ ( ExtStrCat ‘ 𝑈 ) ) )
24	16 23	funcres	⊢ ( 𝜑 → ( ⟨ ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) ⟩ ↾_f ( Hom ‘ 𝑅 ) ) ∈ ( ( ( ExtStrCat ‘ 𝑈 ) ↾_cat ( Hom ‘ 𝑅 ) ) Func 𝑆 ) )
25		mptexg	⊢ ( 𝑈 ∈ WUni → ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) ∈ V )
26	4 25	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) ∈ V )
27		fvex	⊢ ( Hom ‘ 𝑅 ) ∈ V
28	27	a1i	⊢ ( 𝜑 → ( Hom ‘ 𝑅 ) ∈ V )
29		mpoexga	⊢ ( ( 𝑈 ∈ WUni ∧ 𝑈 ∈ WUni ) → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) ∈ V )
30	4 4 29	syl2anc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) ∈ V )
31	18 22	rnghmresfn	⊢ ( 𝜑 → ( Hom ‘ 𝑅 ) Fn ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) )
32	26 28 30 31	resfval2	⊢ ( 𝜑 → ( ⟨ ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) ⟩ ↾_f ( Hom ‘ 𝑅 ) ) = ⟨ ( ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) ↾ ( Base ‘ 𝑅 ) ) , ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ ( Base ‘ 𝑅 ) ↦ ( ( 𝑎 ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) ) ⟩ )
33		inss1	⊢ ( 𝑈 ∩ Rng ) ⊆ 𝑈
34	18 33	eqsstrdi	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ⊆ 𝑈 )
35	34	resmptd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) ↾ ( Base ‘ 𝑅 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( Base ‘ 𝑥 ) ) )
36	3	a1i	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
37	36	mpteq1d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( Base ‘ 𝑥 ) ) )
38	5 37	eqtr2d	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( Base ‘ 𝑥 ) ) = 𝐹 )
39	35 38	eqtrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) ↾ ( Base ‘ 𝑅 ) ) = 𝐹 )
40		oveq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 RngHom 𝑦 ) = ( 𝑎 RngHom 𝑦 ) )
41	40	reseq2d	⊢ ( 𝑥 = 𝑎 → ( I ↾ ( 𝑥 RngHom 𝑦 ) ) = ( I ↾ ( 𝑎 RngHom 𝑦 ) ) )
42		oveq2	⊢ ( 𝑦 = 𝑏 → ( 𝑎 RngHom 𝑦 ) = ( 𝑎 RngHom 𝑏 ) )
43	42	reseq2d	⊢ ( 𝑦 = 𝑏 → ( I ↾ ( 𝑎 RngHom 𝑦 ) ) = ( I ↾ ( 𝑎 RngHom 𝑏 ) ) )
44	41 43	cbvmpov	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ ( I ↾ ( 𝑎 RngHom 𝑏 ) ) )
45	44	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ ( I ↾ ( 𝑎 RngHom 𝑏 ) ) ) )
46	3	a1i	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝑅 ) )
47		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) )
48		fveq2	⊢ ( 𝑦 = 𝑏 → ( Base ‘ 𝑦 ) = ( Base ‘ 𝑏 ) )
49		fveq2	⊢ ( 𝑥 = 𝑎 → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑎 ) )
50	48 49	oveqan12rd	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) = ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) )
51	50	reseq2d	⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) = ( I ↾ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ) )
52	51	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ) → ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) = ( I ↾ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ) )
53	3 34	eqsstrid	⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
54	53	sseld	⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 → 𝑎 ∈ 𝑈 ) )
55	54	com12	⊢ ( 𝑎 ∈ 𝐵 → ( 𝜑 → 𝑎 ∈ 𝑈 ) )
56	55	adantr	⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝜑 → 𝑎 ∈ 𝑈 ) )
57	56	impcom	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝑈 )
58	53	sseld	⊢ ( 𝜑 → ( 𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑈 ) )
59	58	adantld	⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝑈 ) )
60	59	imp	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝑈 )
61		ovexd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ∈ V )
62	61	resiexd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( I ↾ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ) ∈ V )
63	47 52 57 60 62	ovmpod	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) = ( I ↾ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ) )
64	63	reseq1d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑎 ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) = ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) )
65	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑈 ∈ WUni )
66		simprl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑎 ∈ 𝐵 )
67		simprr	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → 𝑏 ∈ 𝐵 )
68	1 3 65 21 66 67	rngchom	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) = ( 𝑎 RngHom 𝑏 ) )
69	68	reseq2d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) = ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 RngHom 𝑏 ) ) )
70		eqid	⊢ ( Base ‘ 𝑎 ) = ( Base ‘ 𝑎 )
71		eqid	⊢ ( Base ‘ 𝑏 ) = ( Base ‘ 𝑏 )
72	70 71	rnghmf	⊢ ( 𝑓 ∈ ( 𝑎 RngHom 𝑏 ) → 𝑓 : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) )
73		fvex	⊢ ( Base ‘ 𝑏 ) ∈ V
74		fvex	⊢ ( Base ‘ 𝑎 ) ∈ V
75	73 74	pm3.2i	⊢ ( ( Base ‘ 𝑏 ) ∈ V ∧ ( Base ‘ 𝑎 ) ∈ V )
76	75	a1i	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( Base ‘ 𝑏 ) ∈ V ∧ ( Base ‘ 𝑎 ) ∈ V ) )
77		elmapg	⊢ ( ( ( Base ‘ 𝑏 ) ∈ V ∧ ( Base ‘ 𝑎 ) ∈ V ) → ( 𝑓 ∈ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ↔ 𝑓 : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) )
78	76 77	syl	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑓 ∈ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ↔ 𝑓 : ( Base ‘ 𝑎 ) ⟶ ( Base ‘ 𝑏 ) ) )
79	72 78	imbitrrid	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑓 ∈ ( 𝑎 RngHom 𝑏 ) → 𝑓 ∈ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ) )
80	79	ssrdv	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 RngHom 𝑏 ) ⊆ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) )
81	80	resabs1d	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑_m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 RngHom 𝑏 ) ) = ( I ↾ ( 𝑎 RngHom 𝑏 ) ) )
82	64 69 81	3eqtrrd	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( I ↾ ( 𝑎 RngHom 𝑏 ) ) = ( ( 𝑎 ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) )
83	36 46 82	mpoeq123dva	⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ ( I ↾ ( 𝑎 RngHom 𝑏 ) ) ) = ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ ( Base ‘ 𝑅 ) ↦ ( ( 𝑎 ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) ) )
84	6 45 83	3eqtrrd	⊢ ( 𝜑 → ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ ( Base ‘ 𝑅 ) ↦ ( ( 𝑎 ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) ) = 𝐺 )
85	39 84	opeq12d	⊢ ( 𝜑 → ⟨ ( ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) ↾ ( Base ‘ 𝑅 ) ) , ( 𝑎 ∈ ( Base ‘ 𝑅 ) , 𝑏 ∈ ( Base ‘ 𝑅 ) ↦ ( ( 𝑎 ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) ) ⟩ = ⟨ 𝐹 , 𝐺 ⟩ )
86	32 85	eqtr2d	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ( ⟨ ( 𝑥 ∈ 𝑈 ↦ ( Base ‘ 𝑥 ) ) , ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑_m ( Base ‘ 𝑥 ) ) ) ) ⟩ ↾_f ( Hom ‘ 𝑅 ) ) )
87	1 4 18 22	rngcval	⊢ ( 𝜑 → 𝑅 = ( ( ExtStrCat ‘ 𝑈 ) ↾_cat ( Hom ‘ 𝑅 ) ) )
88	87	oveq1d	⊢ ( 𝜑 → ( 𝑅 Func 𝑆 ) = ( ( ( ExtStrCat ‘ 𝑈 ) ↾_cat ( Hom ‘ 𝑅 ) ) Func 𝑆 ) )
89	24 86 88	3eltr4d	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
90		df-br	⊢ ( 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
91	89 90	sylibr	⊢ ( 𝜑 → 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )

Metamath Proof Explorer

Theorem funcrngcsetc

Proof