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

Theorem isorel 5985
Description: An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
Assertion
Ref Expression
isorel  |-  ( ( H  Isom  R ,  S  ( A ,  B )  /\  ( C  e.  A  /\  D  e.  A )
)  ->  ( C R D  <->  ( H `  C ) S ( H `  D ) ) )

Proof of Theorem isorel
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-isom 5403 . . 3  |-  ( H 
Isom  R ,  S  ( A ,  B )  <-> 
( H : A -1-1-onto-> B  /\  A. x  e.  A  A. y  e.  A  ( x R y  <-> 
( H `  x
) S ( H `
 y ) ) ) )
21simprbi 451 . 2  |-  ( H 
Isom  R ,  S  ( A ,  B )  ->  A. x  e.  A  A. y  e.  A  ( x R y  <-> 
( H `  x
) S ( H `
 y ) ) )
3 breq1 4156 . . . 4  |-  ( x  =  C  ->  (
x R y  <->  C R
y ) )
4 fveq2 5668 . . . . 5  |-  ( x  =  C  ->  ( H `  x )  =  ( H `  C ) )
54breq1d 4163 . . . 4  |-  ( x  =  C  ->  (
( H `  x
) S ( H `
 y )  <->  ( H `  C ) S ( H `  y ) ) )
63, 5bibi12d 313 . . 3  |-  ( x  =  C  ->  (
( x R y  <-> 
( H `  x
) S ( H `
 y ) )  <-> 
( C R y  <-> 
( H `  C
) S ( H `
 y ) ) ) )
7 breq2 4157 . . . 4  |-  ( y  =  D  ->  ( C R y  <->  C R D ) )
8 fveq2 5668 . . . . 5  |-  ( y  =  D  ->  ( H `  y )  =  ( H `  D ) )
98breq2d 4165 . . . 4  |-  ( y  =  D  ->  (
( H `  C
) S ( H `
 y )  <->  ( H `  C ) S ( H `  D ) ) )
107, 9bibi12d 313 . . 3  |-  ( y  =  D  ->  (
( C R y  <-> 
( H `  C
) S ( H `
 y ) )  <-> 
( C R D  <-> 
( H `  C
) S ( H `
 D ) ) ) )
116, 10rspc2v 3001 . 2  |-  ( ( C  e.  A  /\  D  e.  A )  ->  ( A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) )  ->  ( C R D  <->  ( H `  C ) S ( H `  D ) ) ) )
122, 11mpan9 456 1  |-  ( ( H  Isom  R ,  S  ( A ,  B )  /\  ( C  e.  A  /\  D  e.  A )
)  ->  ( C R D  <->  ( H `  C ) S ( H `  D ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2649   class class class wbr 4153   -1-1-onto->wf1o 5393   ` cfv 5394    Isom wiso 5395
This theorem is referenced by:  soisores  5986  isomin  5996  isoini  5997  isopolem  6004  isosolem  6006  weniso  6014  smoiso  6560  supisolem  7408  ordiso2  7417  cantnflt  7560  cantnfp1lem3  7569  cantnflem1b  7575  cantnflem1  7578  wemapwe  7587  cnfcomlem  7589  cnfcom  7590  cnfcom3lem  7593  fpwwe2lem6  8443  fpwwe2lem7  8444  fpwwe2lem9  8446  leisorel  11636  seqcoll  11639  seqcoll2  11640  isercoll  12388  ordthmeolem  17754  iccpnfhmeo  18841  xrhmeo  18842  dvcnvrelem1  19768  dvcvx  19771  isoun  23930  erdszelem8  24663  erdsze2lem2  24669
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-isom 5403
  Copyright terms: Public domain W3C validator