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 ↾ ( 𝑥 RngHomo 𝑦 ) ) ) )
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 ↾ ( 𝑥 RngHomo 𝑦 ) ) ) )
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	syl6bi	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 → 𝑥 ∈ 𝑈 ) )
16	15	ssrdv	⊢ ( 𝜑 → 𝐵 ⊆ 𝑈 )
17	16	resmptd	⊢ ( 𝜑 → ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ↾ 𝐵 ) = ( 𝑢 ∈ 𝐵 ↦ ( Base ‘ 𝑢 ) ) )
18	10 17	syl5req	⊢ ( 𝜑 → ( 𝑢 ∈ 𝐵 ↦ ( Base ‘ 𝑢 ) ) = ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ∘ ( I ↾ 𝐵 ) ) )
19	9 18	eqtrd	⊢ ( 𝜑 → 𝐹 = ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ∘ ( I ↾ 𝐵 ) ) )
20		coires1	⊢ ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ) = ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ↾ ( 𝑥 RngHomo 𝑦 ) )
21		eqid	⊢ ( Base ‘ 𝑥 ) = ( Base ‘ 𝑥 )
22		eqid	⊢ ( Base ‘ 𝑦 ) = ( Base ‘ 𝑦 )
23	21 22	rnghmf	⊢ ( 𝑧 ∈ ( 𝑥 RngHomo 𝑦 ) → 𝑧 : ( 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	syl5ibr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑧 ∈ ( 𝑥 RngHomo 𝑦 ) → 𝑧 ∈ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) )
30	29	ssrdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 RngHomo 𝑦 ) ⊆ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) )
31	30	resabs1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ↾ ( 𝑥 RngHomo 𝑦 ) ) = ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) )
32	20 31	syl5req	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) = ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ) )
33	32	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ) ) )
34	6 33	eqtrd	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ) ) )
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	syl6bi	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝑈 ) )
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 ↾ ( 𝑓 RngHomo 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) )
66		oveq12	⊢ ( ( 𝑓 = 𝑥 ∧ 𝑔 = 𝑦 ) → ( 𝑓 RngHomo 𝑔 ) = ( 𝑥 RngHomo 𝑦 ) )
67	66	reseq2d	⊢ ( ( 𝑓 = 𝑥 ∧ 𝑔 = 𝑦 ) → ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) = ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) )
68	67	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ( 𝑓 = 𝑥 ∧ 𝑔 = 𝑦 ) ) → ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) = ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) )
69		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
70		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
71		ovex	⊢ ( 𝑥 RngHomo 𝑦 ) ∈ V
72	71	a1i	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 RngHomo 𝑦 ) ∈ V )
73	72	resiexd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ∈ V )
74	65 68 69 70 73	ovmpod	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) 𝑦 ) = ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) )
75	74	eqcomd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) = ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) 𝑦 ) )
76	64 75	coeq12d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ) = ( ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) 𝑦 ) ) )
77	35 36 76	mpoeq123dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( I ↾ ( ( Base ‘ 𝑦 ) ↑m ( Base ‘ 𝑥 ) ) ) ∘ ( I ↾ ( 𝑥 RngHomo 𝑦 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) 𝑦 ) ) ) )
78	34 77	eqtrd	⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) 𝑦 ) ) ) )
79	19 78	opeq12d	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ⟨ ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ∘ ( I ↾ 𝐵 ) ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) 𝑦 ) ) ) ⟩ )
80		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
81		eqid	⊢ ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
82		eqidd	⊢ ( 𝜑 → ( I ↾ 𝐵 ) = ( I ↾ 𝐵 ) )
83		eqidd	⊢ ( 𝜑 → ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) = ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) )
84	1 81 3 4 82 83	rngcifuestrc	⊢ ( 𝜑 → ( I ↾ 𝐵 ) ( 𝑅 Func ( ExtStrCat ‘ 𝑈 ) ) ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) )
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 ↾ ( 𝑓 RngHomo 𝑔 ) ) ) ⟩ ) = ⟨ ( ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) ∘ ( I ↾ 𝐵 ) ) , ( 𝑥 ∈ ( Base ‘ 𝑅 ) , 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ ( ( ( ( I ↾ 𝐵 ) ‘ 𝑥 ) ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ( ( I ↾ 𝐵 ) ‘ 𝑦 ) ) ∘ ( 𝑥 ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) 𝑦 ) ) ) ⟩ )
102	79 101	eqtr4d	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ = ( ⟨ ( 𝑢 ∈ 𝑈 ↦ ( Base ‘ 𝑢 ) ) , ( 𝑤 ∈ 𝑈 , 𝑧 ∈ 𝑈 ↦ ( I ↾ ( ( Base ‘ 𝑧 ) ↑m ( Base ‘ 𝑤 ) ) ) ) ⟩ ∘func ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) ⟩ ) )
103		df-br	⊢ ( ( I ↾ 𝐵 ) ( 𝑅 Func ( ExtStrCat ‘ 𝑈 ) ) ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) ↔ ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) ⟩ ∈ ( 𝑅 Func ( ExtStrCat ‘ 𝑈 ) ) )
104	84 103	sylib	⊢ ( 𝜑 → ⟨ ( I ↾ 𝐵 ) , ( 𝑓 ∈ 𝐵 , 𝑔 ∈ 𝐵 ↦ ( I ↾ ( 𝑓 RngHomo 𝑔 ) ) ) ⟩ ∈ ( 𝑅 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 ↾ ( 𝑓 RngHomo 𝑔 ) ) ) ⟩ ) ∈ ( 𝑅 Func 𝑆 ) )
108	102 107	eqeltrd	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
109		df-br	⊢ ( 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 Func 𝑆 ) )
110	108 109	sylibr	⊢ ( 𝜑 → 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )