fucofvalg

Description: Value of the function giving the functor composition bifunctor. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	fucofvalg.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑈 )
	fucofvalg.c	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) = 𝐶 )
	fucofvalg.d	⊢ ( 𝜑 → ( 2^nd ‘ 𝑃 ) = 𝐷 )
	fucofvalg.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
	fucofvalg.o	⊢ ( 𝜑 → ( 𝑃 ∘_F 𝐸 ) = ⚬ )
	fucofvalg.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
Assertion	fucofvalg	⊢ ( 𝜑 → ⚬ = ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		fucofvalg.p	⊢ ( 𝜑 → 𝑃 ∈ 𝑈 )
2		fucofvalg.c	⊢ ( 𝜑 → ( 1^st ‘ 𝑃 ) = 𝐶 )
3		fucofvalg.d	⊢ ( 𝜑 → ( 2^nd ‘ 𝑃 ) = 𝐷 )
4		fucofvalg.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
5		fucofvalg.o	⊢ ( 𝜑 → ( 𝑃 ∘_F 𝐸 ) = ⚬ )
6		fucofvalg.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
7		df-fuco	⊢ ∘_F = ( 𝑝 ∈ V , 𝑒 ∈ V ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( ( 𝑑 Func 𝑒 ) × ( 𝑐 Func 𝑑 ) ) / 𝑤 ⦌ ⟨ ( ∘_func ↾ 𝑤 ) , ( 𝑢 ∈ 𝑤 , 𝑣 ∈ 𝑤 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )
8	7	a1i	⊢ ( 𝜑 → ∘_F = ( 𝑝 ∈ V , 𝑒 ∈ V ↦ ⦋ ( 1^st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( ( 𝑑 Func 𝑒 ) × ( 𝑐 Func 𝑑 ) ) / 𝑤 ⦌ ⟨ ( ∘_func ↾ 𝑤 ) , ( 𝑢 ∈ 𝑤 , 𝑣 ∈ 𝑤 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ ) )
9		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) → ( 1^st ‘ 𝑝 ) ∈ V )
10		simprl	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) → 𝑝 = 𝑃 )
11	10	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) → ( 1^st ‘ 𝑝 ) = ( 1^st ‘ 𝑃 ) )
12	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) → ( 1^st ‘ 𝑃 ) = 𝐶 )
13	11 12	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) → ( 1^st ‘ 𝑝 ) = 𝐶 )
14		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ 𝑝 ) ∈ V )
15		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → 𝑝 = 𝑃 )
16	15	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ 𝑝 ) = ( 2^nd ‘ 𝑃 ) )
17	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ 𝑃 ) = 𝐷 )
18	16 17	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ( 2^nd ‘ 𝑝 ) = 𝐷 )
19		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
20		simpllr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) )
21	20	simprd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑒 = 𝐸 )
22	19 21	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑑 Func 𝑒 ) = ( 𝐷 Func 𝐸 ) )
23		simplr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑐 = 𝐶 )
24	23 19	oveq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝑐 Func 𝑑 ) = ( 𝐶 Func 𝐷 ) )
25	22 24	xpeq12d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑑 Func 𝑒 ) × ( 𝑐 Func 𝑑 ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
26		ovexd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝐷 Func 𝐸 ) ∈ V )
27		ovexd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( 𝐶 Func 𝐷 ) ∈ V )
28	26 27	xpexd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) ∈ V )
29	25 28	eqeltrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑑 Func 𝑒 ) × ( 𝑐 Func 𝑑 ) ) ∈ V )
30	6	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
31	25 30	eqtr4d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ( ( 𝑑 Func 𝑒 ) × ( 𝑐 Func 𝑑 ) ) = 𝑊 )
32		simpr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → 𝑤 = 𝑊 )
33	32	reseq2d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( ∘_func ↾ 𝑤 ) = ( ∘_func ↾ 𝑊 ) )
34		simplr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → 𝑑 = 𝐷 )
35	21	adantr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → 𝑒 = 𝐸 )
36	34 35	oveq12d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( 𝑑 Nat 𝑒 ) = ( 𝐷 Nat 𝐸 ) )
37	36	oveqd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) = ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) )
38		simpllr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → 𝑐 = 𝐶 )
39	38 34	oveq12d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( 𝑐 Nat 𝑑 ) = ( 𝐶 Nat 𝐷 ) )
40	39	oveqd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) = ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) )
41	38	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
42	35	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( comp ‘ 𝑒 ) = ( comp ‘ 𝐸 ) )
43	42	oveqd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) = ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) )
44	43	oveqd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) = ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) )
45	41 44	mpteq12dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
46	37 40 45	mpoeq123dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
47	46	csbeq2dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
48	47	csbeq2dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
49	48	csbeq2dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
50	49	csbeq2dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
51	50	csbeq2dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
52	32 32 51	mpoeq123dv	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ( 𝑢 ∈ 𝑤 , 𝑣 ∈ 𝑤 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) = ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
53	33 52	opeq12d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑤 = 𝑊 ) → ⟨ ( ∘_func ↾ 𝑤 ) , ( 𝑢 ∈ 𝑤 , 𝑣 ∈ 𝑤 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ = ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )
54	29 31 53	csbied2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) ∧ 𝑑 = 𝐷 ) → ⦋ ( ( 𝑑 Func 𝑒 ) × ( 𝑐 Func 𝑑 ) ) / 𝑤 ⦌ ⟨ ( ∘_func ↾ 𝑤 ) , ( 𝑢 ∈ 𝑤 , 𝑣 ∈ 𝑤 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ = ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )
55	14 18 54	csbied2	⊢ ( ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) ∧ 𝑐 = 𝐶 ) → ⦋ ( 2^nd ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( ( 𝑑 Func 𝑒 ) × ( 𝑐 Func 𝑑 ) ) / 𝑤 ⦌ ⟨ ( ∘_func ↾ 𝑤 ) , ( 𝑢 ∈ 𝑤 , 𝑣 ∈ 𝑤 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ = ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )
56	9 13 55	csbied2	⊢ ( ( 𝜑 ∧ ( 𝑝 = 𝑃 ∧ 𝑒 = 𝐸 ) ) → ⦋ ( 1^st ‘ 𝑝 ) / 𝑐 ⦌ ⦋ ( 2^nd ‘ 𝑝 ) / 𝑑 ⦌ ⦋ ( ( 𝑑 Func 𝑒 ) × ( 𝑐 Func 𝑑 ) ) / 𝑤 ⦌ ⟨ ( ∘_func ↾ 𝑤 ) , ( 𝑢 ∈ 𝑤 , 𝑣 ∈ 𝑤 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝑑 Nat 𝑒 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝑐 Nat 𝑑 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝑒 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ = ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )
57	1	elexd	⊢ ( 𝜑 → 𝑃 ∈ V )
58	4	elexd	⊢ ( 𝜑 → 𝐸 ∈ V )
59		opex	⊢ ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ ∈ V
60	59	a1i	⊢ ( 𝜑 → ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ ∈ V )
61	8 56 57 58 60	ovmpod	⊢ ( 𝜑 → ( 𝑃 ∘_F 𝐸 ) = ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )
62	5 61	eqtr3d	⊢ ( 𝜑 → ⚬ = ⟨ ( ∘_func ↾ 𝑊 ) , ( 𝑢 ∈ 𝑊 , 𝑣 ∈ 𝑊 ↦ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) / 𝑓 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) / 𝑘 ⦌ ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) ⟩ )

Metamath Proof Explorer

Theorem fucofvalg

Proof