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

Theorem isoeq5 6204
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 5799 . . 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 5587 . 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 5587 . 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 1383   A.wral 2793   class class class wbr 4437   -1-1-onto->wf1o 5577   ` cfv 5578    Isom wiso 5579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-isom 5587
This theorem is referenced by:  isores3  6216  ordiso  7944  ordtypelem9  7954  ordtypelem10  7955  oiid  7969  iunfictbso  8498  ltweuz  12053  fz1isolem  12491  dvgt0lem2  22381  erdszelem1  28612  erdsze  28623  erdsze2lem1  28624  erdsze2lem2  28625  fourierdlem50  31828  fourierdlem89  31867  fourierdlem90  31868  fourierdlem91  31869  fourierdlem96  31874  fourierdlem97  31875  fourierdlem98  31876  fourierdlem99  31877  fourierdlem100  31878  fourierdlem108  31886  fourierdlem110  31888  fourierdlem112  31890  fourierdlem113  31891
  Copyright terms: Public domain W3C validator