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

Theorem catrid 17727
Description: Right identity property of an identity arrow. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
catidcl.b 𝐵 = (Base‘𝐶)
catidcl.h 𝐻 = (Hom ‘𝐶)
catidcl.i 1 = (Id‘𝐶)
catidcl.c (𝜑𝐶 ∈ Cat)
catidcl.x (𝜑𝑋𝐵)
catlid.o · = (comp‘𝐶)
catlid.y (𝜑𝑌𝐵)
catlid.f (𝜑𝐹 ∈ (𝑋𝐻𝑌))
Assertion
Ref Expression
catrid (𝜑 → (𝐹(⟨𝑋, 𝑋· 𝑌)( 1𝑋)) = 𝐹)

Proof of Theorem catrid
Dummy variables 𝑓 𝑔 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 7438 . . 3 (𝑓 = 𝐹 → (𝑓(⟨𝑋, 𝑋· 𝑌)( 1𝑋)) = (𝐹(⟨𝑋, 𝑋· 𝑌)( 1𝑋)))
2 id 22 . . 3 (𝑓 = 𝐹𝑓 = 𝐹)
31, 2eqeq12d 2753 . 2 (𝑓 = 𝐹 → ((𝑓(⟨𝑋, 𝑋· 𝑌)( 1𝑋)) = 𝑓 ↔ (𝐹(⟨𝑋, 𝑋· 𝑌)( 1𝑋)) = 𝐹))
4 oveq2 7439 . . . 4 (𝑦 = 𝑌 → (𝑋𝐻𝑦) = (𝑋𝐻𝑌))
5 oveq2 7439 . . . . . 6 (𝑦 = 𝑌 → (⟨𝑋, 𝑋· 𝑦) = (⟨𝑋, 𝑋· 𝑌))
65oveqd 7448 . . . . 5 (𝑦 = 𝑌 → (𝑓(⟨𝑋, 𝑋· 𝑦)( 1𝑋)) = (𝑓(⟨𝑋, 𝑋· 𝑌)( 1𝑋)))
76eqeq1d 2739 . . . 4 (𝑦 = 𝑌 → ((𝑓(⟨𝑋, 𝑋· 𝑦)( 1𝑋)) = 𝑓 ↔ (𝑓(⟨𝑋, 𝑋· 𝑌)( 1𝑋)) = 𝑓))
84, 7raleqbidv 3346 . . 3 (𝑦 = 𝑌 → (∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)( 1𝑋)) = 𝑓 ↔ ∀𝑓 ∈ (𝑋𝐻𝑌)(𝑓(⟨𝑋, 𝑋· 𝑌)( 1𝑋)) = 𝑓))
9 simpr 484 . . . . . . . 8 ((∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓) → ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)
109ralimi 3083 . . . . . . 7 (∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓) → ∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)
1110a1i 11 . . . . . 6 (𝑔 ∈ (𝑋𝐻𝑋) → (∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓) → ∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓))
1211ss2rabi 4077 . . . . 5 {𝑔 ∈ (𝑋𝐻𝑋) ∣ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)} ⊆ {𝑔 ∈ (𝑋𝐻𝑋) ∣ ∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓}
13 catidcl.b . . . . . . 7 𝐵 = (Base‘𝐶)
14 catidcl.h . . . . . . 7 𝐻 = (Hom ‘𝐶)
15 catlid.o . . . . . . 7 · = (comp‘𝐶)
16 catidcl.c . . . . . . 7 (𝜑𝐶 ∈ Cat)
17 catidcl.i . . . . . . 7 1 = (Id‘𝐶)
18 catidcl.x . . . . . . 7 (𝜑𝑋𝐵)
1913, 14, 15, 16, 17, 18cidval 17720 . . . . . 6 (𝜑 → ( 1𝑋) = (𝑔 ∈ (𝑋𝐻𝑋)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)))
2013, 14, 15, 16, 18catideu 17718 . . . . . . 7 (𝜑 → ∃!𝑔 ∈ (𝑋𝐻𝑋)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓))
21 riotacl2 7404 . . . . . . 7 (∃!𝑔 ∈ (𝑋𝐻𝑋)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓) → (𝑔 ∈ (𝑋𝐻𝑋)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)) ∈ {𝑔 ∈ (𝑋𝐻𝑋) ∣ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)})
2220, 21syl 17 . . . . . 6 (𝜑 → (𝑔 ∈ (𝑋𝐻𝑋)∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)) ∈ {𝑔 ∈ (𝑋𝐻𝑋) ∣ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)})
2319, 22eqeltrd 2841 . . . . 5 (𝜑 → ( 1𝑋) ∈ {𝑔 ∈ (𝑋𝐻𝑋) ∣ ∀𝑦𝐵 (∀𝑓 ∈ (𝑦𝐻𝑋)(𝑔(⟨𝑦, 𝑋· 𝑋)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓)})
2412, 23sselid 3981 . . . 4 (𝜑 → ( 1𝑋) ∈ {𝑔 ∈ (𝑋𝐻𝑋) ∣ ∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓})
25 oveq2 7439 . . . . . . . 8 (𝑔 = ( 1𝑋) → (𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = (𝑓(⟨𝑋, 𝑋· 𝑦)( 1𝑋)))
2625eqeq1d 2739 . . . . . . 7 (𝑔 = ( 1𝑋) → ((𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑋, 𝑋· 𝑦)( 1𝑋)) = 𝑓))
27262ralbidv 3221 . . . . . 6 (𝑔 = ( 1𝑋) → (∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓 ↔ ∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)( 1𝑋)) = 𝑓))
2827elrab 3692 . . . . 5 (( 1𝑋) ∈ {𝑔 ∈ (𝑋𝐻𝑋) ∣ ∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓} ↔ (( 1𝑋) ∈ (𝑋𝐻𝑋) ∧ ∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)( 1𝑋)) = 𝑓))
2928simprbi 496 . . . 4 (( 1𝑋) ∈ {𝑔 ∈ (𝑋𝐻𝑋) ∣ ∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)𝑔) = 𝑓} → ∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)( 1𝑋)) = 𝑓)
3024, 29syl 17 . . 3 (𝜑 → ∀𝑦𝐵𝑓 ∈ (𝑋𝐻𝑦)(𝑓(⟨𝑋, 𝑋· 𝑦)( 1𝑋)) = 𝑓)
31 catlid.y . . 3 (𝜑𝑌𝐵)
328, 30, 31rspcdva 3623 . 2 (𝜑 → ∀𝑓 ∈ (𝑋𝐻𝑌)(𝑓(⟨𝑋, 𝑋· 𝑌)( 1𝑋)) = 𝑓)
33 catlid.f . 2 (𝜑𝐹 ∈ (𝑋𝐻𝑌))
343, 32, 33rspcdva 3623 1 (𝜑 → (𝐹(⟨𝑋, 𝑋· 𝑌)( 1𝑋)) = 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  wral 3061  ∃!wreu 3378  {crab 3436  cop 4632  cfv 6561  crio 7387  (class class class)co 7431  Basecbs 17247  Hom chom 17308  compcco 17309  Catccat 17707  Idccid 17708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-cat 17711  df-cid 17712
This theorem is referenced by:  oppccatid  17762  sectcan  17799  monsect  17827  invisoinvl  17834  rcaninv  17838  subccatid  17891  fucidcl  18013  fucrid  18015  invfuc  18022  arwrid  18118  xpccatid  18233  curf2cl  18276  curfuncf  18283  uncfcurf  18284  hofcl  18304  yonedalem3b  18324  bj-endmnd  37319  endmndlem  48904  idepi  48909  upeu2lem  48911  fucorid  49057  precofvalALT  49063
  Copyright terms: Public domain W3C validator