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

Theorem isorel 6848
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 6144 . . 3 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴1-1-onto𝐵 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦))))
21simprbi 492 . 2 (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)))
3 breq1 4889 . . . 4 (𝑥 = 𝐶 → (𝑥𝑅𝑦𝐶𝑅𝑦))
4 fveq2 6446 . . . . 5 (𝑥 = 𝐶 → (𝐻𝑥) = (𝐻𝐶))
54breq1d 4896 . . . 4 (𝑥 = 𝐶 → ((𝐻𝑥)𝑆(𝐻𝑦) ↔ (𝐻𝐶)𝑆(𝐻𝑦)))
63, 5bibi12d 337 . . 3 (𝑥 = 𝐶 → ((𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) ↔ (𝐶𝑅𝑦 ↔ (𝐻𝐶)𝑆(𝐻𝑦))))
7 breq2 4890 . . . 4 (𝑦 = 𝐷 → (𝐶𝑅𝑦𝐶𝑅𝐷))
8 fveq2 6446 . . . . 5 (𝑦 = 𝐷 → (𝐻𝑦) = (𝐻𝐷))
98breq2d 4898 . . . 4 (𝑦 = 𝐷 → ((𝐻𝐶)𝑆(𝐻𝑦) ↔ (𝐻𝐶)𝑆(𝐻𝐷)))
107, 9bibi12d 337 . . 3 (𝑦 = 𝐷 → ((𝐶𝑅𝑦 ↔ (𝐻𝐶)𝑆(𝐻𝑦)) ↔ (𝐶𝑅𝐷 ↔ (𝐻𝐶)𝑆(𝐻𝐷))))
116, 10rspc2v 3524 . 2 ((𝐶𝐴𝐷𝐴) → (∀𝑥𝐴𝑦𝐴 (𝑥𝑅𝑦 ↔ (𝐻𝑥)𝑆(𝐻𝑦)) → (𝐶𝑅𝐷 ↔ (𝐻𝐶)𝑆(𝐻𝐷))))
122, 11mpan9 502 1 ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶𝐴𝐷𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻𝐶)𝑆(𝐻𝐷)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wcel 2107  wral 3090   class class class wbr 4886  1-1-ontowf1o 6134  cfv 6135   Isom wiso 6136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-isom 6144
This theorem is referenced by:  soisores  6849  isomin  6859  isoini  6860  isopolem  6867  isosolem  6869  weniso  6876  smoiso  7742  supisolem  8667  ordiso2  8709  cantnflt  8866  cantnfp1lem3  8874  cantnflem1b  8880  cantnflem1  8883  wemapwe  8891  cnfcomlem  8893  cnfcom  8894  cnfcom3lem  8897  fpwwe2lem6  9792  fpwwe2lem7  9793  fpwwe2lem9  9795  leisorel  13558  seqcoll  13562  seqcoll2  13563  isercoll  14806  ordthmeolem  22013  iccpnfhmeo  23152  xrhmeo  23153  dvcnvrelem1  24217  dvcvx  24220  isoun  30045  erdszelem8  31779  erdsze2lem2  31785  fourierdlem20  41275  fourierdlem46  41300  fourierdlem50  41304  fourierdlem63  41317  fourierdlem64  41318  fourierdlem65  41319  fourierdlem76  41330  fourierdlem79  41333  fourierdlem102  41356  fourierdlem103  41357  fourierdlem104  41358  fourierdlem114  41368
  Copyright terms: Public domain W3C validator