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

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

Proof of Theorem isoeq4
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oeq2 6823 . . 3 (𝐴 = 𝐶 → (𝐻:𝐴1-1-onto𝐵𝐻:𝐶1-1-onto𝐵))
2 raleq 3323 . . . 4 (𝐴 = 𝐶 → (∀𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ∀𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
32raleqbi1dv 3334 . . 3 (𝐴 = 𝐶 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ∀𝑥𝐶𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
41, 3anbi12d 632 . 2 (𝐴 = 𝐶 → ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ↔ (𝐻:𝐶1-1-onto𝐵 ∧ ∀𝑥𝐶𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))))
5 df-isom 6553 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
6 df-isom 6553 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵) ↔ (𝐻:𝐶1-1-onto𝐵 ∧ ∀𝑥𝐶𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
74, 5, 63bitr4g 314 1 (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wral 3062   class class class wbr 5149  1-1-ontowf1o 6543  cfv 6544   Isom wiso 6545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ral 3063  df-rex 3072  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-isom 6553
This theorem is referenced by:  oieu  9534  oiid  9536  finnisoeu  10108  iunfictbso  10109  fz1isolem  14422  isercolllem3  15613  summolem2a  15661  prodmolem2a  15878  erdszelem1  34182  erdsze  34193  erdsze2lem1  34194  erdsze2lem2  34195  isoeq145d  42170  fzisoeu  44010  fourierdlem36  44859  fourierdlem112  44934  fourierdlem113  44935
  Copyright terms: Public domain W3C validator