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

Theorem isoeq5 7323
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 6823 . . 3 (𝐵 = 𝐶 → (𝐻:𝐴1-1-onto𝐵𝐻:𝐴1-1-onto𝐶))
21anbi1d 629 . 2 (𝐵 = 𝐶 → ((𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))) ↔ (𝐻:𝐴1-1-onto𝐶 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))))
3 df-isom 6551 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
4 df-isom 6551 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶) ↔ (𝐻:𝐴1-1-onto𝐶 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
52, 3, 43bitr4g 314 1 (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395   = wceq 1534  wral 3056   class class class wbr 5142  1-1-ontowf1o 6541  cfv 6542   Isom wiso 6543
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-isom 6551
This theorem is referenced by:  isores3  7337  ordiso  9531  ordtypelem9  9541  ordtypelem10  9542  oiid  9556  iunfictbso  10129  ltweuz  13950  fz1isolem  14446  dvgt0lem2  25923  erdszelem1  34737  erdsze  34748  erdsze2lem1  34749  erdsze2lem2  34750  isoeq145d  42772  alephiso3  42912  fourierdlem50  45467  fourierdlem89  45506  fourierdlem90  45507  fourierdlem91  45508  fourierdlem96  45513  fourierdlem97  45514  fourierdlem98  45515  fourierdlem99  45516  fourierdlem100  45517  fourierdlem108  45525  fourierdlem110  45527  fourierdlem112  45529  fourierdlem113  45530
  Copyright terms: Public domain W3C validator