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

Theorem isoeq5 6035
Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
Assertion
Ref Expression
isoeq5  |-  ( B  =  C  ->  ( H  Isom  R ,  S  ( A ,  B )  <-> 
H  Isom  R ,  S  ( A ,  C ) ) )

Proof of Theorem isoeq5
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oeq3 5659 . . 3  |-  ( B  =  C  ->  ( H : A -1-1-onto-> B  <->  H : A -1-1-onto-> C ) )
21anbi1d 686 . 2  |-  ( B  =  C  ->  (
( H : A -1-1-onto-> B  /\  A. x  e.  A  A. y  e.  A  ( x R y  <-> 
( H `  x
) S ( H `
 y ) ) )  <->  ( H : A
-1-1-onto-> C  /\  A. x  e.  A  A. y  e.  A  ( x R y  <->  ( H `  x ) S ( H `  y ) ) ) ) )
3 df-isom 5455 . 2  |-  ( 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 ) ) ) )
4 df-isom 5455 . 2  |-  ( H 
Isom  R ,  S  ( A ,  C )  <-> 
( H : A -1-1-onto-> C  /\  A. x  e.  A  A. y  e.  A  ( x R y  <-> 
( H `  x
) S ( H `
 y ) ) ) )
52, 3, 43bitr4g 280 1  |-  ( B  =  C  ->  ( H  Isom  R ,  S  ( A ,  B )  <-> 
H  Isom  R ,  S  ( A ,  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1652   A.wral 2697   class class class wbr 4204   -1-1-onto->wf1o 5445   ` cfv 5446    Isom wiso 5447
This theorem is referenced by:  isores3  6047  ordiso  7477  ordtypelem9  7487  ordtypelem10  7488  oiid  7502  iunfictbso  7987  ltweuz  11293  fz1isolem  11702  dvgt0lem2  19879  erdszelem1  24869  erdsze  24880  erdsze2lem1  24881  erdsze2lem2  24882
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-in 3319  df-ss 3326  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-isom 5455
  Copyright terms: Public domain W3C validator