Theorem fuco21 48905

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

Hypotheses

Ref	Expression
fuco11.o	⊢ (𝜑 → (⟨𝐶, 𝐷⟩ ∘F 𝐸) = ⟨𝑂, 𝑃⟩)
fuco11.f	⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺)
fuco11.k	⊢ (𝜑 → 𝐾(𝐷 Func 𝐸)𝐿)
fuco11.u	⊢ (𝜑 → 𝑈 = ⟨⟨𝐾, 𝐿⟩, ⟨𝐹, 𝐺⟩⟩)
fuco21.m	⊢ (𝜑 → 𝑀(𝐶 Func 𝐷)𝑁)
fuco21.r	⊢ (𝜑 → 𝑅(𝐷 Func 𝐸)𝑆)
fuco21.v	⊢ (𝜑 → 𝑉 = ⟨⟨𝑅, 𝑆⟩, ⟨𝑀, 𝑁⟩⟩)

Assertion

Ref	Expression
fuco21	⊢ (𝜑 → (𝑈𝑃𝑉) = (𝑏 ∈ (⟨𝐾, 𝐿⟩(𝐷 Nat 𝐸)⟨𝑅, 𝑆⟩), 𝑎 ∈ (⟨𝐹, 𝐺⟩(𝐶 Nat 𝐷)⟨𝑀, 𝑁⟩) ↦ (𝑥 ∈ (Base‘𝐶) ↦ ((𝑏‘(𝑀‘𝑥))(⟨(𝐾‘(𝐹‘𝑥)), (𝐾‘(𝑀‘𝑥))⟩(comp‘𝐸)(𝑅‘(𝑀‘𝑥)))(((𝐹‘𝑥)𝐿(𝑀‘𝑥))‘(𝑎‘𝑥))))))

Distinct variable groups:   𝐶,𝑎,𝑏,𝑥   𝐷,𝑎,𝑏,𝑥   𝐸,𝑎,𝑏,𝑥   𝐹,𝑎,𝑏,𝑥   𝐺,𝑎,𝑏   𝐾,𝑎,𝑏,𝑥   𝐿,𝑎,𝑏,𝑥   𝑀,𝑎,𝑏,𝑥   𝑁,𝑎,𝑏   𝑅,𝑎,𝑏,𝑥   𝑆,𝑎,𝑏   𝑈,𝑎,𝑏,𝑥   𝑉,𝑎,𝑏,𝑥   𝜑,𝑎,𝑏,𝑥

Allowed substitution hints:   𝑃(𝑥,𝑎,𝑏)   𝑆(𝑥)   𝐺(𝑥)   𝑁(𝑥)   𝑂(𝑥,𝑎,𝑏)

Proof of Theorem fuco21

Dummy variables 𝑓 𝑘 𝑙 𝑚 𝑟 𝑢 𝑣 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3481  ⦋csb 3911  ⟨cop 4640   class class class wbr 5151   ↦ cmpt 5234   × cxp 5691  ‘cfv 6569  (class class class)co 7438   ∈ cmpo 7440  1^st c1st 8020  2^nd c2nd 8021  Basecbs 17254  compcco 17319  Catccat 17718   Func cfunc 17914   Nat cnat 18005   ∘_F cfuco 48885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5288  ax-sep 5305  ax-nul 5315  ax-pow 5374  ax-pr 5441  ax-un 7761

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3483  df-sbc 3795  df-csb 3912  df-dif 3969  df-un 3971  df-in 3973  df-ss 3983  df-nul 4343  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-op 4641  df-uni 4916  df-iun 5001  df-br 5152  df-opab 5214  df-mpt 5235  df-id 5587  df-xp 5699  df-rel 5700  df-cnv 5701  df-co 5702  df-dm 5703  df-rn 5704  df-res 5705  df-ima 5706  df-iota 6522  df-fun 6571  df-fn 6572  df-f 6573  df-f1 6574  df-fo 6575  df-f1o 6576  df-fv 6577  df-ov 7441  df-oprab 7442  df-mpo 7443  df-1st 8022  df-2nd 8023  df-func 17918  df-cofu 17920  df-fuco 48886

This theorem is referenced by:  fuco22  48906  fucof21  48914