fuco21

Description: The morphism part of the functor composition bifunctor. (Contributed by Zhi Wang, 29-Sep-2025)

	Ref	Expression
Hypotheses	fuco11.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fuco11.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
	fuco11.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
	fuco11.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
	fuco21.m	⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 )
	fuco21.r	⊢ ( 𝜑 → 𝑅 ( 𝐷 Func 𝐸 ) 𝑆 )
	fuco21.v	⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
Assertion	fuco21	⊢ ( 𝜑 → ( 𝑈 𝑃 𝑉 ) = ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fuco11.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		fuco11.f	⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
3		fuco11.k	⊢ ( 𝜑 → 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 )
4		fuco11.u	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
5		fuco21.m	⊢ ( 𝜑 → 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 )
6		fuco21.r	⊢ ( 𝜑 → 𝑅 ( 𝐷 Func 𝐸 ) 𝑆 )
7		fuco21.v	⊢ ( 𝜑 → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
8	2	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
9	3	funcrcl2	⊢ ( 𝜑 → 𝐷 ∈ Cat )
10	3	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )
11		eqidd	⊢ ( 𝜑 → ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
12	8 9 10 1 11	fuco2	⊢ ( 𝜑 → 𝑃 = ( 𝑢 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 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 ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ) )
13		fvexd	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) ∈ V )
14		simprl	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → 𝑢 = 𝑈 )
15	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
16	14 15	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → 𝑢 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
17	16	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) = ( 1^st ‘ ( 2^nd ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) )
19		opex	⊢ ⟨ 𝐾 , 𝐿 ⟩ ∈ V
20		opex	⊢ ⟨ 𝐹 , 𝐺 ⟩ ∈ V
21	19 20	op2nd	⊢ ( 2^nd ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) = ⟨ 𝐹 , 𝐺 ⟩
22	21	fveq2i	⊢ ( 1^st ‘ ( 2^nd ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) = ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ )
23		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
24	23	brrelex1i	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → 𝐹 ∈ V )
25	2 24	syl	⊢ ( 𝜑 → 𝐹 ∈ V )
26	23	brrelex2i	⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 → 𝐺 ∈ V )
27	2 26	syl	⊢ ( 𝜑 → 𝐺 ∈ V )
28		op1stg	⊢ ( ( 𝐹 ∈ V ∧ 𝐺 ∈ V ) → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
29	25 27 28	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
30	22 29	eqtrid	⊢ ( 𝜑 → ( 1^st ‘ ( 2^nd ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) = 𝐹 )
31	30	adantr	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → ( 1^st ‘ ( 2^nd ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) = 𝐹 )
32	18 31	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → ( 1^st ‘ ( 2^nd ‘ 𝑢 ) ) = 𝐹 )
33		fvexd	⊢ ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) ∈ V )
34	14	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → 𝑢 = 𝑈 )
35	15	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
36	34 35	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → 𝑢 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
37	36	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 1^st ‘ 𝑢 ) = ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) )
38	37	fveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) )
39	19 20	op1st	⊢ ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) = ⟨ 𝐾 , 𝐿 ⟩
40	39	fveq2i	⊢ ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) = ( 1^st ‘ ⟨ 𝐾 , 𝐿 ⟩ )
41		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
42	41	brrelex1i	⊢ ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 → 𝐾 ∈ V )
43	3 42	syl	⊢ ( 𝜑 → 𝐾 ∈ V )
44	41	brrelex2i	⊢ ( 𝐾 ( 𝐷 Func 𝐸 ) 𝐿 → 𝐿 ∈ V )
45	3 44	syl	⊢ ( 𝜑 → 𝐿 ∈ V )
46		op1stg	⊢ ( ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) → ( 1^st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
47	43 45 46	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐾 )
48	40 47	eqtrid	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) = 𝐾 )
49	48	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) = 𝐾 )
50	38 49	eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ( 1^st ‘ ( 1^st ‘ 𝑢 ) ) = 𝐾 )
51		fvexd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) → ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) ∈ V )
52	34	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) → 𝑢 = 𝑈 )
53	35	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) → 𝑈 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
54	52 53	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) → 𝑢 = ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ )
55	54	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) → ( 1^st ‘ 𝑢 ) = ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) )
56	55	fveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) → ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) = ( 2^nd ‘ ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) )
57	39	fveq2i	⊢ ( 2^nd ‘ ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) = ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ )
58		op2ndg	⊢ ( ( 𝐾 ∈ V ∧ 𝐿 ∈ V ) → ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
59	43 45 58	syl2anc	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝐾 , 𝐿 ⟩ ) = 𝐿 )
60	57 59	eqtrid	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) = 𝐿 )
61	60	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) → ( 2^nd ‘ ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) ) = 𝐿 )
62	56 61	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) → ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) = 𝐿 )
63		fvexd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) → ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) ∈ V )
64		simp-4r	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) → ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) )
65	64	simprd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) → 𝑣 = 𝑉 )
66	7	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
67	65 66	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) → 𝑣 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
68	67	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) → ( 2^nd ‘ 𝑣 ) = ( 2^nd ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) )
69	68	fveq2d	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) → ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) = ( 1^st ‘ ( 2^nd ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) ) )
70		opex	⊢ ⟨ 𝑅 , 𝑆 ⟩ ∈ V
71		opex	⊢ ⟨ 𝑀 , 𝑁 ⟩ ∈ V
72	70 71	op2nd	⊢ ( 2^nd ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) = ⟨ 𝑀 , 𝑁 ⟩
73	72	fveq2i	⊢ ( 1^st ‘ ( 2^nd ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) ) = ( 1^st ‘ ⟨ 𝑀 , 𝑁 ⟩ )
74	23	brrelex1i	⊢ ( 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 → 𝑀 ∈ V )
75	5 74	syl	⊢ ( 𝜑 → 𝑀 ∈ V )
76	23	brrelex2i	⊢ ( 𝑀 ( 𝐶 Func 𝐷 ) 𝑁 → 𝑁 ∈ V )
77	5 76	syl	⊢ ( 𝜑 → 𝑁 ∈ V )
78		op1stg	⊢ ( ( 𝑀 ∈ V ∧ 𝑁 ∈ V ) → ( 1^st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
79	75 77 78	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑀 , 𝑁 ⟩ ) = 𝑀 )
80	73 79	eqtrid	⊢ ( 𝜑 → ( 1^st ‘ ( 2^nd ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) ) = 𝑀 )
81	80	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) → ( 1^st ‘ ( 2^nd ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) ) = 𝑀 )
82	69 81	eqtrd	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) → ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) = 𝑀 )
83		fvexd	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) → ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) ∈ V )
84	65	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) → 𝑣 = 𝑉 )
85	66	adantr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) → 𝑉 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
86	84 85	eqtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) → 𝑣 = ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ )
87	86	fveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) → ( 1^st ‘ 𝑣 ) = ( 1^st ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) )
88	87	fveq2d	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) → ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) ) )
89	70 71	op1st	⊢ ( 1^st ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) = ⟨ 𝑅 , 𝑆 ⟩
90	89	fveq2i	⊢ ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) ) = ( 1^st ‘ ⟨ 𝑅 , 𝑆 ⟩ )
91	41	brrelex1i	⊢ ( 𝑅 ( 𝐷 Func 𝐸 ) 𝑆 → 𝑅 ∈ V )
92	6 91	syl	⊢ ( 𝜑 → 𝑅 ∈ V )
93	41	brrelex2i	⊢ ( 𝑅 ( 𝐷 Func 𝐸 ) 𝑆 → 𝑆 ∈ V )
94	6 93	syl	⊢ ( 𝜑 → 𝑆 ∈ V )
95		op1stg	⊢ ( ( 𝑅 ∈ V ∧ 𝑆 ∈ V ) → ( 1^st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑅 )
96	92 94 95	syl2anc	⊢ ( 𝜑 → ( 1^st ‘ ⟨ 𝑅 , 𝑆 ⟩ ) = 𝑅 )
97	90 96	eqtrid	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) ) = 𝑅 )
98	97	ad5antr	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) → ( 1^st ‘ ( 1^st ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) ) = 𝑅 )
99	88 98	eqtrd	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) → ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) = 𝑅 )
100	55	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 1^st ‘ 𝑢 ) = ( 1^st ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) )
101	100 39	eqtrdi	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 1^st ‘ 𝑢 ) = ⟨ 𝐾 , 𝐿 ⟩ )
102	87	adantr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 1^st ‘ 𝑣 ) = ( 1^st ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) )
103	102 89	eqtrdi	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 1^st ‘ 𝑣 ) = ⟨ 𝑅 , 𝑆 ⟩ )
104	101 103	oveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) = ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) )
105	17	ad5antr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 2^nd ‘ 𝑢 ) = ( 2^nd ‘ ⟨ ⟨ 𝐾 , 𝐿 ⟩ , ⟨ 𝐹 , 𝐺 ⟩ ⟩ ) )
106	105 21	eqtrdi	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 2^nd ‘ 𝑢 ) = ⟨ 𝐹 , 𝐺 ⟩ )
107	68	ad2antrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 2^nd ‘ 𝑣 ) = ( 2^nd ‘ ⟨ ⟨ 𝑅 , 𝑆 ⟩ , ⟨ 𝑀 , 𝑁 ⟩ ⟩ ) )
108	107 72	eqtrdi	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 2^nd ‘ 𝑣 ) = ⟨ 𝑀 , 𝑁 ⟩ )
109	106 108	oveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) = ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) )
110		simp-4r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → 𝑘 = 𝐾 )
111		simp-5r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → 𝑓 = 𝐹 )
112	111	fveq1d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 𝑓 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
113	110 112	fveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) = ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) )
114		simplr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → 𝑚 = 𝑀 )
115	114	fveq1d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 𝑚 ‘ 𝑥 ) = ( 𝑀 ‘ 𝑥 ) )
116	110 115	fveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) = ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) )
117	113 116	opeq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ = ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ )
118		simpr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → 𝑟 = 𝑅 )
119	118 115	fveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) = ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) )
120	117 119	oveq12d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) = ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) )
121	115	fveq2d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) = ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) )
122		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → 𝑙 = 𝐿 )
123	122 112 115	oveq123d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) )
124	123	fveq1d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) )
125	120 121 124	oveq123d	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) = ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) )
126	125	mpteq2dv	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) )
127	104 109 126	mpoeq123dv	⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) ∧ 𝑟 = 𝑅 ) → ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
128	83 99 127	csbied2	⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) ∧ 𝑚 = 𝑀 ) → ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
129	63 82 128	csbied2	⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) ∧ 𝑙 = 𝐿 ) → ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
130	51 62 129	csbied2	⊢ ( ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) ∧ 𝑘 = 𝐾 ) → ⦋ ( 2^nd ‘ ( 1^st ‘ 𝑢 ) ) / 𝑙 ⦌ ⦋ ( 1^st ‘ ( 2^nd ‘ 𝑣 ) ) / 𝑚 ⦌ ⦋ ( 1^st ‘ ( 1^st ‘ 𝑣 ) ) / 𝑟 ⦌ ( 𝑏 ∈ ( ( 1^st ‘ 𝑢 ) ( 𝐷 Nat 𝐸 ) ( 1^st ‘ 𝑣 ) ) , 𝑎 ∈ ( ( 2^nd ‘ 𝑢 ) ( 𝐶 Nat 𝐷 ) ( 2^nd ‘ 𝑣 ) ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑚 ‘ 𝑥 ) ) ( ⟨ ( 𝑘 ‘ ( 𝑓 ‘ 𝑥 ) ) , ( 𝑘 ‘ ( 𝑚 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
131	33 50 130	csbied2	⊢ ( ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) ∧ 𝑓 = 𝐹 ) → ⦋ ( 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 ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
132	13 32 131	csbied2	⊢ ( ( 𝜑 ∧ ( 𝑢 = 𝑈 ∧ 𝑣 = 𝑉 ) ) → ⦋ ( 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 ‘ 𝐸 ) ( 𝑟 ‘ ( 𝑚 ‘ 𝑥 ) ) ) ( ( ( 𝑓 ‘ 𝑥 ) 𝑙 ( 𝑚 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) = ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )
133	11 4 3 2	fuco2eld	⊢ ( 𝜑 → 𝑈 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
134	11 7 6 5	fuco2eld	⊢ ( 𝜑 → 𝑉 ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
135		ovex	⊢ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) ∈ V
136		ovex	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ∈ V
137	135 136	mpoex	⊢ ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V
138	137	a1i	⊢ ( 𝜑 → ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) ∈ V )
139	12 132 133 134 138	ovmpod	⊢ ( 𝜑 → ( 𝑈 𝑃 𝑉 ) = ( 𝑏 ∈ ( ⟨ 𝐾 , 𝐿 ⟩ ( 𝐷 Nat 𝐸 ) ⟨ 𝑅 , 𝑆 ⟩ ) , 𝑎 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ ( 𝐶 Nat 𝐷 ) ⟨ 𝑀 , 𝑁 ⟩ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑏 ‘ ( 𝑀 ‘ 𝑥 ) ) ( ⟨ ( 𝐾 ‘ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐾 ‘ ( 𝑀 ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( 𝑅 ‘ ( 𝑀 ‘ 𝑥 ) ) ) ( ( ( 𝐹 ‘ 𝑥 ) 𝐿 ( 𝑀 ‘ 𝑥 ) ) ‘ ( 𝑎 ‘ 𝑥 ) ) ) ) ) )

Metamath Proof Explorer

Theorem fuco21

Proof