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

Theorem invfun 16514
Description: The inverse relation is a function, which is to say that every morphism has at most one inverse. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
invfval.b 𝐵 = (Base‘𝐶)
invfval.n 𝑁 = (Inv‘𝐶)
invfval.c (𝜑𝐶 ∈ Cat)
invfval.x (𝜑𝑋𝐵)
invfval.y (𝜑𝑌𝐵)
Assertion
Ref Expression
invfun (𝜑 → Fun (𝑋𝑁𝑌))

Proof of Theorem invfun
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 invfval.b . . . 4 𝐵 = (Base‘𝐶)
2 invfval.n . . . 4 𝑁 = (Inv‘𝐶)
3 invfval.c . . . 4 (𝜑𝐶 ∈ Cat)
4 invfval.x . . . 4 (𝜑𝑋𝐵)
5 invfval.y . . . 4 (𝜑𝑌𝐵)
6 eqid 2692 . . . 4 (Hom ‘𝐶) = (Hom ‘𝐶)
71, 2, 3, 4, 5, 6invss 16511 . . 3 (𝜑 → (𝑋𝑁𝑌) ⊆ ((𝑋(Hom ‘𝐶)𝑌) × (𝑌(Hom ‘𝐶)𝑋)))
8 relxp 5203 . . 3 Rel ((𝑋(Hom ‘𝐶)𝑌) × (𝑌(Hom ‘𝐶)𝑋))
9 relss 5283 . . 3 ((𝑋𝑁𝑌) ⊆ ((𝑋(Hom ‘𝐶)𝑌) × (𝑌(Hom ‘𝐶)𝑋)) → (Rel ((𝑋(Hom ‘𝐶)𝑌) × (𝑌(Hom ‘𝐶)𝑋)) → Rel (𝑋𝑁𝑌)))
107, 8, 9mpisyl 21 . 2 (𝜑 → Rel (𝑋𝑁𝑌))
11 eqid 2692 . . . . . 6 (Sect‘𝐶) = (Sect‘𝐶)
123adantr 472 . . . . . 6 ((𝜑 ∧ (𝑓(𝑋𝑁𝑌)𝑔𝑓(𝑋𝑁𝑌))) → 𝐶 ∈ Cat)
135adantr 472 . . . . . 6 ((𝜑 ∧ (𝑓(𝑋𝑁𝑌)𝑔𝑓(𝑋𝑁𝑌))) → 𝑌𝐵)
144adantr 472 . . . . . 6 ((𝜑 ∧ (𝑓(𝑋𝑁𝑌)𝑔𝑓(𝑋𝑁𝑌))) → 𝑋𝐵)
151, 2, 3, 4, 5, 11isinv 16510 . . . . . . . 8 (𝜑 → (𝑓(𝑋𝑁𝑌)𝑔 ↔ (𝑓(𝑋(Sect‘𝐶)𝑌)𝑔𝑔(𝑌(Sect‘𝐶)𝑋)𝑓)))
1615simplbda 655 . . . . . . 7 ((𝜑𝑓(𝑋𝑁𝑌)𝑔) → 𝑔(𝑌(Sect‘𝐶)𝑋)𝑓)
1716adantrr 755 . . . . . 6 ((𝜑 ∧ (𝑓(𝑋𝑁𝑌)𝑔𝑓(𝑋𝑁𝑌))) → 𝑔(𝑌(Sect‘𝐶)𝑋)𝑓)
181, 2, 3, 4, 5, 11isinv 16510 . . . . . . . 8 (𝜑 → (𝑓(𝑋𝑁𝑌) ↔ (𝑓(𝑋(Sect‘𝐶)𝑌)(𝑌(Sect‘𝐶)𝑋)𝑓)))
1918simprbda 654 . . . . . . 7 ((𝜑𝑓(𝑋𝑁𝑌)) → 𝑓(𝑋(Sect‘𝐶)𝑌))
2019adantrl 754 . . . . . 6 ((𝜑 ∧ (𝑓(𝑋𝑁𝑌)𝑔𝑓(𝑋𝑁𝑌))) → 𝑓(𝑋(Sect‘𝐶)𝑌))
211, 11, 12, 13, 14, 17, 20sectcan 16505 . . . . 5 ((𝜑 ∧ (𝑓(𝑋𝑁𝑌)𝑔𝑓(𝑋𝑁𝑌))) → 𝑔 = )
2221ex 449 . . . 4 (𝜑 → ((𝑓(𝑋𝑁𝑌)𝑔𝑓(𝑋𝑁𝑌)) → 𝑔 = ))
2322alrimiv 1936 . . 3 (𝜑 → ∀((𝑓(𝑋𝑁𝑌)𝑔𝑓(𝑋𝑁𝑌)) → 𝑔 = ))
2423alrimivv 1937 . 2 (𝜑 → ∀𝑓𝑔((𝑓(𝑋𝑁𝑌)𝑔𝑓(𝑋𝑁𝑌)) → 𝑔 = ))
25 dffun2 5979 . 2 (Fun (𝑋𝑁𝑌) ↔ (Rel (𝑋𝑁𝑌) ∧ ∀𝑓𝑔((𝑓(𝑋𝑁𝑌)𝑔𝑓(𝑋𝑁𝑌)) → 𝑔 = )))
2610, 24, 25sylanbrc 701 1 (𝜑 → Fun (𝑋𝑁𝑌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wal 1562   = wceq 1564  wcel 2071  wss 3648   class class class wbr 4728   × cxp 5184  Rel wrel 5191  Fun wfun 5963  cfv 5969  (class class class)co 6733  Basecbs 15948  Hom chom 16043  Catccat 16415  Sectcsect 16494  Invcinv 16495
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-8 2073  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-rep 4847  ax-sep 4857  ax-nul 4865  ax-pow 4916  ax-pr 4979  ax-un 7034
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-eu 2543  df-mo 2544  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ne 2865  df-ral 2987  df-rex 2988  df-reu 2989  df-rmo 2990  df-rab 2991  df-v 3274  df-sbc 3510  df-csb 3608  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-nul 3992  df-if 4163  df-pw 4236  df-sn 4254  df-pr 4256  df-op 4260  df-uni 4513  df-iun 4598  df-br 4729  df-opab 4789  df-mpt 4806  df-id 5096  df-xp 5192  df-rel 5193  df-cnv 5194  df-co 5195  df-dm 5196  df-rn 5197  df-res 5198  df-ima 5199  df-iota 5932  df-fun 5971  df-fn 5972  df-f 5973  df-f1 5974  df-fo 5975  df-f1o 5976  df-fv 5977  df-riota 6694  df-ov 6736  df-oprab 6737  df-mpt2 6738  df-1st 7253  df-2nd 7254  df-cat 16419  df-cid 16420  df-sect 16497  df-inv 16498
This theorem is referenced by:  inviso1  16516  invf  16518  invco  16521  idinv  16539  funciso  16624  ffthiso  16679  fuciso  16725  setciso  16831  catciso  16847  rngciso  42377  rngcisoALTV  42389  ringciso  42428  ringcisoALTV  42452
  Copyright terms: Public domain W3C validator