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

Theorem isorel 6004
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 5415 . . 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 461 . 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 4283 . . . 4  |-  ( x  =  C  ->  (
x R y  <->  C R
y ) )
4 fveq2 5679 . . . . 5  |-  ( x  =  C  ->  ( H `  x )  =  ( H `  C ) )
54breq1d 4290 . . . 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 4284 . . . 4  |-  ( y  =  D  ->  ( C R y  <->  C R D ) )
8 fveq2 5679 . . . . 5  |-  ( y  =  D  ->  ( H `  y )  =  ( H `  D ) )
98breq2d 4292 . . . 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 3068 . 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 466 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 1362    e. wcel 1755   A.wral 2705   class class class wbr 4280   -1-1-onto->wf1o 5405   ` cfv 5406    Isom wiso 5407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-isom 5415
This theorem is referenced by:  soisores  6005  isomin  6015  isoini  6016  isopolem  6023  isosolem  6025  weniso  6032  smoiso  6809  supisolem  7708  ordiso2  7717  cantnflt  7868  cantnfp1lem3  7876  cantnflem1b  7882  cantnflem1  7885  cantnfltOLD  7898  cantnfp1lem3OLD  7902  cantnflem1bOLD  7905  cantnflem1OLD  7908  wemapwe  7916  wemapweOLD  7917  cnfcomlem  7920  cnfcom  7921  cnfcom3lem  7924  cnfcomlemOLD  7928  cnfcomOLD  7929  cnfcom3lemOLD  7932  fpwwe2lem6  8790  fpwwe2lem7  8791  fpwwe2lem9  8793  leisorel  12197  seqcoll  12200  seqcoll2  12201  isercoll  13129  ordthmeolem  19216  iccpnfhmeo  20359  xrhmeo  20360  dvcnvrelem1  21331  dvcvx  21334  isoun  25821  erdszelem8  26934  erdsze2lem2  26940
  Copyright terms: Public domain W3C validator