Theorem fuco21 50551

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  Vcvv 3450  ⦋csb 3846  ⟨cop 4834   class class class wbr 5102   ↦ cmpt 5185   × cxp 5648  ‘cfv 6538  (class class class)co 7420   ∈ cmpo 7422  1^st c1st 7999  2^nd c2nd 8000  Basecbs 17392  compcco 17445  Catccat 17843   Func cfunc 18034   Nat cnat 18124   ∘_F cfuco 50531

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-func 18038  df-cofu 18040  df-fuco 50532

This theorem is used by:  fuco22  50554  fucof21  50562