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

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

Proof of Theorem isoeq1
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1oeq1 6835 . . 3 (𝐻 = 𝐺 → (𝐻:𝐴1-1-onto𝐵𝐺:𝐴1-1-onto𝐵))
2 fveq1 6904 . . . . . 6 (𝐻 = 𝐺 → (𝐻𝑥) = (𝐺𝑥))
3 fveq1 6904 . . . . . 6 (𝐻 = 𝐺 → (𝐻𝑦) = (𝐺𝑦))
42, 3breq12d 5155 . . . . 5 (𝐻 = 𝐺 → ((𝐻𝑥)𝑆(𝐻𝑦) ↔ (𝐺𝑥)𝑆(𝐺𝑦)))
54bibi2d 342 . . . 4 (𝐻 = 𝐺 → ((𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦))))
652ralbidv 3220 . . 3 (𝐻 = 𝐺 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦))))
71, 6anbi12d 632 . 2 (𝐻 = 𝐺 → ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ↔ (𝐺:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦)))))
8 df-isom 6569 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
9 df-isom 6569 . 2 (𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐺:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐺𝑥)𝑆(𝐺𝑦))))
107, 8, 93bitr4g 314 1 (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1539  wral 3060   class class class wbr 5142  1-1-ontowf1o 6559  cfv 6560   Isom wiso 6561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ral 3061  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-isom 6569
This theorem is referenced by:  isores1  7355  wemoiso  7999  wemoiso2  8000  ordiso  9557  oieu  9580  finnisoeu  10154  iunfictbso  10155  infrenegsup  12252  ltweuz  14003  fz1isolem  14501  isercolllem2  15703  isercoll  15705  dvgt0lem2  26043  efcvx  26494  relogiso  26641  logccv  26706  erdszelem1  35197  erdsze  35208  erdsze2lem2  35210  isoeq145d  43437  fzisoeu  45317  fourierdlem36  46163  fourierdlem96  46222  fourierdlem97  46223  fourierdlem98  46224  fourierdlem99  46225  fourierdlem105  46231  fourierdlem106  46232  fourierdlem108  46234  fourierdlem110  46236  fourierdlem112  46238  fourierdlem113  46239  fourierdlem115  46241  rrx2plordisom  48649
  Copyright terms: Public domain W3C validator