Metamath Proof Explorer

Theorem funcringcsetc

Description: The "natural forgetful functor" from the category of unital rings into the category of sets which sends each ring to its underlying set (base set) and the morphisms (ring homomorphisms) to mappings of the corresponding base sets. (Contributed by AV, 26-Mar-2020)

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

Proof

Step Hyp Ref Expression
1 funcringcsetc.r ⊢ 𝑅 = ( RingCat ‘ 𝑈 )
2 funcringcsetc.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
3 funcringcsetc.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 funcringcsetc.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
5 funcringcsetc.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
6 funcringcsetc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) )
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 ringcbas ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( 𝑈 ∩ Ring ) )
19 incom ⊢ ( 𝑈 ∩ Ring ) = ( Ring ∩ 𝑈 )
20 18 19 eqtrdi ⊢ ( 𝜑 → ( Base ‘ 𝑅 ) = ( Ring ∩ 𝑈 ) )
21 eqid ⊢ ( Hom ‘ 𝑅 ) = ( Hom ‘ 𝑅 )
22 1 17 4 21 ringchomfval ⊢ ( 𝜑 → ( Hom ‘ 𝑅 ) = ( RingHom ↾ ( ( Base ‘ 𝑅 ) × ( Base ‘ 𝑅 ) ) ) )
23 7 4 20 22 rhmsubcsetc ⊢ ( 𝜑 → ( 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 rhmresfn ⊢ ( 𝜑 → ( 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 ⊢ ( 𝑈 ∩ Ring ) ⊆ 𝑈
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 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 RingHom 𝑦 ) = ( 𝑎 RingHom 𝑦 ) )
41 40 reseq2d ⊢ ( 𝑥 = 𝑎 → ( I ↾ ( 𝑥 RingHom 𝑦 ) ) = ( I ↾ ( 𝑎 RingHom 𝑦 ) ) )
42 oveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝑎 RingHom 𝑦 ) = ( 𝑎 RingHom 𝑏 ) )
43 42 reseq2d ⊢ ( 𝑦 = 𝑏 → ( I ↾ ( 𝑎 RingHom 𝑦 ) ) = ( I ↾ ( 𝑎 RingHom 𝑏 ) ) )
44 41 43 cbvmpov ⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ ( I ↾ ( 𝑎 RingHom 𝑏 ) ) )
45 44 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RingHom 𝑦 ) ) ) = ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ ( I ↾ ( 𝑎 RingHom 𝑏 ) ) ) )
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 ringchom ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) = ( 𝑎 RingHom 𝑏 ) )
69 68 reseq2d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) = ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 RingHom 𝑏 ) ) )
70 eqid ⊢ ( Base ‘ 𝑎 ) = ( Base ‘ 𝑎 )
71 eqid ⊢ ( Base ‘ 𝑏 ) = ( Base ‘ 𝑏 )
72 70 71 rhmf ⊢ ( 𝑓 ∈ ( 𝑎 RingHom 𝑏 ) → 𝑓 : ( 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 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑓 ∈ ( 𝑎 RingHom 𝑏 ) → 𝑓 ∈ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) )
80 79 ssrdv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( 𝑎 RingHom 𝑏 ) ⊆ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) )
81 80 resabs1d ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( I ↾ ( ( Base ‘ 𝑏 ) ↑m ( Base ‘ 𝑎 ) ) ) ↾ ( 𝑎 RingHom 𝑏 ) ) = ( I ↾ ( 𝑎 RingHom 𝑏 ) ) )
82 64 69 81 3eqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( I ↾ ( 𝑎 RingHom 𝑏 ) ) = ( ( 𝑎 ( 𝑥 ∈ 𝑈 , 𝑦 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ) 𝑏 ) ↾ ( 𝑎 ( Hom ‘ 𝑅 ) 𝑏 ) ) )
83 36 46 82 mpoeq123dva ⊢ ( 𝜑 → ( 𝑎 ∈ 𝐵 , 𝑏 ∈ 𝐵 ↦ ( I ↾ ( 𝑎 RingHom 𝑏 ) ) ) = ( 𝑎 ∈ ( 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 ringcval ⊢ ( 𝜑 → 𝑅 = ( ( 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 𝑆 ) 𝐺 )