Metamath Proof Explorer

Theorem funcrngcsetcALT

Description: Alternate proof of funcrngcsetc , 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 . Surprisingly, this proof is longer than the direct proof given in funcrngcsetc . (Contributed by AV, 30-Mar-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 funcrngcsetcALT.r ⊢ 𝑅 = ( RngCat ‘ 𝑈 )
2 funcrngcsetcALT.s ⊢ 𝑆 = ( SetCat ‘ 𝑈 )
3 funcrngcsetcALT.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
4 funcrngcsetcALT.u ⊢ ( 𝜑 → 𝑈 ∈ WUni )
5 funcrngcsetcALT.f ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) )
6 funcrngcsetcALT.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) )
7 fveq2 ⊢ ( 𝑥 = 𝑢 → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑢 ) )
8 7 cbvmptv ⊢ ( 𝑥 ∈ 𝐵 ↦ ( Base ‘ 𝑥 ) ) = ( 𝑢 ∈ 𝐵 ↦ ( Base ‘ 𝑢 ) )
9 5 8 eqtrdi ⊢ ( 𝜑 → 𝐹 = ( 𝑢 ∈ 𝐵 ↦ ( Base ‘ 𝑢 ) ) )
10 coires1 ⊢ ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ∘ ( I ↾ 𝐵 ) ) = ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ↾ 𝐵 )
11 1 3 4 rngcbas ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
12 11 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( 𝑈 ∩ Rng ) ) )
13 elin ⊢ ( 𝑥 ∈ ( 𝑈 ∩ Rng ) ↔ ( 𝑥 ∈ 𝑈 ∧ 𝑥 ∈ Rng ) )
14 13 simplbi ⊢ ( 𝑥 ∈ ( 𝑈 ∩ Rng ) → 𝑥 ∈ 𝑈 )
15 12 14 biimtrdi ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈 ) )
16 15 ssrdv ⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
17 16 resmptd ⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ↾ 𝐵 ) = ( 𝑢 ∈ 𝐵 ↦ ( Base ‘ 𝑢 ) ) )
18 10 17 eqtr2id ⊢ ( 𝜑 → ( 𝑢 ∈ 𝐵 ↦ ( Base ‘ 𝑢 ) ) = ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ∘ ( I ↾ 𝐵 ) ) )
19 9 18 eqtrd ⊢ ( 𝜑 → 𝐹 = ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ∘ ( I ↾ 𝐵 ) ) )
20 coires1 ⊢ ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) = ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ↾ ( 𝑥 RngHom 𝑦 ) )
21 eqid ⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
22 eqid ⊢ ( Base ‘ 𝑦 ) = ( Base ‘ 𝑦 )
23 21 22 rnghmf ⊢ ( 𝑧 ∈ ( 𝑥 RngHom 𝑦 ) → 𝑧 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) )
24 fvex ⊢ ( Base ‘ 𝑦 ) ∈ V
25 fvex ⊢ ( Base ‘ 𝑥 ) ∈ V
26 24 25 pm3.2i ⊢ ( ( Base ‘ 𝑦 ) ∈ V ∧ ( Base ‘ 𝑥 ) ∈ V )
27 elmapg ⊢ ( ( ( Base ‘ 𝑦 ) ∈ V ∧ ( Base ‘ 𝑥 ) ∈ V ) → ( 𝑧 ∈ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ↔ 𝑧 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
28 26 27 mp1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 ∈ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ↔ 𝑧 : ( Base ‘ 𝑥 ) ⟶ ( Base ‘ 𝑦 ) ) )
29 23 28 imbitrrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 ∈ ( 𝑥 RngHom 𝑦 ) → 𝑧 ∈ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
30 29 ssrdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 RngHom 𝑦 ) ⊆ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) )
31 30 resabs1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ↾ ( 𝑥 RngHom 𝑦 ) ) = ( I ↾ ( 𝑥 RngHom 𝑦 ) ) )
32 20 31 eqtr2id ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( I ↾ ( 𝑥 RngHom 𝑦 ) ) = ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) )
33 32 mpoeq3dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) ) )
34 6 33 eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) ) )
35 3 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑅 ) )
36 3 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐵 = ( Base ‘ 𝑅 ) )
37 fvresi ⊢ ( 𝑥 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
38 37 adantr ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
39 38 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑥 ) = 𝑥 )
40 fvresi ⊢ ( 𝑦 ∈ 𝐵 → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
41 40 adantl ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
42 41 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ 𝐵 ) ‘ 𝑦 ) = 𝑦 )
43 39 42 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) = ( 𝑥 ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) 𝑦 ) )
44 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) = ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) )
45 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ) → 𝑧 = 𝑦 )
46 45 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ) → ( Base ‘ 𝑧 ) = ( Base ‘ 𝑦 ) )
47 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ) → 𝑤 = 𝑥 )
48 47 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ) → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑥 ) )
49 46 48 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ) → ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) = ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) )
50 49 reseq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑤 = 𝑥 ∧ 𝑧 = 𝑦 ) ) → ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) = ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
51 15 com12 ⊢ ( 𝑥 ∈ 𝐵 → ( 𝜑 → 𝑥 ∈ 𝑈 ) )
52 51 adantr ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝜑 → 𝑥 ∈ 𝑈 ) )
53 52 impcom ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝑈 )
54 11 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( 𝑈 ∩ Rng ) ) )
55 elin ⊢ ( 𝑦 ∈ ( 𝑈 ∩ Rng ) ↔ ( 𝑦 ∈ 𝑈 ∧ 𝑦 ∈ Rng ) )
56 55 simplbi ⊢ ( 𝑦 ∈ ( 𝑈 ∩ Rng ) → 𝑦 ∈ 𝑈 )
57 54 56 biimtrdi ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑈 ) )
58 57 a1d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑈 ) ) )
59 58 imp32 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝑈 )
60 ovex ⊢ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ∈ V
61 60 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ∈ V )
62 61 resiexd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∈ V )
63 44 50 53 59 62 ovmpod ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) 𝑦 ) = ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
64 43 63 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) = ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) )
65 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) )
66 oveq12 ⊢ ( ( 𝑓 = 𝑥 ∧ 𝑔 = 𝑦 ) → ( 𝑓 RngHom 𝑔 ) = ( 𝑥 RngHom 𝑦 ) )
67 66 reseq2d ⊢ ( ( 𝑓 = 𝑥 ∧ 𝑔 = 𝑦 ) → ( I ↾ ( 𝑓 RngHom 𝑔 ) ) = ( I ↾ ( 𝑥 RngHom 𝑦 ) ) )
68 67 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑓 = 𝑥 ∧ 𝑔 = 𝑦 ) ) → ( I ↾ ( 𝑓 RngHom 𝑔 ) ) = ( I ↾ ( 𝑥 RngHom 𝑦 ) ) )
69 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
70 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
71 ovex ⊢ ( 𝑥 RngHom 𝑦 ) ∈ V
72 71 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 RngHom 𝑦 ) ∈ V )
73 72 resiexd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ∈ V )
74 65 68 69 70 73 ovmpod ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) 𝑦 ) = ( I ↾ ( 𝑥 RngHom 𝑦 ) ) )
75 74 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( I ↾ ( 𝑥 RngHom 𝑦 ) ) = ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) 𝑦 ) )
76 64 75 coeq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) = ( ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) 𝑦 ) ) )
77 35 36 76 mpoeq123dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHom 𝑦 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) 𝑦 ) ) ) )
78 34 77 eqtrd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) 𝑦 ) ) ) )
79 19 78 opeq12d ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ⟨ ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ∘ ( I ↾ 𝐵 ) ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) 𝑦 ) ) ) ⟩ )
80 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
81 eqid ⊢ ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
82 eqidd ⊢ ( 𝜑 → ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) )
83 eqidd ⊢ ( 𝜑 → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) )
84 1 81 3 4 82 83 rngcifuestrc ⊢ ( 𝜑 → ( I ↾ 𝐵 ) ( 𝑅 Func ( ExtStrCat ‘ 𝑈 ) ) ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) )
85 eqid ⊢ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( Base ‘ ( ExtStrCat ‘ 𝑈 ) )
86 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
87 81 4 estrcbas ⊢ ( 𝜑 → 𝑈 = ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) )
88 87 mpteq1d ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) = ( 𝑢 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ↦ ( Base ‘ 𝑢 ) ) )
89 fveq2 ⊢ ( 𝑤 = 𝑢 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝑢 ) )
90 89 oveq2d ⊢ ( 𝑤 = 𝑢 → ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) = ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑢 ) ) )
91 90 reseq2d ⊢ ( 𝑤 = 𝑢 → ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) = ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑢 ) ) ) )
92 fveq2 ⊢ ( 𝑧 = 𝑣 → ( Base ‘ 𝑧 ) = ( Base ‘ 𝑣 ) )
93 92 oveq1d ⊢ ( 𝑧 = 𝑣 → ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑢 ) ) = ( ( Base ‘ 𝑣 ) ↑m ( Base ‘ 𝑢 ) ) )
94 93 reseq2d ⊢ ( 𝑧 = 𝑣 → ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑢 ) ) ) = ( I ↾ ( ( Base ‘ 𝑣 ) ↑m ( Base ‘ 𝑢 ) ) ) )
95 91 94 cbvmpov ⊢ ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) = ( 𝑢 ∈ 𝑈 , 𝑣 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑣 ) ↑m ( Base ‘ 𝑢 ) ) ) )
96 95 a1i ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) = ( 𝑢 ∈ 𝑈 , 𝑣 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑣 ) ↑m ( Base ‘ 𝑢 ) ) ) ) )
97 eqidd ⊢ ( 𝜑 → ( I ↾ ( ( Base ‘ 𝑣 ) ↑m ( Base ‘ 𝑢 ) ) ) = ( I ↾ ( ( Base ‘ 𝑣 ) ↑m ( Base ‘ 𝑢 ) ) ) )
98 87 87 97 mpoeq123dv ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 , 𝑣 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑣 ) ↑m ( Base ‘ 𝑢 ) ) ) ) = ( 𝑢 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) , 𝑣 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ↦ ( I ↾ ( ( Base ‘ 𝑣 ) ↑m ( Base ‘ 𝑢 ) ) ) ) )
99 96 98 eqtrd ⊢ ( 𝜑 → ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) = ( 𝑢 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) , 𝑣 ∈ ( Base ‘ ( ExtStrCat ‘ 𝑈 ) ) ↦ ( I ↾ ( ( Base ‘ 𝑣 ) ↑m ( Base ‘ 𝑢 ) ) ) ) )
100 81 2 85 86 4 88 99 funcestrcsetc ⊢ ( 𝜑 → ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) )
101 80 84 100 cofuval2 ⊢ ( 𝜑 → ( ⟨ ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) , ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ⟩ ∘func ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) ⟩ ) = ⟨ ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ∘ ( I ↾ 𝐵 ) ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) 𝑦 ) ) ) ⟩ )
102 79 101 eqtr4d ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ( ⟨ ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) , ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ⟩ ∘func ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) ⟩ ) )
103 df-br ⊢ ( ( I ↾ 𝐵 ) ( 𝑅 Func ( ExtStrCat ‘ 𝑈 ) ) ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) ↔ ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) ⟩ ∈ ( 𝑅 Func ( ExtStrCat ‘ 𝑈 ) ) )
104 84 103 sylib ⊢ ( 𝜑 → ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) ⟩ ∈ ( 𝑅 Func ( ExtStrCat ‘ 𝑈 ) ) )
105 df-br ⊢ ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ↔ ⟨ ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) , ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ⟩ ∈ ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) )
106 100 105 sylib ⊢ ( 𝜑 → ⟨ ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) , ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ⟩ ∈ ( ( ExtStrCat ‘ 𝑈 ) Func 𝑆 ) )
107 104 106 cofucl ⊢ ( 𝜑 → ( ⟨ ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) , ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ⟩ ∘func ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHom 𝑔 ) ) ) ⟩ ) ∈ ( 𝑅 Func 𝑆 ) )
108 102 107 eqeltrd ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
109 df-br ⊢ ( 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
110 108 109 sylibr ⊢ ( 𝜑 → 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )