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

Theorem isoeq5 6230
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 5824 . . 3  |-  ( B  =  C  ->  ( H : A -1-1-onto-> B  <->  H : A -1-1-onto-> C ) )
21anbi1d 709 . 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 5610 . 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 5610 . 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 291 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 187    /\ wa 370    = wceq 1437   A.wral 2771   class class class wbr 4423   -1-1-onto->wf1o 5600   ` cfv 5601    Isom wiso 5602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-isom 5610
This theorem is referenced by:  isores3  6242  ordiso  8041  ordtypelem9  8051  ordtypelem10  8052  oiid  8066  iunfictbso  8553  ltweuz  12182  fz1isolem  12629  dvgt0lem2  22954  erdszelem1  29923  erdsze  29934  erdsze2lem1  29935  erdsze2lem2  29936  fourierdlem50  37961  fourierdlem89  38000  fourierdlem90  38001  fourierdlem91  38002  fourierdlem96  38007  fourierdlem97  38008  fourierdlem98  38009  fourierdlem99  38010  fourierdlem100  38011  fourierdlem108  38019  fourierdlem110  38021  fourierdlem112  38023  fourierdlem113  38024
  Copyright terms: Public domain W3C validator