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

Theorem isorel 6020
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 5430 . . 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 4298 . . . 4  |-  ( x  =  C  ->  (
x R y  <->  C R
y ) )
4 fveq2 5694 . . . . 5  |-  ( x  =  C  ->  ( H `  x )  =  ( H `  C ) )
54breq1d 4305 . . . 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 4299 . . . 4  |-  ( y  =  D  ->  ( C R y  <->  C R D ) )
8 fveq2 5694 . . . . 5  |-  ( y  =  D  ->  ( H `  y )  =  ( H `  D ) )
98breq2d 4307 . . . 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 3082 . 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 1369    e. wcel 1756   A.wral 2718   class class class wbr 4295   -1-1-onto->wf1o 5420   ` cfv 5421    Isom wiso 5422
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-iota 5384  df-fv 5429  df-isom 5430
This theorem is referenced by:  soisores  6021  isomin  6031  isoini  6032  isopolem  6039  isosolem  6041  weniso  6048  smoiso  6826  supisolem  7723  ordiso2  7732  cantnflt  7883  cantnfp1lem3  7891  cantnflem1b  7897  cantnflem1  7900  cantnfltOLD  7913  cantnfp1lem3OLD  7917  cantnflem1bOLD  7920  cantnflem1OLD  7923  wemapwe  7931  wemapweOLD  7932  cnfcomlem  7935  cnfcom  7936  cnfcom3lem  7939  cnfcomlemOLD  7943  cnfcomOLD  7944  cnfcom3lemOLD  7947  fpwwe2lem6  8805  fpwwe2lem7  8806  fpwwe2lem9  8808  leisorel  12216  seqcoll  12219  seqcoll2  12220  isercoll  13148  ordthmeolem  19377  iccpnfhmeo  20520  xrhmeo  20521  dvcnvrelem1  21492  dvcvx  21495  isoun  26000  erdszelem8  27089  erdsze2lem2  27095
  Copyright terms: Public domain W3C validator