MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  curf1cl Structured version   Visualization version   GIF version

Theorem curf1cl 18158
Description: The partially evaluated curry functor is a functor. (Contributed by Mario Carneiro, 13-Jan-2017.)
Hypotheses
Ref Expression
curfval.g 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
curfval.a 𝐴 = (Base‘𝐶)
curfval.c (𝜑𝐶 ∈ Cat)
curfval.d (𝜑𝐷 ∈ Cat)
curfval.f (𝜑𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
curfval.b 𝐵 = (Base‘𝐷)
curf1.x (𝜑𝑋𝐴)
curf1.k 𝐾 = ((1st𝐺)‘𝑋)
Assertion
Ref Expression
curf1cl (𝜑𝐾 ∈ (𝐷 Func 𝐸))

Proof of Theorem curf1cl
Dummy variables 𝑔 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 curfval.g . . . 4 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
2 curfval.a . . . 4 𝐴 = (Base‘𝐶)
3 curfval.c . . . 4 (𝜑𝐶 ∈ Cat)
4 curfval.d . . . 4 (𝜑𝐷 ∈ Cat)
5 curfval.f . . . 4 (𝜑𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
6 curfval.b . . . 4 𝐵 = (Base‘𝐷)
7 curf1.x . . . 4 (𝜑𝑋𝐴)
8 curf1.k . . . 4 𝐾 = ((1st𝐺)‘𝑋)
9 eqid 2731 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
10 eqid 2731 . . . 4 (Id‘𝐶) = (Id‘𝐶)
111, 2, 3, 4, 5, 6, 7, 8, 9, 10curf1 18155 . . 3 (𝜑𝐾 = ⟨(𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
126fvexi 6887 . . . . . . 7 𝐵 ∈ V
1312mptex 7204 . . . . . 6 (𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)) ∈ V
1412, 12mpoex 8043 . . . . . 6 (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))) ∈ V
1513, 14op1std 7962 . . . . 5 (𝐾 = ⟨(𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (1st𝐾) = (𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)))
1611, 15syl 17 . . . 4 (𝜑 → (1st𝐾) = (𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)))
1713, 14op2ndd 7963 . . . . 5 (𝐾 = ⟨(𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (2nd𝐾) = (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))))
1811, 17syl 17 . . . 4 (𝜑 → (2nd𝐾) = (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))))
1916, 18opeq12d 4869 . . 3 (𝜑 → ⟨(1st𝐾), (2nd𝐾)⟩ = ⟨(𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
2011, 19eqtr4d 2774 . 2 (𝜑𝐾 = ⟨(1st𝐾), (2nd𝐾)⟩)
21 eqid 2731 . . . 4 (Base‘𝐸) = (Base‘𝐸)
22 eqid 2731 . . . 4 (Hom ‘𝐸) = (Hom ‘𝐸)
23 eqid 2731 . . . 4 (Id‘𝐷) = (Id‘𝐷)
24 eqid 2731 . . . 4 (Id‘𝐸) = (Id‘𝐸)
25 eqid 2731 . . . 4 (comp‘𝐷) = (comp‘𝐷)
26 eqid 2731 . . . 4 (comp‘𝐸) = (comp‘𝐸)
27 funcrcl 17790 . . . . . 6 (𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸) → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
285, 27syl 17 . . . . 5 (𝜑 → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
2928simprd 496 . . . 4 (𝜑𝐸 ∈ Cat)
30 eqid 2731 . . . . . . . . 9 (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
3130, 2, 6xpcbas 18107 . . . . . . . 8 (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
32 relfunc 17789 . . . . . . . . 9 Rel ((𝐶 ×c 𝐷) Func 𝐸)
33 1st2ndbr 8005 . . . . . . . . 9 ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
3432, 5, 33sylancr 587 . . . . . . . 8 (𝜑 → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
3531, 21, 34funcf1 17793 . . . . . . 7 (𝜑 → (1st𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
3635adantr 481 . . . . . 6 ((𝜑𝑦𝐵) → (1st𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
377adantr 481 . . . . . 6 ((𝜑𝑦𝐵) → 𝑋𝐴)
38 simpr 485 . . . . . 6 ((𝜑𝑦𝐵) → 𝑦𝐵)
3936, 37, 38fovcdmd 7557 . . . . 5 ((𝜑𝑦𝐵) → (𝑋(1st𝐹)𝑦) ∈ (Base‘𝐸))
4016, 39fmpt3d 7095 . . . 4 (𝜑 → (1st𝐾):𝐵⟶(Base‘𝐸))
41 eqid 2731 . . . . . 6 (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))) = (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))
42 ovex 7421 . . . . . . 7 (𝑦(Hom ‘𝐷)𝑧) ∈ V
4342mptex 7204 . . . . . 6 (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V
4441, 43fnmpoi 8033 . . . . 5 (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)
4518fneq1d 6626 . . . . 5 (𝜑 → ((2nd𝐾) Fn (𝐵 × 𝐵) ↔ (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)))
4644, 45mpbiri 257 . . . 4 (𝜑 → (2nd𝐾) Fn (𝐵 × 𝐵))
4718oveqd 7405 . . . . . 6 (𝜑 → (𝑦(2nd𝐾)𝑧) = (𝑦(𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧))
4841ovmpt4g 7533 . . . . . . 7 ((𝑦𝐵𝑧𝐵 ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V) → (𝑦(𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))
4943, 48mp3an3 1450 . . . . . 6 ((𝑦𝐵𝑧𝐵) → (𝑦(𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))
5047, 49sylan9eq 2791 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(2nd𝐾)𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))
51 eqid 2731 . . . . . . . 8 (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
5234ad2antrr 724 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
537ad2antrr 724 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑋𝐴)
54 simplrl 775 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦𝐵)
5553, 54opelxpd 5702 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
56 simplrr 776 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑧𝐵)
5753, 56opelxpd 5702 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
5831, 51, 22, 52, 55, 57funcf2 17795 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑋, 𝑧⟩)))
59 eqid 2731 . . . . . . . . 9 (Hom ‘𝐶) = (Hom ‘𝐶)
6030, 31, 59, 9, 51, 55, 57xpchom 18109 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = (((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩))))
613ad2antrr 724 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐶 ∈ Cat)
624ad2antrr 724 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐷 ∈ Cat)
635ad2antrr 724 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
641, 2, 61, 62, 63, 6, 53, 8, 54curf11 18156 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st𝐾)‘𝑦) = (𝑋(1st𝐹)𝑦))
65 df-ov 7391 . . . . . . . . . 10 (𝑋(1st𝐹)𝑦) = ((1st𝐹)‘⟨𝑋, 𝑦⟩)
6664, 65eqtr2di 2788 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st𝐹)‘⟨𝑋, 𝑦⟩) = ((1st𝐾)‘𝑦))
671, 2, 61, 62, 63, 6, 53, 8, 56curf11 18156 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st𝐾)‘𝑧) = (𝑋(1st𝐹)𝑧))
68 df-ov 7391 . . . . . . . . . 10 (𝑋(1st𝐹)𝑧) = ((1st𝐹)‘⟨𝑋, 𝑧⟩)
6967, 68eqtr2di 2788 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st𝐹)‘⟨𝑋, 𝑧⟩) = ((1st𝐾)‘𝑧))
7066, 69oveq12d 7406 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((1st𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑋, 𝑧⟩)) = (((1st𝐾)‘𝑦)(Hom ‘𝐸)((1st𝐾)‘𝑧)))
7160, 70feq23d 6694 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑋, 𝑧⟩)) ↔ (⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st𝐾)‘𝑦)(Hom ‘𝐸)((1st𝐾)‘𝑧))))
7258, 71mpbid 231 . . . . . 6 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st𝐾)‘𝑦)(Hom ‘𝐸)((1st𝐾)‘𝑧)))
732, 59, 10, 61, 53catidcl 17603 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
74 op1stg 7964 . . . . . . . . 9 ((𝑋𝐴𝑦𝐵) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
7553, 54, 74syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
76 op1stg 7964 . . . . . . . . 9 ((𝑋𝐴𝑧𝐵) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
7753, 56, 76syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
7875, 77oveq12d 7406 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) = (𝑋(Hom ‘𝐶)𝑋))
7973, 78eleqtrrd 2835 . . . . . 6 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)))
80 simpr 485 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
81 op2ndg 7965 . . . . . . . . 9 ((𝑋𝐴𝑦𝐵) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
8253, 54, 81syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
83 op2ndg 7965 . . . . . . . . 9 ((𝑋𝐴𝑧𝐵) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
8453, 56, 83syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
8582, 84oveq12d 7406 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)) = (𝑦(Hom ‘𝐷)𝑧))
8680, 85eleqtrrd 2835 . . . . . 6 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))
8772, 79, 86fovcdmd 7557 . . . . 5 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔) ∈ (((1st𝐾)‘𝑦)(Hom ‘𝐸)((1st𝐾)‘𝑧)))
8850, 87fmpt3d 7095 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(2nd𝐾)𝑧):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st𝐾)‘𝑦)(Hom ‘𝐸)((1st𝐾)‘𝑧)))
893adantr 481 . . . . . . . . 9 ((𝜑𝑦𝐵) → 𝐶 ∈ Cat)
904adantr 481 . . . . . . . . 9 ((𝜑𝑦𝐵) → 𝐷 ∈ Cat)
91 eqid 2731 . . . . . . . . 9 (Id‘(𝐶 ×c 𝐷)) = (Id‘(𝐶 ×c 𝐷))
9230, 89, 90, 2, 6, 10, 23, 91, 37, 38xpcid 18118 . . . . . . . 8 ((𝜑𝑦𝐵) → ((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩) = ⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
9392fveq2d 6877 . . . . . . 7 ((𝜑𝑦𝐵) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩))
94 df-ov 7391 . . . . . . 7 (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
9593, 94eqtr4di 2789 . . . . . 6 ((𝜑𝑦𝐵) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
9634adantr 481 . . . . . . 7 ((𝜑𝑦𝐵) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
97 opelxpi 5701 . . . . . . . 8 ((𝑋𝐴𝑦𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
987, 97sylan 580 . . . . . . 7 ((𝜑𝑦𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
9931, 91, 24, 96, 98funcid 17797 . . . . . 6 ((𝜑𝑦𝐵) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((Id‘𝐸)‘((1st𝐹)‘⟨𝑋, 𝑦⟩)))
10095, 99eqtr3d 2773 . . . . 5 ((𝜑𝑦𝐵) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st𝐹)‘⟨𝑋, 𝑦⟩)))
1015adantr 481 . . . . . 6 ((𝜑𝑦𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
1026, 9, 23, 90, 38catidcl 17603 . . . . . 6 ((𝜑𝑦𝐵) → ((Id‘𝐷)‘𝑦) ∈ (𝑦(Hom ‘𝐷)𝑦))
1031, 2, 89, 90, 101, 6, 37, 8, 38, 9, 10, 38, 102curf12 18157 . . . . 5 ((𝜑𝑦𝐵) → ((𝑦(2nd𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
1041, 2, 89, 90, 101, 6, 37, 8, 38curf11 18156 . . . . . . 7 ((𝜑𝑦𝐵) → ((1st𝐾)‘𝑦) = (𝑋(1st𝐹)𝑦))
105104, 65eqtrdi 2787 . . . . . 6 ((𝜑𝑦𝐵) → ((1st𝐾)‘𝑦) = ((1st𝐹)‘⟨𝑋, 𝑦⟩))
106105fveq2d 6877 . . . . 5 ((𝜑𝑦𝐵) → ((Id‘𝐸)‘((1st𝐾)‘𝑦)) = ((Id‘𝐸)‘((1st𝐹)‘⟨𝑋, 𝑦⟩)))
107100, 103, 1063eqtr4d 2781 . . . 4 ((𝜑𝑦𝐵) → ((𝑦(2nd𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st𝐾)‘𝑦)))
10873ad2ant1 1133 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋𝐴)
109 simp21 1206 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑦𝐵)
110 simp22 1207 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧𝐵)
111 eqid 2731 . . . . . . . . . 10 (comp‘𝐶) = (comp‘𝐶)
112 eqid 2731 . . . . . . . . . 10 (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
113 simp23 1208 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤𝐵)
11433ad2ant1 1133 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
1152, 59, 10, 114, 108catidcl 17603 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
116 simp3l 1201 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
117 simp3r 1202 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ∈ (𝑧(Hom ‘𝐷)𝑤))
11830, 2, 6, 59, 9, 108, 109, 108, 110, 111, 25, 112, 108, 113, 115, 116, 115, 117xpcco2 18116 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
1192, 59, 10, 114, 108, 111, 108, 115catlid 17604 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)) = ((Id‘𝐶)‘𝑋))
120119opeq1d 4867 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩ = ⟨((Id‘𝐶)‘𝑋), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
121118, 120eqtrd 2771 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨((Id‘𝐶)‘𝑋), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
122121fveq2d 6877 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩))
123 df-ov 7391 . . . . . . 7 (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
124122, 123eqtr4di 2789 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)))
125343ad2ant1 1133 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
126108, 109opelxpd 5702 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
127108, 110opelxpd 5702 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
128108, 113opelxpd 5702 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
129115, 116opelxpd 5702 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
13030, 2, 6, 59, 9, 108, 109, 108, 110, 51xpchom2 18115 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
131129, 130eleqtrrd 2835 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩))
132115, 117opelxpd 5702 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
13330, 2, 6, 59, 9, 108, 110, 108, 113, 51xpchom2 18115 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
134132, 133eleqtrrd 2835 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
13531, 51, 112, 26, 125, 126, 127, 128, 131, 134funcco 17798 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = (((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑦⟩), ((1st𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
136124, 135eqtr3d 2773 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑦⟩), ((1st𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
13743ad2ant1 1133 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat)
13853ad2ant1 1133 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
1396, 9, 25, 137, 109, 110, 113, 116, 117catcocl 17606 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐷)𝑤))
1401, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 113, 139curf12 18157 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd𝐾)𝑤)‘((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)))
1411, 2, 114, 137, 138, 6, 108, 8, 109curf11 18156 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑦) = (𝑋(1st𝐹)𝑦))
142141, 65eqtrdi 2787 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑦) = ((1st𝐹)‘⟨𝑋, 𝑦⟩))
1431, 2, 114, 137, 138, 6, 108, 8, 110curf11 18156 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑧) = (𝑋(1st𝐹)𝑧))
144143, 68eqtrdi 2787 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑧) = ((1st𝐹)‘⟨𝑋, 𝑧⟩))
145142, 144opeq12d 4869 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st𝐾)‘𝑦), ((1st𝐾)‘𝑧)⟩ = ⟨((1st𝐹)‘⟨𝑋, 𝑦⟩), ((1st𝐹)‘⟨𝑋, 𝑧⟩)⟩)
1461, 2, 114, 137, 138, 6, 108, 8, 113curf11 18156 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑤) = (𝑋(1st𝐹)𝑤))
147 df-ov 7391 . . . . . . . 8 (𝑋(1st𝐹)𝑤) = ((1st𝐹)‘⟨𝑋, 𝑤⟩)
148146, 147eqtrdi 2787 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑤) = ((1st𝐹)‘⟨𝑋, 𝑤⟩))
149145, 148oveq12d 7406 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((1st𝐾)‘𝑦), ((1st𝐾)‘𝑧)⟩(comp‘𝐸)((1st𝐾)‘𝑤)) = (⟨((1st𝐹)‘⟨𝑋, 𝑦⟩), ((1st𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑋, 𝑤⟩)))
1501, 2, 114, 137, 138, 6, 108, 8, 110, 9, 10, 113, 117curf12 18157 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd𝐾)𝑤)‘) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)))
151 df-ov 7391 . . . . . . 7 (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)) = ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ⟩)
152150, 151eqtrdi 2787 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd𝐾)𝑤)‘) = ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ⟩))
1531, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 110, 116curf12 18157 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd𝐾)𝑧)‘𝑔) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))
154 df-ov 7391 . . . . . . 7 (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)
155153, 154eqtrdi 2787 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd𝐾)𝑧)‘𝑔) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩))
156149, 152, 155oveq123d 7409 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd𝐾)𝑤)‘)(⟨((1st𝐾)‘𝑦), ((1st𝐾)‘𝑧)⟩(comp‘𝐸)((1st𝐾)‘𝑤))((𝑦(2nd𝐾)𝑧)‘𝑔)) = (((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑦⟩), ((1st𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
157136, 140, 1563eqtr4d 2781 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd𝐾)𝑤)‘((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((𝑧(2nd𝐾)𝑤)‘)(⟨((1st𝐾)‘𝑦), ((1st𝐾)‘𝑧)⟩(comp‘𝐸)((1st𝐾)‘𝑤))((𝑦(2nd𝐾)𝑧)‘𝑔)))
1586, 21, 9, 22, 23, 24, 25, 26, 4, 29, 40, 46, 88, 107, 157isfuncd 17792 . . 3 (𝜑 → (1st𝐾)(𝐷 Func 𝐸)(2nd𝐾))
159 df-br 5137 . . 3 ((1st𝐾)(𝐷 Func 𝐸)(2nd𝐾) ↔ ⟨(1st𝐾), (2nd𝐾)⟩ ∈ (𝐷 Func 𝐸))
160158, 159sylib 217 . 2 (𝜑 → ⟨(1st𝐾), (2nd𝐾)⟩ ∈ (𝐷 Func 𝐸))
16120, 160eqeltrd 2832 1 (𝜑𝐾 ∈ (𝐷 Func 𝐸))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  Vcvv 3469  cop 4623   class class class wbr 5136  cmpt 5219   × cxp 5662  Rel wrel 5669   Fn wfn 6522  wf 6523  cfv 6527  (class class class)co 7388  cmpo 7390  1st c1st 7950  2nd c2nd 7951  Basecbs 17121  Hom chom 17185  compcco 17186  Catccat 17585  Idccid 17586   Func cfunc 17781   ×c cxpc 18097   curryF ccurf 18140
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5273  ax-sep 5287  ax-nul 5294  ax-pow 5351  ax-pr 5415  ax-un 7703  ax-cnex 11143  ax-resscn 11144  ax-1cn 11145  ax-icn 11146  ax-addcl 11147  ax-addrcl 11148  ax-mulcl 11149  ax-mulrcl 11150  ax-mulcom 11151  ax-addass 11152  ax-mulass 11153  ax-distr 11154  ax-i2m1 11155  ax-1ne0 11156  ax-1rid 11157  ax-rnegex 11158  ax-rrecex 11159  ax-cnre 11160  ax-pre-lttri 11161  ax-pre-lttrn 11162  ax-pre-ltadd 11163  ax-pre-mulgt0 11164
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3374  df-reu 3375  df-rab 3429  df-v 3471  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3958  df-nul 4314  df-if 4518  df-pw 4593  df-sn 4618  df-pr 4620  df-tp 4622  df-op 4624  df-uni 4897  df-iun 4987  df-br 5137  df-opab 5199  df-mpt 5220  df-tr 5254  df-id 5562  df-eprel 5568  df-po 5576  df-so 5577  df-fr 5619  df-we 5621  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6284  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-riota 7344  df-ov 7391  df-oprab 7392  df-mpo 7393  df-om 7834  df-1st 7952  df-2nd 7953  df-frecs 8243  df-wrecs 8274  df-recs 8348  df-rdg 8387  df-1o 8443  df-er 8681  df-map 8800  df-ixp 8870  df-en 8918  df-dom 8919  df-sdom 8920  df-fin 8921  df-pnf 11227  df-mnf 11228  df-xr 11229  df-ltxr 11230  df-le 11231  df-sub 11423  df-neg 11424  df-nn 12190  df-2 12252  df-3 12253  df-4 12254  df-5 12255  df-6 12256  df-7 12257  df-8 12258  df-9 12259  df-n0 12450  df-z 12536  df-dec 12655  df-uz 12800  df-fz 13462  df-struct 17057  df-slot 17092  df-ndx 17104  df-base 17122  df-hom 17198  df-cco 17199  df-cat 17589  df-cid 17590  df-func 17785  df-xpc 18101  df-curf 18144
This theorem is referenced by:  curf2cl  18161  curfcl  18162
  Copyright terms: Public domain W3C validator