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

Theorem idinv 17490
Description: The inverse of the identity is the identity. Example 3.13 of [Adamek] p. 28. (Contributed by AV, 9-Apr-2020.)
Hypotheses
Ref Expression
invid.b 𝐵 = (Base‘𝐶)
invid.i 𝐼 = (Id‘𝐶)
invid.c (𝜑𝐶 ∈ Cat)
invid.x (𝜑𝑋𝐵)
Assertion
Ref Expression
idinv (𝜑 → ((𝑋(Inv‘𝐶)𝑋)‘(𝐼𝑋)) = (𝐼𝑋))

Proof of Theorem idinv
StepHypRef Expression
1 invid.b . . 3 𝐵 = (Base‘𝐶)
2 eqid 2738 . . 3 (Inv‘𝐶) = (Inv‘𝐶)
3 invid.c . . 3 (𝜑𝐶 ∈ Cat)
4 invid.x . . 3 (𝜑𝑋𝐵)
51, 2, 3, 4, 4invfun 17465 . 2 (𝜑 → Fun (𝑋(Inv‘𝐶)𝑋))
6 invid.i . . 3 𝐼 = (Id‘𝐶)
71, 6, 3, 4invid 17488 . 2 (𝜑 → (𝐼𝑋)(𝑋(Inv‘𝐶)𝑋)(𝐼𝑋))
8 funbrfv 6814 . 2 (Fun (𝑋(Inv‘𝐶)𝑋) → ((𝐼𝑋)(𝑋(Inv‘𝐶)𝑋)(𝐼𝑋) → ((𝑋(Inv‘𝐶)𝑋)‘(𝐼𝑋)) = (𝐼𝑋)))
95, 7, 8sylc 65 1 (𝜑 → ((𝑋(Inv‘𝐶)𝑋)‘(𝐼𝑋)) = (𝐼𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wcel 2106   class class class wbr 5075  Fun wfun 6422  cfv 6428  (class class class)co 7269  Basecbs 16901  Catccat 17362  Idccid 17363  Invcinv 17446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5210  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7580
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3433  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4259  df-if 4462  df-pw 4537  df-sn 4564  df-pr 4566  df-op 4570  df-uni 4842  df-iun 4928  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5486  df-xp 5592  df-rel 5593  df-cnv 5594  df-co 5595  df-dm 5596  df-rn 5597  df-res 5598  df-ima 5599  df-iota 6386  df-fun 6430  df-fn 6431  df-f 6432  df-f1 6433  df-fo 6434  df-f1o 6435  df-fv 6436  df-riota 7226  df-ov 7272  df-oprab 7273  df-mpo 7274  df-1st 7822  df-2nd 7823  df-cat 17366  df-cid 17367  df-sect 17448  df-inv 17449
This theorem is referenced by:  invisoinvl  17491
  Copyright terms: Public domain W3C validator