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

Theorem curf2 17975
Description: Value of the curry functor at a morphism. (Contributed by Mario Carneiro, 13-Jan-2017.)
Hypotheses
Ref Expression
curf2.g 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
curf2.a 𝐴 = (Base‘𝐶)
curf2.c (𝜑𝐶 ∈ Cat)
curf2.d (𝜑𝐷 ∈ Cat)
curf2.f (𝜑𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
curf2.b 𝐵 = (Base‘𝐷)
curf2.h 𝐻 = (Hom ‘𝐶)
curf2.i 𝐼 = (Id‘𝐷)
curf2.x (𝜑𝑋𝐴)
curf2.y (𝜑𝑌𝐴)
curf2.k (𝜑𝐾 ∈ (𝑋𝐻𝑌))
curf2.l 𝐿 = ((𝑋(2nd𝐺)𝑌)‘𝐾)
Assertion
Ref Expression
curf2 (𝜑𝐿 = (𝑧𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧))))
Distinct variable groups:   𝑧,𝐶   𝑧,𝐹   𝑧,𝐻   𝑧,𝐿   𝑧,𝐸   𝑧,𝐺   𝑧,𝐼   𝜑,𝑧   𝑧,𝐵   𝑧,𝐷   𝑧,𝑋   𝑧,𝐾   𝑧,𝑌
Allowed substitution hint:   𝐴(𝑧)

Proof of Theorem curf2
Dummy variables 𝑥 𝑦 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 curf2.l . 2 𝐿 = ((𝑋(2nd𝐺)𝑌)‘𝐾)
2 curf2.g . . . . 5 𝐺 = (⟨𝐶, 𝐷⟩ curryF 𝐹)
3 curf2.a . . . . 5 𝐴 = (Base‘𝐶)
4 curf2.c . . . . 5 (𝜑𝐶 ∈ Cat)
5 curf2.d . . . . 5 (𝜑𝐷 ∈ Cat)
6 curf2.f . . . . 5 (𝜑𝐹 ∈ ((𝐶 ×c 𝐷) Func 𝐸))
7 curf2.b . . . . 5 𝐵 = (Base‘𝐷)
8 eqid 2733 . . . . 5 (Hom ‘𝐷) = (Hom ‘𝐷)
9 eqid 2733 . . . . 5 (Id‘𝐶) = (Id‘𝐶)
10 curf2.h . . . . 5 𝐻 = (Hom ‘𝐶)
11 curf2.i . . . . 5 𝐼 = (Id‘𝐷)
122, 3, 4, 5, 6, 7, 8, 9, 10, 11curfval 17969 . . . 4 (𝜑𝐺 = ⟨(𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))⟩)
133fvexi 6806 . . . . . 6 𝐴 ∈ V
1413mptex 7119 . . . . 5 (𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩) ∈ V
1513, 13mpoex 7940 . . . . 5 (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧))))) ∈ V
1614, 15op2ndd 7862 . . . 4 (𝐺 = ⟨(𝑥𝐴 ↦ ⟨(𝑦𝐵 ↦ (𝑥(1st𝐹)𝑦)), (𝑦𝐵, 𝑧𝐵 ↦ (𝑔 ∈ (𝑦(Hom ‘𝐷)𝑧) ↦ (((Id‘𝐶)‘𝑥)(⟨𝑥, 𝑦⟩(2nd𝐹)⟨𝑥, 𝑧⟩)𝑔)))⟩), (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))))⟩ → (2nd𝐺) = (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧))))))
1712, 16syl 17 . . 3 (𝜑 → (2nd𝐺) = (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧))))))
18 curf2.x . . . 4 (𝜑𝑋𝐴)
19 curf2.y . . . . 5 (𝜑𝑌𝐴)
2019adantr 480 . . . 4 ((𝜑𝑥 = 𝑋) → 𝑌𝐴)
21 ovex 7328 . . . . . 6 (𝑥𝐻𝑦) ∈ V
2221mptex 7119 . . . . 5 (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))) ∈ V
2322a1i 11 . . . 4 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))) ∈ V)
24 curf2.k . . . . . . 7 (𝜑𝐾 ∈ (𝑋𝐻𝑌))
2524adantr 480 . . . . . 6 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → 𝐾 ∈ (𝑋𝐻𝑌))
26 simprl 767 . . . . . . 7 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → 𝑥 = 𝑋)
27 simprr 769 . . . . . . 7 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → 𝑦 = 𝑌)
2826, 27oveq12d 7313 . . . . . 6 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → (𝑥𝐻𝑦) = (𝑋𝐻𝑌))
2925, 28eleqtrrd 2837 . . . . 5 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → 𝐾 ∈ (𝑥𝐻𝑦))
307fvexi 6806 . . . . . . 7 𝐵 ∈ V
3130mptex 7119 . . . . . 6 (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧))) ∈ V
3231a1i 11 . . . . 5 (((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧))) ∈ V)
33 simplrl 773 . . . . . . . . 9 (((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑥 = 𝑋)
3433opeq1d 4812 . . . . . . . 8 (((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → ⟨𝑥, 𝑧⟩ = ⟨𝑋, 𝑧⟩)
35 simplrr 774 . . . . . . . . 9 (((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑦 = 𝑌)
3635opeq1d 4812 . . . . . . . 8 (((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → ⟨𝑦, 𝑧⟩ = ⟨𝑌, 𝑧⟩)
3734, 36oveq12d 7313 . . . . . . 7 (((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩) = (⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩))
38 simpr 484 . . . . . . 7 (((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → 𝑔 = 𝐾)
39 eqidd 2734 . . . . . . 7 (((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝐼𝑧) = (𝐼𝑧))
4037, 38, 39oveq123d 7316 . . . . . 6 (((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)) = (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧)))
4140mpteq2dv 5179 . . . . 5 (((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) ∧ 𝑔 = 𝐾) → (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧))) = (𝑧𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧))))
4229, 32, 41fvmptdv2 6913 . . . 4 ((𝜑 ∧ (𝑥 = 𝑋𝑦 = 𝑌)) → ((𝑋(2nd𝐺)𝑌) = (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧)))) → ((𝑋(2nd𝐺)𝑌)‘𝐾) = (𝑧𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧)))))
4318, 20, 23, 42ovmpodv 7450 . . 3 (𝜑 → ((2nd𝐺) = (𝑥𝐴, 𝑦𝐴 ↦ (𝑔 ∈ (𝑥𝐻𝑦) ↦ (𝑧𝐵 ↦ (𝑔(⟨𝑥, 𝑧⟩(2nd𝐹)⟨𝑦, 𝑧⟩)(𝐼𝑧))))) → ((𝑋(2nd𝐺)𝑌)‘𝐾) = (𝑧𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧)))))
4417, 43mpd 15 . 2 (𝜑 → ((𝑋(2nd𝐺)𝑌)‘𝐾) = (𝑧𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧))))
451, 44eqtrid 2785 1 (𝜑𝐿 = (𝑧𝐵 ↦ (𝐾(⟨𝑋, 𝑧⟩(2nd𝐹)⟨𝑌, 𝑧⟩)(𝐼𝑧))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2101  Vcvv 3434  cop 4570  cmpt 5160  cfv 6447  (class class class)co 7295  cmpo 7297  1st c1st 7849  2nd c2nd 7850  Basecbs 16940  Hom chom 17001  Catccat 17401  Idccid 17402   Func cfunc 17597   ×c cxpc 17913   curryF ccurf 17956
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-rep 5212  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7608
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3223  df-rab 3224  df-v 3436  df-sbc 3719  df-csb 3835  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4260  df-if 4463  df-pw 4538  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-iun 4929  df-br 5078  df-opab 5140  df-mpt 5161  df-id 5491  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-iota 6399  df-fun 6449  df-fn 6450  df-f 6451  df-f1 6452  df-fo 6453  df-f1o 6454  df-fv 6455  df-ov 7298  df-oprab 7299  df-mpo 7300  df-1st 7851  df-2nd 7852  df-curf 17960
This theorem is referenced by:  curf2val  17976  curf2cl  17977  curfcl  17978  diag2  17991  curf2ndf  17993
  Copyright terms: Public domain W3C validator