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

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

Proof of Theorem isoeq4
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oeq2 5791 . . 3  |-  ( A  =  C  ->  ( H : A -1-1-onto-> B  <->  H : C -1-1-onto-> B ) )
2 raleq 3004 . . . 4  |-  ( A  =  C  ->  ( A. y  e.  A  ( x R y  <-> 
( H `  x
) S ( H `
 y ) )  <->  A. y  e.  C  ( x R y  <-> 
( H `  x
) S ( H `
 y ) ) ) )
32raleqbi1dv 3012 . . 3  |-  ( A  =  C  ->  ( A. x  e.  A  A. y  e.  A  ( x R y  <-> 
( H `  x
) S ( H `
 y ) )  <->  A. x  e.  C  A. y  e.  C  ( x R y  <-> 
( H `  x
) S ( H `
 y ) ) ) )
41, 3anbi12d 709 . 2  |-  ( A  =  C  ->  (
( H : A -1-1-onto-> B  /\  A. x  e.  A  A. y  e.  A  ( x R y  <-> 
( H `  x
) S ( H `
 y ) ) )  <->  ( H : C
-1-1-onto-> B  /\  A. x  e.  C  A. y  e.  C  ( x R y  <->  ( H `  x ) S ( H `  y ) ) ) ) )
5 df-isom 5578 . 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 ) ) ) )
6 df-isom 5578 . 2  |-  ( H 
Isom  R ,  S  ( C ,  B )  <-> 
( H : C -1-1-onto-> B  /\  A. x  e.  C  A. y  e.  C  ( x R y  <-> 
( H `  x
) S ( H `
 y ) ) ) )
74, 5, 63bitr4g 288 1  |-  ( A  =  C  ->  ( H  Isom  R ,  S  ( A ,  B )  <-> 
H  Isom  R ,  S  ( C ,  B ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1405   A.wral 2754   class class class wbr 4395   -1-1-onto->wf1o 5568   ` cfv 5569    Isom wiso 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-fn 5572  df-f 5573  df-f1 5574  df-fo 5575  df-f1o 5576  df-isom 5578
This theorem is referenced by:  oieu  7998  oiid  8000  finnisoeu  8526  iunfictbso  8527  fz1isolem  12559  isercolllem3  13638  summolem2a  13686  prodmolem2a  13893  erdszelem1  29488  erdsze  29499  erdsze2lem1  29500  erdsze2lem2  29501  fzisoeu  36869  fourierdlem36  37293  fourierdlem112  37369  fourierdlem113  37370
  Copyright terms: Public domain W3C validator