Theorem fuco21 48991

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  Vcvv 3464  ⦋csb 3881  ⟨cop 4614   class class class wbr 5125   ↦ cmpt 5207   × cxp 5665  ‘cfv 6542  (class class class)co 7414   ∈ cmpo 7416  1^st c1st 7995  2^nd c2nd 7996  Basecbs 17230  compcco 17286  Catccat 17679   Func cfunc 17871   Nat cnat 17961   ∘_F cfuco 48971

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 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5261  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3773  df-csb 3882  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-iun 4975  df-br 5126  df-opab 5188  df-mpt 5208  df-id 5560  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7997  df-2nd 7998  df-func 17875  df-cofu 17877  df-fuco 48972

This theorem is referenced by:  fuco22  48994  fucof21  49002