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

Theorem isoeq5 6238
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 5829 . . 3  |-  ( B  =  C  ->  ( H : A -1-1-onto-> B  <->  H : A -1-1-onto-> C ) )
21anbi1d 716 . 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 5609 . 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 5609 . 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 296 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 189    /\ wa 375    = wceq 1454   A.wral 2748   class class class wbr 4415   -1-1-onto->wf1o 5599   ` cfv 5600    Isom wiso 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3422  df-ss 3429  df-f 5604  df-f1 5605  df-fo 5606  df-f1o 5607  df-isom 5609
This theorem is referenced by:  isores3  6250  ordiso  8056  ordtypelem9  8066  ordtypelem10  8067  oiid  8081  iunfictbso  8570  ltweuz  12206  fz1isolem  12656  dvgt0lem2  23003  erdszelem1  29962  erdsze  29973  erdsze2lem1  29974  erdsze2lem2  29975  fourierdlem50  38057  fourierdlem89  38096  fourierdlem90  38097  fourierdlem91  38098  fourierdlem96  38103  fourierdlem97  38104  fourierdlem98  38105  fourierdlem99  38106  fourierdlem100  38107  fourierdlem108  38115  fourierdlem110  38117  fourierdlem112  38119  fourierdlem113  38120
  Copyright terms: Public domain W3C validator