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

Theorem isorel 6207
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 5587 . . 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 464 . 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 4440 . . . 4  |-  ( x  =  C  ->  (
x R y  <->  C R
y ) )
4 fveq2 5856 . . . . 5  |-  ( x  =  C  ->  ( H `  x )  =  ( H `  C ) )
54breq1d 4447 . . . 4  |-  ( x  =  C  ->  (
( H `  x
) S ( H `
 y )  <->  ( H `  C ) S ( H `  y ) ) )
63, 5bibi12d 321 . . 3  |-  ( x  =  C  ->  (
( x R y  <-> 
( H `  x
) S ( H `
 y ) )  <-> 
( C R y  <-> 
( H `  C
) S ( H `
 y ) ) ) )
7 breq2 4441 . . . 4  |-  ( y  =  D  ->  ( C R y  <->  C R D ) )
8 fveq2 5856 . . . . 5  |-  ( y  =  D  ->  ( H `  y )  =  ( H `  D ) )
98breq2d 4449 . . . 4  |-  ( y  =  D  ->  (
( H `  C
) S ( H `
 y )  <->  ( H `  C ) S ( H `  D ) ) )
107, 9bibi12d 321 . . 3  |-  ( y  =  D  ->  (
( C R y  <-> 
( H `  C
) S ( H `
 y ) )  <-> 
( C R D  <-> 
( H `  C
) S ( H `
 D ) ) ) )
116, 10rspc2v 3205 . 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 469 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 setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1383    e. wcel 1804   A.wral 2793   class class class wbr 4437   -1-1-onto->wf1o 5577   ` cfv 5578    Isom wiso 5579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-isom 5587
This theorem is referenced by:  soisores  6208  isomin  6218  isoini  6219  isopolem  6226  isosolem  6228  weniso  6235  smoiso  7035  supisolem  7934  ordiso2  7943  cantnflt  8094  cantnfp1lem3  8102  cantnflem1b  8108  cantnflem1  8111  cantnfltOLD  8124  cantnfp1lem3OLD  8128  cantnflem1bOLD  8131  cantnflem1OLD  8134  wemapwe  8142  wemapweOLD  8143  cnfcomlem  8146  cnfcom  8147  cnfcom3lem  8150  cnfcomlemOLD  8154  cnfcomOLD  8155  cnfcom3lemOLD  8158  fpwwe2lem6  9016  fpwwe2lem7  9017  fpwwe2lem9  9019  leisorel  12490  seqcoll  12493  seqcoll2  12494  isercoll  13471  ordthmeolem  20279  iccpnfhmeo  21422  xrhmeo  21423  dvcnvrelem1  22395  dvcvx  22398  isoun  27496  erdszelem8  28619  erdsze2lem2  28625  fourierdlem20  31798  fourierdlem46  31824  fourierdlem50  31828  fourierdlem63  31841  fourierdlem64  31842  fourierdlem65  31843  fourierdlem76  31854  fourierdlem79  31857  fourierdlem102  31880  fourierdlem103  31881  fourierdlem104  31882  fourierdlem114  31892
  Copyright terms: Public domain W3C validator