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

Theorem isorel 5839
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 5280 . . 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 450 . 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 4042 . . . 4  |-  ( x  =  C  ->  (
x R y  <->  C R
y ) )
4 fveq2 5541 . . . . 5  |-  ( x  =  C  ->  ( H `  x )  =  ( H `  C ) )
54breq1d 4049 . . . 4  |-  ( x  =  C  ->  (
( H `  x
) S ( H `
 y )  <->  ( H `  C ) S ( H `  y ) ) )
63, 5bibi12d 312 . . 3  |-  ( x  =  C  ->  (
( x R y  <-> 
( H `  x
) S ( H `
 y ) )  <-> 
( C R y  <-> 
( H `  C
) S ( H `
 y ) ) ) )
7 breq2 4043 . . . 4  |-  ( y  =  D  ->  ( C R y  <->  C R D ) )
8 fveq2 5541 . . . . 5  |-  ( y  =  D  ->  ( H `  y )  =  ( H `  D ) )
98breq2d 4051 . . . 4  |-  ( y  =  D  ->  (
( H `  C
) S ( H `
 y )  <->  ( H `  C ) S ( H `  D ) ) )
107, 9bibi12d 312 . . 3  |-  ( y  =  D  ->  (
( C R y  <-> 
( H `  C
) S ( H `
 y ) )  <-> 
( C R D  <-> 
( H `  C
) S ( H `
 D ) ) ) )
116, 10rspc2v 2903 . 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 455 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 176    /\ wa 358    = wceq 1632    e. wcel 1696   A.wral 2556   class class class wbr 4039   -1-1-onto->wf1o 5270   ` cfv 5271    Isom wiso 5272
This theorem is referenced by:  soisores  5840  isomin  5850  isoini  5851  isopolem  5858  isosolem  5860  weniso  5868  smoiso  6395  supisolem  7237  ordiso2  7246  cantnflt  7389  cantnfp1lem3  7398  cantnflem1b  7404  cantnflem1  7407  wemapwe  7416  cnfcomlem  7418  cnfcom  7419  cnfcom3lem  7422  fpwwe2lem6  8273  fpwwe2lem7  8274  fpwwe2lem9  8276  leisorel  11414  seqcoll  11417  seqcoll2  11418  isercoll  12157  ordthmeolem  17508  iccpnfhmeo  18459  xrhmeo  18460  dvcnvrelem1  19380  dvcvx  19383  isoun  23257  erdszelem8  23744  erdsze2lem2  23750
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-isom 5280
  Copyright terms: Public domain W3C validator