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

Theorem isorel 7063
 Description: An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.)
Assertion
Ref Expression
isorel ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶𝐴𝐷𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻𝐶)𝑆(𝐻𝐷)))

Proof of Theorem isorel
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-isom 6343 . . 3 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simprbi 500 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))
3 breq1 5045 . . . 4 (𝑥 = 𝐶 → (𝑥𝑅𝑦𝐶𝑅𝑦))
4 fveq2 6652 . . . . 5 (𝑥 = 𝐶 → (𝐻𝑥) = (𝐻𝐶))
54breq1d 5052 . . . 4 (𝑥 = 𝐶 → ((𝐻𝑥)𝑆(𝐻𝑦) ↔ (𝐻𝐶)𝑆(𝐻𝑦)))
63, 5bibi12d 349 . . 3 (𝑥 = 𝐶 → ((𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ (𝐶𝑅𝑦 ↔ (𝐻𝐶)𝑆(𝐻𝑦))))
7 breq2 5046 . . . 4 (𝑦 = 𝐷 → (𝐶𝑅𝑦𝐶𝑅𝐷))
8 fveq2 6652 . . . . 5 (𝑦 = 𝐷 → (𝐻𝑦) = (𝐻𝐷))
98breq2d 5054 . . . 4 (𝑦 = 𝐷 → ((𝐻𝐶)𝑆(𝐻𝑦) ↔ (𝐻𝐶)𝑆(𝐻𝐷)))
107, 9bibi12d 349 . . 3 (𝑦 = 𝐷 → ((𝐶𝑅𝑦 ↔ (𝐻𝐶)𝑆(𝐻𝑦)) ↔ (𝐶𝑅𝐷 ↔ (𝐻𝐶)𝑆(𝐻𝐷))))
116, 10rspc2v 3608 . 2 ((𝐶𝐴𝐷𝐴) → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) → (𝐶𝑅𝐷 ↔ (𝐻𝐶)𝑆(𝐻𝐷))))
122, 11mpan9 510 1 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶𝐴𝐷𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻𝐶)𝑆(𝐻𝐷)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2114  ∀wral 3130   class class class wbr 5042  –1-1-onto→wf1o 6333  ‘cfv 6334   Isom wiso 6335 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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-ral 3135  df-v 3471  df-un 3913  df-in 3915  df-ss 3925  df-sn 4540  df-pr 4542  df-op 4546  df-uni 4814  df-br 5043  df-iota 6293  df-fv 6342  df-isom 6343 This theorem is referenced by:  soisores  7064  isomin  7074  isoini  7075  isopolem  7082  isosolem  7084  weniso  7091  smoiso  7986  supisolem  8925  ordiso2  8967  cantnflt  9123  cantnfp1lem3  9131  cantnflem1b  9137  cantnflem1  9140  wemapwe  9148  cnfcomlem  9150  cnfcom  9151  cnfcom3lem  9154  fpwwe2lem6  10046  fpwwe2lem7  10047  fpwwe2lem9  10049  leisorel  13814  seqcoll  13818  seqcoll2  13819  isercoll  15015  ordthmeolem  22404  iccpnfhmeo  23548  xrhmeo  23549  dvcnvrelem1  24618  dvcvx  24621  isoun  30445  erdszelem8  32519  erdsze2lem2  32525  fourierdlem20  42709  fourierdlem46  42734  fourierdlem50  42738  fourierdlem63  42751  fourierdlem64  42752  fourierdlem65  42753  fourierdlem76  42764  fourierdlem79  42767  fourierdlem102  42790  fourierdlem103  42791  fourierdlem104  42792  fourierdlem114  42802
 Copyright terms: Public domain W3C validator