MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isinv Structured version   Unicode version

Theorem isinv 15185
Description: Value of the inverse relation. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
invfval.b  |-  B  =  ( Base `  C
)
invfval.n  |-  N  =  (Inv `  C )
invfval.c  |-  ( ph  ->  C  e.  Cat )
invfval.x  |-  ( ph  ->  X  e.  B )
invfval.y  |-  ( ph  ->  Y  e.  B )
invfval.s  |-  S  =  (Sect `  C )
Assertion
Ref Expression
isinv  |-  ( ph  ->  ( F ( X N Y ) G  <-> 
( F ( X S Y ) G  /\  G ( Y S X ) F ) ) )

Proof of Theorem isinv
StepHypRef Expression
1 invfval.b . . . . 5  |-  B  =  ( Base `  C
)
2 invfval.n . . . . 5  |-  N  =  (Inv `  C )
3 invfval.c . . . . 5  |-  ( ph  ->  C  e.  Cat )
4 invfval.x . . . . 5  |-  ( ph  ->  X  e.  B )
5 invfval.y . . . . 5  |-  ( ph  ->  Y  e.  B )
6 invfval.s . . . . 5  |-  S  =  (Sect `  C )
71, 2, 3, 4, 5, 6invfval 15184 . . . 4  |-  ( ph  ->  ( X N Y )  =  ( ( X S Y )  i^i  `' ( Y S X ) ) )
87breqd 4391 . . 3  |-  ( ph  ->  ( F ( X N Y ) G  <-> 
F ( ( X S Y )  i^i  `' ( Y S X ) ) G ) )
9 brin 4429 . . 3  |-  ( F ( ( X S Y )  i^i  `' ( Y S X ) ) G  <->  ( F
( X S Y ) G  /\  F `' ( Y S X ) G ) )
108, 9syl6bb 261 . 2  |-  ( ph  ->  ( F ( X N Y ) G  <-> 
( F ( X S Y ) G  /\  F `' ( Y S X ) G ) ) )
11 eqid 2392 . . . . . 6  |-  ( Hom  `  C )  =  ( Hom  `  C )
12 eqid 2392 . . . . . 6  |-  (comp `  C )  =  (comp `  C )
13 eqid 2392 . . . . . 6  |-  ( Id
`  C )  =  ( Id `  C
)
141, 11, 12, 13, 6, 3, 5, 4sectss 15177 . . . . 5  |-  ( ph  ->  ( Y S X )  C_  ( ( Y ( Hom  `  C
) X )  X.  ( X ( Hom  `  C ) Y ) ) )
15 relxp 5036 . . . . 5  |-  Rel  (
( Y ( Hom  `  C ) X )  X.  ( X ( Hom  `  C ) Y ) )
16 relss 5016 . . . . 5  |-  ( ( Y S X ) 
C_  ( ( Y ( Hom  `  C
) X )  X.  ( X ( Hom  `  C ) Y ) )  ->  ( Rel  ( ( Y ( Hom  `  C ) X )  X.  ( X ( Hom  `  C
) Y ) )  ->  Rel  ( Y S X ) ) )
1714, 15, 16mpisyl 18 . . . 4  |-  ( ph  ->  Rel  ( Y S X ) )
18 relbrcnvg 5301 . . . 4  |-  ( Rel  ( Y S X )  ->  ( F `' ( Y S X ) G  <->  G ( Y S X ) F ) )
1917, 18syl 16 . . 3  |-  ( ph  ->  ( F `' ( Y S X ) G  <->  G ( Y S X ) F ) )
2019anbi2d 701 . 2  |-  ( ph  ->  ( ( F ( X S Y ) G  /\  F `' ( Y S X ) G )  <->  ( F
( X S Y ) G  /\  G
( Y S X ) F ) ) )
2110, 20bitrd 253 1  |-  ( ph  ->  ( F ( X N Y ) G  <-> 
( F ( X S Y ) G  /\  G ( Y S X ) F ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1399    e. wcel 1836    i^i cin 3401    C_ wss 3402   class class class wbr 4380    X. cxp 4924   `'ccnv 4925   Rel wrel 4931   ` cfv 5509  (class class class)co 6214   Basecbs 14653   Hom chom 14732  compcco 14733   Catccat 15090   Idccid 15091  Sectcsect 15169  Invcinv 15170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370  ax-rep 4491  ax-sep 4501  ax-nul 4509  ax-pow 4556  ax-pr 4614  ax-un 6509
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-mo 2233  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ne 2589  df-ral 2747  df-rex 2748  df-reu 2749  df-rab 2751  df-v 3049  df-sbc 3266  df-csb 3362  df-dif 3405  df-un 3407  df-in 3409  df-ss 3416  df-nul 3725  df-if 3871  df-pw 3942  df-sn 3958  df-pr 3960  df-op 3964  df-uni 4177  df-iun 4258  df-br 4381  df-opab 4439  df-mpt 4440  df-id 4722  df-xp 4932  df-rel 4933  df-cnv 4934  df-co 4935  df-dm 4936  df-rn 4937  df-res 4938  df-ima 4939  df-iota 5473  df-fun 5511  df-fn 5512  df-f 5513  df-f1 5514  df-fo 5515  df-f1o 5516  df-fv 5517  df-ov 6217  df-oprab 6218  df-mpt2 6219  df-1st 6717  df-2nd 6718  df-sect 15172  df-inv 15173
This theorem is referenced by:  invsym  15187  invfun  15189  invco  15196  inveq  15199  monsect  15208  invid  15212  invcoisoid  15217  isocoinvid  15218  cicref  15226  funcinv  15298  fthinv  15351  fucinv  15398  invfuc  15399  2initoinv  15425  2termoinv  15432  setcinv  15505  catcisolem  15521  catciso  15522  rngcinv  33024  rngcinvALTV  33036  ringcinv  33075  ringcinvALTV  33099
  Copyright terms: Public domain W3C validator