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

Theorem isoeq4 7340
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 6837 . . 3 (𝐴 = 𝐶 → (𝐻:𝐴1-1-onto𝐵𝐻:𝐶1-1-onto𝐵))
2 raleq 3323 . . . 4 (𝐴 = 𝐶 → (∀𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ∀𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
32raleqbi1dv 3338 . . 3 (𝐴 = 𝐶 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ∀𝑥𝐶𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
41, 3anbi12d 632 . 2 (𝐴 = 𝐶 → ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ↔ (𝐻:𝐶1-1-onto𝐵 ∧ ∀𝑥𝐶𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))))
5 df-isom 6570 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
6 df-isom 6570 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵) ↔ (𝐻:𝐶1-1-onto𝐵 ∧ ∀𝑥𝐶𝑦𝐶 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
74, 5, 63bitr4g 314 1 (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wral 3061   class class class wbr 5143  1-1-ontowf1o 6560  cfv 6561   Isom wiso 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ral 3062  df-rex 3071  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-isom 6570
This theorem is referenced by:  oieu  9579  oiid  9581  finnisoeu  10153  iunfictbso  10154  fz1isolem  14500  isercolllem3  15703  summolem2a  15751  prodmolem2a  15970  erdszelem1  35196  erdsze  35207  erdsze2lem1  35208  erdsze2lem2  35209  isoeq145d  43432  fzisoeu  45312  fourierdlem36  46158  fourierdlem112  46233  fourierdlem113  46234
  Copyright terms: Public domain W3C validator