Metamath Proof Explorer

Theorem 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 ↾ ( 𝑥 RngHomo 𝑦 ) ) ) )
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 ↾ ( 𝑥 RngHomo 𝑦 ) ) ) )
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 ‘ 𝑅 ) = ( RngHomo ↾ ( ( 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 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 RngHomo 𝑦 ) = ( 𝑎 RngHomo 𝑦 ) )
41 40 reseq2d ⊢ ( 𝑥 = 𝑎 → ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) = ( I ↾ ( 𝑎 RngHomo 𝑦 ) ) )
42 oveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 RngHomo 𝑦 ) = ( 𝑎 RngHomo 𝑏 ) )
43 42 reseq2d ⊢ ( 𝑦 = 𝑏 → ( I ↾ ( 𝑎 RngHomo 𝑦 ) ) = ( I ↾ ( 𝑎 RngHomo 𝑏 ) ) )
44 41 43 cbvmpov ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ) = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ ( I ↾ ( 𝑎 RngHomo 𝑏 ) ) )
45 44 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ) = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ ( I ↾ ( 𝑎 RngHomo 𝑏 ) ) ) )
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 ‘ 𝑅 ) 𝑏 ) = ( 𝑎 RngHomo 𝑏 ) )
69 68 reseq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) = ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 RngHomo 𝑏 ) ) )
70 eqid ⊢ ( Base ‘ 𝑎 ) = ( Base ‘ 𝑎 )
71 eqid ⊢ ( Base ‘ 𝑏 ) = ( Base ‘ 𝑏 )
72 70 71 rnghmf ⊢ ( 𝑓 ∈ ( 𝑎 RngHomo 𝑏 ) → 𝑓 : ( 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 syl5ibr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑓 ∈ ( 𝑎 RngHomo 𝑏 ) → 𝑓 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
80 79 ssrdv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 RngHomo 𝑏 ) ⊆ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
81 80 resabs1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 RngHomo 𝑏 ) ) = ( I ↾ ( 𝑎 RngHomo 𝑏 ) ) )
82 64 69 81 3eqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( I ↾ ( 𝑎 RngHomo 𝑏 ) ) = ( ( 𝑎 ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) )
83 36 46 82 mpoeq123dva ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ ( I ↾ ( 𝑎 RngHomo 𝑏 ) ) ) = ( 𝑎 ∈ ( 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 𝑆 ) 𝐺 )