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

Theorem isoeq5 6205
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 5807 . . 3  |-  ( B  =  C  ->  ( H : A -1-1-onto-> B  <->  H : A -1-1-onto-> C ) )
21anbi1d 704 . 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 5595 . 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 5595 . 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 288 1  |-  ( B  =  C  ->  ( H  Isom  R ,  S  ( A ,  B )  <-> 
H  Isom  R ,  S  ( A ,  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   A.wral 2814   class class class wbr 4447   -1-1-onto->wf1o 5585   ` cfv 5586    Isom wiso 5587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-isom 5595
This theorem is referenced by:  isores3  6217  ordiso  7937  ordtypelem9  7947  ordtypelem10  7948  oiid  7962  iunfictbso  8491  ltweuz  12036  fz1isolem  12472  dvgt0lem2  22139  erdszelem1  28275  erdsze  28286  erdsze2lem1  28287  erdsze2lem2  28288  fzisoeu  31077  fourierdlem50  31457  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem96  31503  fourierdlem97  31504  fourierdlem98  31505  fourierdlem99  31506  fourierdlem100  31507  fourierdlem104  31511  fourierdlem108  31515  fourierdlem110  31517  fourierdlem112  31519  fourierdlem113  31520
  Copyright terms: Public domain W3C validator