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

Theorem isinv 15662
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 15661 . . . 4  |-  ( ph  ->  ( X N Y )  =  ( ( X S Y )  i^i  `' ( Y S X ) ) )
87breqd 4433 . . 3  |-  ( ph  ->  ( F ( X N Y ) G  <-> 
F ( ( X S Y )  i^i  `' ( Y S X ) ) G ) )
9 brin 4472 . . 3  |-  ( F ( ( X S Y )  i^i  `' ( Y S X ) ) G  <->  ( F
( X S Y ) G  /\  F `' ( Y S X ) G ) )
108, 9syl6bb 265 . 2  |-  ( ph  ->  ( F ( X N Y ) G  <-> 
( F ( X S Y ) G  /\  F `' ( Y S X ) G ) ) )
11 eqid 2423 . . . . . 6  |-  ( Hom  `  C )  =  ( Hom  `  C )
12 eqid 2423 . . . . . 6  |-  (comp `  C )  =  (comp `  C )
13 eqid 2423 . . . . . 6  |-  ( Id
`  C )  =  ( Id `  C
)
141, 11, 12, 13, 6, 3, 5, 4sectss 15654 . . . . 5  |-  ( ph  ->  ( Y S X )  C_  ( ( Y ( Hom  `  C
) X )  X.  ( X ( Hom  `  C ) Y ) ) )
15 relxp 4960 . . . . 5  |-  Rel  (
( Y ( Hom  `  C ) X )  X.  ( X ( Hom  `  C ) Y ) )
16 relss 4940 . . . . 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 22 . . . 4  |-  ( ph  ->  Rel  ( Y S X ) )
18 relbrcnvg 5226 . . . 4  |-  ( Rel  ( Y S X )  ->  ( F `' ( Y S X ) G  <->  G ( Y S X ) F ) )
1917, 18syl 17 . . 3  |-  ( ph  ->  ( F `' ( Y S X ) G  <->  G ( Y S X ) F ) )
2019anbi2d 709 . 2  |-  ( ph  ->  ( ( F ( X S Y ) G  /\  F `' ( Y S X ) G )  <->  ( F
( X S Y ) G  /\  G
( Y S X ) F ) ) )
2110, 20bitrd 257 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 188    /\ wa 371    = wceq 1438    e. wcel 1869    i^i cin 3437    C_ wss 3438   class class class wbr 4422    X. cxp 4850   `'ccnv 4851   Rel wrel 4857   ` cfv 5600  (class class class)co 6304   Basecbs 15118   Hom chom 15198  compcco 15199   Catccat 15567   Idccid 15568  Sectcsect 15646  Invcinv 15647
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-rep 4535  ax-sep 4545  ax-nul 4554  ax-pow 4601  ax-pr 4659  ax-un 6596
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3084  df-sbc 3302  df-csb 3398  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-nul 3764  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4219  df-iun 4300  df-br 4423  df-opab 4482  df-mpt 4483  df-id 4767  df-xp 4858  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-res 4864  df-ima 4865  df-iota 5564  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-fv 5608  df-ov 6307  df-oprab 6308  df-mpt2 6309  df-1st 6806  df-2nd 6807  df-sect 15649  df-inv 15650
This theorem is referenced by:  invsym  15664  invfun  15666  invco  15673  inveq  15676  monsect  15685  invid  15689  invcoisoid  15694  isocoinvid  15695  cicref  15703  funcinv  15775  fthinv  15828  fucinv  15875  invfuc  15876  2initoinv  15902  2termoinv  15909  setcinv  15982  catcisolem  15998  catciso  15999  rngcinv  39375  rngcinvALTV  39387  ringcinv  39426  ringcinvALTV  39450
  Copyright terms: Public domain W3C validator