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

Theorem isoeq4 7066
 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 6596 . . 3 (𝐴 = 𝐶 → (𝐻:𝐴1-1-onto𝐵𝐻:𝐶1-1-onto𝐵))
2 raleq 3396 . . . 4 (𝐴 = 𝐶 → (∀𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ∀𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
32raleqbi1dv 3394 . . 3 (𝐴 = 𝐶 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ∀𝑥𝐶𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
41, 3anbi12d 633 . 2 (𝐴 = 𝐶 → ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ↔ (𝐻:𝐶1-1-onto𝐵 ∧ ∀𝑥𝐶𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))))
5 df-isom 6352 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
6 df-isom 6352 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵) ↔ (𝐻:𝐶1-1-onto𝐵 ∧ ∀𝑥𝐶𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
74, 5, 63bitr4g 317 1 (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538  ∀wral 3133   class class class wbr 5052  –1-1-onto→wf1o 6342  ‘cfv 6343   Isom wiso 6344 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2817  df-clel 2896  df-ral 3138  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-isom 6352 This theorem is referenced by:  oieu  9000  oiid  9002  finnisoeu  9537  iunfictbso  9538  fz1isolem  13824  isercolllem3  15023  summolem2a  15072  prodmolem2a  15288  erdszelem1  32495  erdsze  32506  erdsze2lem1  32507  erdsze2lem2  32508  fzisoeu  41858  fourierdlem36  42711  fourierdlem112  42786  fourierdlem113  42787
 Copyright terms: Public domain W3C validator