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

Theorem curf1cl 17471
 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 2825 . . . 4 (Hom ‘𝐷) = (Hom ‘𝐷)
10 eqid 2825 . . . 4 (Id‘𝐶) = (Id‘𝐶)
111, 2, 3, 4, 5, 6, 7, 8, 9, 10curf1 17468 . . 3 (𝜑𝐾 = ⟨(𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
126fvexi 6680 . . . . . . 7 𝐵 ∈ V
1312mptex 6984 . . . . . 6 (𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)) ∈ V
1412, 12mpoex 7771 . . . . . 6 (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))) ∈ V
1513, 14op1std 7693 . . . . 5 (𝐾 = ⟨(𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (1st𝐾) = (𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)))
1611, 15syl 17 . . . 4 (𝜑 → (1st𝐾) = (𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)))
1713, 14op2ndd 7694 . . . . 5 (𝐾 = ⟨(𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩ → (2nd𝐾) = (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))))
1811, 17syl 17 . . . 4 (𝜑 → (2nd𝐾) = (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))))
1916, 18opeq12d 4809 . . 3 (𝜑 → ⟨(1st𝐾), (2nd𝐾)⟩ = ⟨(𝑦𝐵 ↦ (𝑋(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))⟩)
2011, 19eqtr4d 2863 . 2 (𝜑𝐾 = ⟨(1st𝐾), (2nd𝐾)⟩)
21 eqid 2825 . . . 4 (Base‘𝐸) = (Base‘𝐸)
22 eqid 2825 . . . 4 (Hom ‘𝐸) = (Hom ‘𝐸)
23 eqid 2825 . . . 4 (Id‘𝐷) = (Id‘𝐷)
24 eqid 2825 . . . 4 (Id‘𝐸) = (Id‘𝐸)
25 eqid 2825 . . . 4 (comp‘𝐷) = (comp‘𝐷)
26 eqid 2825 . . . 4 (comp‘𝐸) = (comp‘𝐸)
27 funcrcl 17126 . . . . . 6 (𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸) → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
285, 27syl 17 . . . . 5 (𝜑 → ((𝐶 ×c 𝐷) ∈ Cat ∧ 𝐸 ∈ Cat))
2928simprd 496 . . . 4 (𝜑𝐸 ∈ Cat)
30 eqid 2825 . . . . . . . . 9 (𝐶 ×c 𝐷) = (𝐶 ×c 𝐷)
3130, 2, 6xpcbas 17421 . . . . . . . 8 (𝐴 × 𝐵) = (Base‘(𝐶 ×c 𝐷))
32 relfunc 17125 . . . . . . . . 9 Rel ((𝐶 ×c 𝐷) Func 𝐸)
33 1st2ndbr 7735 . . . . . . . . 9 ((Rel ((𝐶 ×c 𝐷) Func 𝐸) ∧ 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸)) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
3432, 5, 33sylancr 587 . . . . . . . 8 (𝜑 → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
3531, 21, 34funcf1 17129 . . . . . . 7 (𝜑 → (1st𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
3635adantr 481 . . . . . 6 ((𝜑𝑦𝐵) → (1st𝐹):(𝐴 × 𝐵)⟶(Base‘𝐸))
377adantr 481 . . . . . 6 ((𝜑𝑦𝐵) → 𝑋𝐴)
38 simpr 485 . . . . . 6 ((𝜑𝑦𝐵) → 𝑦𝐵)
3936, 37, 38fovrnd 7313 . . . . 5 ((𝜑𝑦𝐵) → (𝑋(1st𝐹)𝑦) ∈ (Base‘𝐸))
4016, 39fmpt3d 6875 . . . 4 (𝜑 → (1st𝐾):𝐵⟶(Base‘𝐸))
41 eqid 2825 . . . . . 6 (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))) = (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))
42 ovex 7184 . . . . . . 7 (𝑦(Hom ‘𝐷)𝑧) ∈ V
4342mptex 6984 . . . . . 6 (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V
4441, 43fnmpoi 7762 . . . . 5 (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)
4518fneq1d 6442 . . . . 5 (𝜑 → ((2nd𝐾) Fn (𝐵 × 𝐵) ↔ (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))) Fn (𝐵 × 𝐵)))
4644, 45mpbiri 259 . . . 4 (𝜑 → (2nd𝐾) Fn (𝐵 × 𝐵))
4718oveqd 7168 . . . . . 6 (𝜑 → (𝑦(2nd𝐾)𝑧) = (𝑦(𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧))
4841ovmpt4g 7290 . . . . . . 7 ((𝑦𝐵𝑧𝐵 ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)) ∈ V) → (𝑦(𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))
4943, 48mp3an3 1443 . . . . . 6 ((𝑦𝐵𝑧𝐵) → (𝑦(𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))
5047, 49sylan9eq 2880 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(2nd𝐾)𝑧) = (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔)))
51 eqid 2825 . . . . . . . 8 (Hom ‘(𝐶 ×c 𝐷)) = (Hom ‘(𝐶 ×c 𝐷))
5234ad2antrr 722 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
537ad2antrr 722 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑋𝐴)
54 simplrl 773 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑦𝐵)
5553, 54opelxpd 5591 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
56 simplrr 774 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑧𝐵)
5753, 56opelxpd 5591 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
5831, 51, 22, 52, 55, 57funcf2 17131 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑋, 𝑧⟩)))
59 eqid 2825 . . . . . . . . 9 (Hom ‘𝐶) = (Hom ‘𝐶)
6030, 31, 59, 9, 51, 55, 57xpchom 17423 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = (((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩))))
613ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐶 ∈ Cat)
624ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐷 ∈ Cat)
635ad2antrr 722 . . . . . . . . . . 11 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
641, 2, 61, 62, 63, 6, 53, 8, 54curf11 17469 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st𝐾)‘𝑦) = (𝑋(1st𝐹)𝑦))
65 df-ov 7154 . . . . . . . . . 10 (𝑋(1st𝐹)𝑦) = ((1st𝐹)‘⟨𝑋, 𝑦⟩)
6664, 65syl6req 2877 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st𝐹)‘⟨𝑋, 𝑦⟩) = ((1st𝐾)‘𝑦))
671, 2, 61, 62, 63, 6, 53, 8, 56curf11 17469 . . . . . . . . . 10 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st𝐾)‘𝑧) = (𝑋(1st𝐹)𝑧))
68 df-ov 7154 . . . . . . . . . 10 (𝑋(1st𝐹)𝑧) = ((1st𝐹)‘⟨𝑋, 𝑧⟩)
6967, 68syl6req 2877 . . . . . . . . 9 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st𝐹)‘⟨𝑋, 𝑧⟩) = ((1st𝐾)‘𝑧))
7066, 69oveq12d 7169 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((1st𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑋, 𝑧⟩)) = (((1st𝐾)‘𝑦)(Hom ‘𝐸)((1st𝐾)‘𝑧)))
7160, 70feq23d 6505 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩):(⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩)⟶(((1st𝐹)‘⟨𝑋, 𝑦⟩)(Hom ‘𝐸)((1st𝐹)‘⟨𝑋, 𝑧⟩)) ↔ (⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st𝐾)‘𝑦)(Hom ‘𝐸)((1st𝐾)‘𝑧))))
7258, 71mpbid 233 . . . . . 6 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩):(((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) × ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))⟶(((1st𝐾)‘𝑦)(Hom ‘𝐸)((1st𝐾)‘𝑧)))
732, 59, 10, 61, 53catidcl 16946 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
74 op1stg 7695 . . . . . . . . 9 ((𝑋𝐴𝑦𝐵) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
7553, 54, 74syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑦⟩) = 𝑋)
76 op1stg 7695 . . . . . . . . 9 ((𝑋𝐴𝑧𝐵) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
7753, 56, 76syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (1st ‘⟨𝑋, 𝑧⟩) = 𝑋)
7875, 77oveq12d 7169 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)) = (𝑋(Hom ‘𝐶)𝑋))
7973, 78eleqtrrd 2920 . . . . . 6 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((Id‘𝐶)‘𝑋) ∈ ((1st ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐶)(1st ‘⟨𝑋, 𝑧⟩)))
80 simpr 485 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
81 op2ndg 7696 . . . . . . . . 9 ((𝑋𝐴𝑦𝐵) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
8253, 54, 81syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑦⟩) = 𝑦)
83 op2ndg 7696 . . . . . . . . 9 ((𝑋𝐴𝑧𝐵) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
8453, 56, 83syl2anc 584 . . . . . . . 8 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (2nd ‘⟨𝑋, 𝑧⟩) = 𝑧)
8582, 84oveq12d 7169 . . . . . . 7 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)) = (𝑦(Hom ‘𝐷)𝑧))
8680, 85eleqtrrd 2920 . . . . . 6 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → 𝑔 ∈ ((2nd ‘⟨𝑋, 𝑦⟩)(Hom ‘𝐷)(2nd ‘⟨𝑋, 𝑧⟩)))
8772, 79, 86fovrnd 7313 . . . . 5 (((𝜑 ∧ (𝑦𝐵𝑧𝐵)) ∧ 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧)) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔) ∈ (((1st𝐾)‘𝑦)(Hom ‘𝐸)((1st𝐾)‘𝑧)))
8850, 87fmpt3d 6875 . . . 4 ((𝜑 ∧ (𝑦𝐵𝑧𝐵)) → (𝑦(2nd𝐾)𝑧):(𝑦(Hom ‘𝐷)𝑧)⟶(((1st𝐾)‘𝑦)(Hom ‘𝐸)((1st𝐾)‘𝑧)))
893adantr 481 . . . . . . . . 9 ((𝜑𝑦𝐵) → 𝐶 ∈ Cat)
904adantr 481 . . . . . . . . 9 ((𝜑𝑦𝐵) → 𝐷 ∈ Cat)
91 eqid 2825 . . . . . . . . 9 (Id‘(𝐶 ×c 𝐷)) = (Id‘(𝐶 ×c 𝐷))
9230, 89, 90, 2, 6, 10, 23, 91, 37, 38xpcid 17432 . . . . . . . 8 ((𝜑𝑦𝐵) → ((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩) = ⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
9392fveq2d 6670 . . . . . . 7 ((𝜑𝑦𝐵) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩))
94 df-ov 7154 . . . . . . 7 (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)‘⟨((Id‘𝐶)‘𝑋), ((Id‘𝐷)‘𝑦)⟩)
9593, 94syl6eqr 2878 . . . . . 6 ((𝜑𝑦𝐵) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
9634adantr 481 . . . . . . 7 ((𝜑𝑦𝐵) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
97 opelxpi 5590 . . . . . . . 8 ((𝑋𝐴𝑦𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
987, 97sylan 580 . . . . . . 7 ((𝜑𝑦𝐵) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
9931, 91, 24, 96, 98funcid 17133 . . . . . 6 ((𝜑𝑦𝐵) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)‘((Id‘(𝐶 ×c 𝐷))‘⟨𝑋, 𝑦⟩)) = ((Id‘𝐸)‘((1st𝐹)‘⟨𝑋, 𝑦⟩)))
10095, 99eqtr3d 2862 . . . . 5 ((𝜑𝑦𝐵) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st𝐹)‘⟨𝑋, 𝑦⟩)))
1015adantr 481 . . . . . 6 ((𝜑𝑦𝐵) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
1026, 9, 23, 90, 38catidcl 16946 . . . . . 6 ((𝜑𝑦𝐵) → ((Id‘𝐷)‘𝑦) ∈ (𝑦(Hom ‘𝐷)𝑦))
1031, 2, 89, 90, 101, 6, 37, 8, 38, 9, 10, 38, 102curf12 17470 . . . . 5 ((𝜑𝑦𝐵) → ((𝑦(2nd𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑦⟩)((Id‘𝐷)‘𝑦)))
1041, 2, 89, 90, 101, 6, 37, 8, 38curf11 17469 . . . . . . 7 ((𝜑𝑦𝐵) → ((1st𝐾)‘𝑦) = (𝑋(1st𝐹)𝑦))
105104, 65syl6eq 2876 . . . . . 6 ((𝜑𝑦𝐵) → ((1st𝐾)‘𝑦) = ((1st𝐹)‘⟨𝑋, 𝑦⟩))
106105fveq2d 6670 . . . . 5 ((𝜑𝑦𝐵) → ((Id‘𝐸)‘((1st𝐾)‘𝑦)) = ((Id‘𝐸)‘((1st𝐹)‘⟨𝑋, 𝑦⟩)))
107100, 103, 1063eqtr4d 2870 . . . 4 ((𝜑𝑦𝐵) → ((𝑦(2nd𝐾)𝑦)‘((Id‘𝐷)‘𝑦)) = ((Id‘𝐸)‘((1st𝐾)‘𝑦)))
10873ad2ant1 1127 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑋𝐴)
109 simp21 1200 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑦𝐵)
110 simp22 1201 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑧𝐵)
111 eqid 2825 . . . . . . . . . 10 (comp‘𝐶) = (comp‘𝐶)
112 eqid 2825 . . . . . . . . . 10 (comp‘(𝐶 ×c 𝐷)) = (comp‘(𝐶 ×c 𝐷))
113 simp23 1202 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑤𝐵)
11433ad2ant1 1127 . . . . . . . . . . 11 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐶 ∈ Cat)
1152, 59, 10, 114, 108catidcl 16946 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((Id‘𝐶)‘𝑋) ∈ (𝑋(Hom ‘𝐶)𝑋))
116 simp3l 1195 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧))
117 simp3r 1196 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ∈ (𝑧(Hom ‘𝐷)𝑤))
11830, 2, 6, 59, 9, 108, 109, 108, 110, 111, 25, 112, 108, 113, 115, 116, 115, 117xpcco2 17430 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
1192, 59, 10, 114, 108, 111, 108, 115catlid 16947 . . . . . . . . . 10 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)) = ((Id‘𝐶)‘𝑋))
120119opeq1d 4807 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨(((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑋⟩(comp‘𝐶)𝑋)((Id‘𝐶)‘𝑋)), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩ = ⟨((Id‘𝐶)‘𝑋), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
121118, 120eqtrd 2860 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((Id‘𝐶)‘𝑋), ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩) = ⟨((Id‘𝐶)‘𝑋), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
122121fveq2d 6670 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩))
123 df-ov 7154 . . . . . . 7 (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)⟩)
124122, 123syl6eqr 2878 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)))
125343ad2ant1 1127 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (1st𝐹)((𝐶 ×c 𝐷) Func 𝐸)(2nd𝐹))
126108, 109opelxpd 5591 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑦⟩ ∈ (𝐴 × 𝐵))
127108, 110opelxpd 5591 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑧⟩ ∈ (𝐴 × 𝐵))
128108, 113opelxpd 5591 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨𝑋, 𝑤⟩ ∈ (𝐴 × 𝐵))
129115, 116opelxpd 5591 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
13030, 2, 6, 59, 9, 108, 109, 108, 110, 51xpchom2 17429 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑦(Hom ‘𝐷)𝑧)))
131129, 130eleqtrrd 2920 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), 𝑔⟩ ∈ (⟨𝑋, 𝑦⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑧⟩))
132115, 117opelxpd 5591 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ⟩ ∈ ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
13330, 2, 6, 59, 9, 108, 110, 108, 113, 51xpchom2 17429 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩) = ((𝑋(Hom ‘𝐶)𝑋) × (𝑧(Hom ‘𝐷)𝑤)))
134132, 133eleqtrrd 2920 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((Id‘𝐶)‘𝑋), ⟩ ∈ (⟨𝑋, 𝑧⟩(Hom ‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩))
13531, 51, 112, 26, 125, 126, 127, 128, 131, 134funcco 17134 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘(⟨((Id‘𝐶)‘𝑋), ⟩(⟨⟨𝑋, 𝑦⟩, ⟨𝑋, 𝑧⟩⟩(comp‘(𝐶 ×c 𝐷))⟨𝑋, 𝑤⟩)⟨((Id‘𝐶)‘𝑋), 𝑔⟩)) = (((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑦⟩), ((1st𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
136124, 135eqtr3d 2862 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑦⟩), ((1st𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
13743ad2ant1 1127 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐷 ∈ Cat)
13853ad2ant1 1127 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → 𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
1396, 9, 25, 137, 109, 110, 113, 116, 117catcocl 16949 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔) ∈ (𝑦(Hom ‘𝐷)𝑤))
1401, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 113, 139curf12 17470 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd𝐾)𝑤)‘((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑤⟩)((⟨𝑦, 𝑧⟩(comp‘𝐷)𝑤)𝑔)))
1411, 2, 114, 137, 138, 6, 108, 8, 109curf11 17469 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑦) = (𝑋(1st𝐹)𝑦))
142141, 65syl6eq 2876 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑦) = ((1st𝐹)‘⟨𝑋, 𝑦⟩))
1431, 2, 114, 137, 138, 6, 108, 8, 110curf11 17469 . . . . . . . . 9 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑧) = (𝑋(1st𝐹)𝑧))
144143, 68syl6eq 2876 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑧) = ((1st𝐹)‘⟨𝑋, 𝑧⟩))
145142, 144opeq12d 4809 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ⟨((1st𝐾)‘𝑦), ((1st𝐾)‘𝑧)⟩ = ⟨((1st𝐹)‘⟨𝑋, 𝑦⟩), ((1st𝐹)‘⟨𝑋, 𝑧⟩)⟩)
1461, 2, 114, 137, 138, 6, 108, 8, 113curf11 17469 . . . . . . . 8 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑤) = (𝑋(1st𝐹)𝑤))
147 df-ov 7154 . . . . . . . 8 (𝑋(1st𝐹)𝑤) = ((1st𝐹)‘⟨𝑋, 𝑤⟩)
148146, 147syl6eq 2876 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((1st𝐾)‘𝑤) = ((1st𝐹)‘⟨𝑋, 𝑤⟩))
149145, 148oveq12d 7169 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (⟨((1st𝐾)‘𝑦), ((1st𝐾)‘𝑧)⟩(comp‘𝐸)((1st𝐾)‘𝑤)) = (⟨((1st𝐹)‘⟨𝑋, 𝑦⟩), ((1st𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑋, 𝑤⟩)))
1501, 2, 114, 137, 138, 6, 108, 8, 110, 9, 10, 113, 117curf12 17470 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd𝐾)𝑤)‘) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)))
151 df-ov 7154 . . . . . . 7 (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)) = ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ⟩)
152150, 151syl6eq 2876 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑧(2nd𝐾)𝑤)‘) = ((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ⟩))
1531, 2, 114, 137, 138, 6, 108, 8, 109, 9, 10, 110, 116curf12 17470 . . . . . . 7 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd𝐾)𝑧)‘𝑔) = (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔))
154 df-ov 7154 . . . . . . 7 (((Id‘𝐶)‘𝑋)(⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)𝑔) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)
155153, 154syl6eq 2876 . . . . . 6 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → ((𝑦(2nd𝐾)𝑧)‘𝑔) = ((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩))
156149, 152, 155oveq123d 7172 . . . . 5 ((𝜑 ∧ (𝑦𝐵𝑧𝐵𝑤𝐵) ∧ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ∧ ∈ (𝑧(Hom ‘𝐷)𝑤))) → (((𝑧(2nd𝐾)𝑤)‘)(⟨((1st𝐾)‘𝑦), ((1st𝐾)‘𝑧)⟩(comp‘𝐸)((1st𝐾)‘𝑤))((𝑦(2nd𝐾)𝑧)‘𝑔)) = (((⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑋, 𝑤⟩)‘⟨((Id‘𝐶)‘𝑋), ⟩)(⟨((1st𝐹)‘⟨𝑋, 𝑦⟩), ((1st𝐹)‘⟨𝑋, 𝑧⟩)⟩(comp‘𝐸)((1st𝐹)‘⟨𝑋, 𝑤⟩))((⟨𝑋, 𝑦⟩(2nd𝐹)⟨𝑋, 𝑧⟩)‘⟨((Id‘𝐶)‘𝑋), 𝑔⟩)))
157136, 140, 1563eqtr4d 2870 . . . 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 17128 . . 3 (𝜑 → (1st𝐾)(𝐷 Func 𝐸)(2nd𝐾))
159 df-br 5063 . . 3 ((1st𝐾)(𝐷 Func 𝐸)(2nd𝐾) ↔ ⟨(1st𝐾), (2nd𝐾)⟩ ∈ (𝐷 Func 𝐸))
160158, 159sylib 219 . 2 (𝜑 → ⟨(1st𝐾), (2nd𝐾)⟩ ∈ (𝐷 Func 𝐸))
16120, 160eqeltrd 2917 1 (𝜑𝐾 ∈ (𝐷 Func 𝐸))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107  Vcvv 3499  ⟨cop 4569   class class class wbr 5062   ↦ cmpt 5142   × cxp 5551  Rel wrel 5558   Fn wfn 6346  ⟶wf 6347  ‘cfv 6351  (class class class)co 7151   ∈ cmpo 7153  1st c1st 7681  2nd c2nd 7682  Basecbs 16476  Hom chom 16569  compcco 16570  Catccat 16928  Idccid 16929   Func cfunc 17117   ×c cxpc 17411   curryF ccurf 17453 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-oadd 8100  df-er 8282  df-map 8401  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-fz 12886  df-struct 16478  df-ndx 16479  df-slot 16480  df-base 16482  df-hom 16582  df-cco 16583  df-cat 16932  df-cid 16933  df-func 17121  df-xpc 17415  df-curf 17457 This theorem is referenced by:  curf2cl  17474  curfcl  17475
 Copyright terms: Public domain W3C validator