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

Theorem isoeq5 7341
Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.)
Assertion
Ref Expression
isoeq5 (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))

Proof of Theorem isoeq5
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oeq3 6839 . . 3 (𝐵 = 𝐶 → (𝐻:𝐴1-1-onto𝐵𝐻:𝐴1-1-onto𝐶))
21anbi1d 631 . 2 (𝐵 = 𝐶 → ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ↔ (𝐻:𝐴1-1-onto𝐶 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))))
3 df-isom 6572 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
4 df-isom 6572 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶) ↔ (𝐻:𝐴1-1-onto𝐶 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
52, 3, 43bitr4g 314 1 (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wral 3059   class class class wbr 5148  1-1-ontowf1o 6562  cfv 6563   Isom wiso 6564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-isom 6572
This theorem is referenced by:  isores3  7355  ordiso  9554  ordtypelem9  9564  ordtypelem10  9565  oiid  9579  iunfictbso  10152  ltweuz  13999  fz1isolem  14497  dvgt0lem2  26057  erdszelem1  35176  erdsze  35187  erdsze2lem1  35188  erdsze2lem2  35189  isoeq145d  43409  alephiso3  43549  fourierdlem50  46112  fourierdlem89  46151  fourierdlem90  46152  fourierdlem91  46153  fourierdlem96  46158  fourierdlem97  46159  fourierdlem98  46160  fourierdlem99  46161  fourierdlem100  46162  fourierdlem108  46170  fourierdlem110  46172  fourierdlem112  46174  fourierdlem113  46175
  Copyright terms: Public domain W3C validator