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

Theorem curfval 17539
 Description: Value of the curry functor. (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
curfval.g 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
curfval.a 𝐴 = (Base‘𝐶)
curfval.c (𝜑𝐶 ∈ Cat)
curfval.d (𝜑𝐷 ∈ Cat)
curfval.f (𝜑𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
curfval.b 𝐵 = (Base‘𝐷)
curfval.j 𝐽 = (Hom ‘𝐷)
curfval.1 1 = (Id‘𝐶)
curfval.h 𝐻 = (Hom ‘𝐶)
curfval.i 𝐼 = (Id‘𝐷)
Assertion
Ref Expression
curfval (𝜑𝐺 = ⟨(𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))⟩)
Distinct variable groups:   𝑥,𝑔,𝑦,𝑧, 1   𝑥,𝐴,𝑦   𝐵,𝑔,𝑥,𝑦,𝑧   𝐶,𝑔,𝑥,𝑦,𝑧   𝐷,𝑔,𝑥,𝑦,𝑧   𝑔,𝐻,𝑦,𝑧   𝜑,𝑔,𝑥,𝑦,𝑧   𝑔,𝐸,𝑦,𝑧   𝑔,𝐽,𝑥   𝑔,𝐹,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐴(𝑧,𝑔)   𝐸(𝑥)   𝐺(𝑥,𝑦,𝑧,𝑔)   𝐻(𝑥)   𝐼(𝑥,𝑦,𝑧,𝑔)   𝐽(𝑦,𝑧)

Proof of Theorem curfval
Dummy variables 𝑐 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 curfval.g . 2 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
2 df-curf 17530 . . . 4 curryF = (𝑒 ∈ V, 𝑓 ∈ V ↦ (1st𝑒) / 𝑐(2nd𝑒) / 𝑑⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩)
32a1i 11 . . 3 (𝜑 → curryF = (𝑒 ∈ V, 𝑓 ∈ V ↦ (1st𝑒) / 𝑐(2nd𝑒) / 𝑑⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩))
4 fvexd 6673 . . . 4 ((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) → (1st𝑒) ∈ V)
5 simprl 770 . . . . . 6 ((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) → 𝑒 = ⟨𝐶, 𝐷⟩)
65fveq2d 6662 . . . . 5 ((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) → (1st𝑒) = (1st ‘⟨𝐶, 𝐷⟩))
7 curfval.c . . . . . . 7 (𝜑𝐶 ∈ Cat)
8 curfval.d . . . . . . 7 (𝜑𝐷 ∈ Cat)
9 op1stg 7705 . . . . . . 7 ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (1st ‘⟨𝐶, 𝐷⟩) = 𝐶)
107, 8, 9syl2anc 587 . . . . . 6 (𝜑 → (1st ‘⟨𝐶, 𝐷⟩) = 𝐶)
1110adantr 484 . . . . 5 ((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) → (1st ‘⟨𝐶, 𝐷⟩) = 𝐶)
126, 11eqtrd 2793 . . . 4 ((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) → (1st𝑒) = 𝐶)
13 fvexd 6673 . . . . 5 (((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) → (2nd𝑒) ∈ V)
145adantr 484 . . . . . . 7 (((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) → 𝑒 = ⟨𝐶, 𝐷⟩)
1514fveq2d 6662 . . . . . 6 (((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) → (2nd𝑒) = (2nd ‘⟨𝐶, 𝐷⟩))
16 op2ndg 7706 . . . . . . . 8 ((𝐶 ∈ Cat ∧ 𝐷 ∈ Cat) → (2nd ‘⟨𝐶, 𝐷⟩) = 𝐷)
177, 8, 16syl2anc 587 . . . . . . 7 (𝜑 → (2nd ‘⟨𝐶, 𝐷⟩) = 𝐷)
1817ad2antrr 725 . . . . . 6 (((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) → (2nd ‘⟨𝐶, 𝐷⟩) = 𝐷)
1915, 18eqtrd 2793 . . . . 5 (((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) → (2nd𝑒) = 𝐷)
20 simplr 768 . . . . . . . . 9 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → 𝑐 = 𝐶)
2120fveq2d 6662 . . . . . . . 8 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Base‘𝑐) = (Base‘𝐶))
22 curfval.a . . . . . . . 8 𝐴 = (Base‘𝐶)
2321, 22eqtr4di 2811 . . . . . . 7 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Base‘𝑐) = 𝐴)
24 simpr 488 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → 𝑑 = 𝐷)
2524fveq2d 6662 . . . . . . . . . 10 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Base‘𝑑) = (Base‘𝐷))
26 curfval.b . . . . . . . . . 10 𝐵 = (Base‘𝐷)
2725, 26eqtr4di 2811 . . . . . . . . 9 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Base‘𝑑) = 𝐵)
28 simprr 772 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) → 𝑓 = 𝐹)
2928ad2antrr 725 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → 𝑓 = 𝐹)
3029fveq2d 6662 . . . . . . . . . 10 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (1st𝑓) = (1st𝐹))
3130oveqd 7167 . . . . . . . . 9 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑥(1st𝑓)𝑦) = (𝑥(1st𝐹)𝑦))
3227, 31mpteq12dv 5117 . . . . . . . 8 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)) = (𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)))
3324fveq2d 6662 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Hom ‘𝑑) = (Hom ‘𝐷))
34 curfval.j . . . . . . . . . . . 12 𝐽 = (Hom ‘𝐷)
3533, 34eqtr4di 2811 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Hom ‘𝑑) = 𝐽)
3635oveqd 7167 . . . . . . . . . 10 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑦(Hom ‘𝑑)𝑧) = (𝑦𝐽𝑧))
3729fveq2d 6662 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (2nd𝑓) = (2nd𝐹))
3837oveqd 7167 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩) = (⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩))
3920fveq2d 6662 . . . . . . . . . . . . 13 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Id‘𝑐) = (Id‘𝐶))
40 curfval.1 . . . . . . . . . . . . 13 1 = (Id‘𝐶)
4139, 40eqtr4di 2811 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Id‘𝑐) = 1 )
4241fveq1d 6660 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → ((Id‘𝑐)‘𝑥) = ( 1𝑥))
43 eqidd 2759 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → 𝑔 = 𝑔)
4438, 42, 43oveq123d 7171 . . . . . . . . . 10 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔) = (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔))
4536, 44mpteq12dv 5117 . . . . . . . . 9 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)) = (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))
4627, 27, 45mpoeq123dv 7223 . . . . . . . 8 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔))) = (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔))))
4732, 46opeq12d 4771 . . . . . . 7 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩ = ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩)
4823, 47mpteq12dv 5117 . . . . . 6 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩) = (𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩))
4920fveq2d 6662 . . . . . . . . . 10 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Hom ‘𝑐) = (Hom ‘𝐶))
50 curfval.h . . . . . . . . . 10 𝐻 = (Hom ‘𝐶)
5149, 50eqtr4di 2811 . . . . . . . . 9 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Hom ‘𝑐) = 𝐻)
5251oveqd 7167 . . . . . . . 8 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑥(Hom ‘𝑐)𝑦) = (𝑥𝐻𝑦))
5337oveqd 7167 . . . . . . . . . 10 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩) = (⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩))
5424fveq2d 6662 . . . . . . . . . . . 12 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Id‘𝑑) = (Id‘𝐷))
55 curfval.i . . . . . . . . . . . 12 𝐼 = (Id‘𝐷)
5654, 55eqtr4di 2811 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (Id‘𝑑) = 𝐼)
5756fveq1d 6660 . . . . . . . . . 10 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → ((Id‘𝑑)‘𝑧) = (𝐼𝑧))
5853, 43, 57oveq123d 7171 . . . . . . . . 9 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)) = (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))
5927, 58mpteq12dv 5117 . . . . . . . 8 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧))) = (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧))))
6052, 59mpteq12dv 5117 . . . . . . 7 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))) = (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))
6123, 23, 60mpoeq123dv 7223 . . . . . 6 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧))))) = (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧))))))
6248, 61opeq12d 4771 . . . . 5 ((((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) ∧ 𝑑 = 𝐷) → ⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩ = ⟨(𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))⟩)
6313, 19, 62csbied2 3842 . . . 4 (((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) ∧ 𝑐 = 𝐶) → (2nd𝑒) / 𝑑⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩ = ⟨(𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))⟩)
644, 12, 63csbied2 3842 . . 3 ((𝜑 ∧ (𝑒 = ⟨𝐶, 𝐷⟩ ∧ 𝑓 = 𝐹)) → (1st𝑒) / 𝑐(2nd𝑒) / 𝑑⟨(𝑥 ∈ (Base‘𝑐) ↦ ⟨(𝑦 ∈ (Base‘𝑑) ↦ (𝑥(1st𝑓)𝑦)), (𝑦 ∈ (Base‘𝑑), 𝑧 ∈ (Base‘𝑑) ↦ (𝑔 ∈ (𝑦(Hom ‘𝑑)𝑧) ↦ (((Id‘𝑐)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝑓)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥 ∈ (Base‘𝑐), 𝑦 ∈ (Base‘𝑐) ↦ (𝑔 ∈ (𝑥(Hom ‘𝑐)𝑦) ↦ (𝑧 ∈ (Base‘𝑑) ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝑓)⟨𝑦, 𝑧⟩)((Id‘𝑑)‘𝑧)))))⟩ = ⟨(𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))⟩)
65 opex 5324 . . . 4 𝐶, 𝐷⟩ ∈ V
6665a1i 11 . . 3 (𝜑 → ⟨𝐶, 𝐷⟩ ∈ V)
67 curfval.f . . . 4 (𝜑𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
6867elexd 3430 . . 3 (𝜑𝐹 ∈ V)
69 opex 5324 . . . 4 ⟨(𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))⟩ ∈ V
7069a1i 11 . . 3 (𝜑 → ⟨(𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))⟩ ∈ V)
713, 64, 66, 68, 70ovmpod 7297 . 2 (𝜑 → (⟨𝐶, 𝐷⟩ curryF 𝐹) = ⟨(𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))⟩)
721, 71syl5eq 2805 1 (𝜑𝐺 = ⟨(𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦𝐽𝑧) ↦ (( 1𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  Vcvv 3409  ⦋csb 3805  ⟨cop 4528   ↦ cmpt 5112  ‘cfv 6335  (class class class)co 7150   ∈ cmpo 7152  1st c1st 7691  2nd c2nd 7692  Basecbs 16541  Hom chom 16634  Catccat 16993  Idccid 16994   Func cfunc 17183   ×c cxpc 17484   curryF ccurf 17526 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-iota 6294  df-fun 6337  df-fv 6343  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7693  df-2nd 7694  df-curf 17530 This theorem is referenced by:  curf1fval  17540  curf2  17545  curfcl  17548  curfpropd  17549  curfuncf  17554
 Copyright terms: Public domain W3C validator