![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isorel | Structured version Visualization version GIF version |
Description: An isomorphism connects binary relations via its function values. (Contributed by NM, 27-Apr-2004.) |
Ref | Expression |
---|---|
isorel | ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-isom 6553 | . . 3 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
2 | 1 | simprbi 498 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) |
3 | breq1 5152 | . . . 4 ⊢ (𝑥 = 𝐶 → (𝑥𝑅𝑦 ↔ 𝐶𝑅𝑦)) | |
4 | fveq2 6892 | . . . . 5 ⊢ (𝑥 = 𝐶 → (𝐻‘𝑥) = (𝐻‘𝐶)) | |
5 | 4 | breq1d 5159 | . . . 4 ⊢ (𝑥 = 𝐶 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦))) |
6 | 3, 5 | bibi12d 346 | . . 3 ⊢ (𝑥 = 𝐶 → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝐶𝑅𝑦 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦)))) |
7 | breq2 5153 | . . . 4 ⊢ (𝑦 = 𝐷 → (𝐶𝑅𝑦 ↔ 𝐶𝑅𝐷)) | |
8 | fveq2 6892 | . . . . 5 ⊢ (𝑦 = 𝐷 → (𝐻‘𝑦) = (𝐻‘𝐷)) | |
9 | 8 | breq2d 5161 | . . . 4 ⊢ (𝑦 = 𝐷 → ((𝐻‘𝐶)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))) |
10 | 7, 9 | bibi12d 346 | . . 3 ⊢ (𝑦 = 𝐷 → ((𝐶𝑅𝑦 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦)) ↔ (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))) |
11 | 6, 10 | rspc2v 3623 | . 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))) |
12 | 2, 11 | mpan9 508 | 1 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3062 class class class wbr 5149 –1-1-onto→wf1o 6543 ‘cfv 6544 Isom wiso 6545 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-iota 6496 df-fv 6552 df-isom 6553 |
This theorem is referenced by: soisores 7324 isomin 7334 isoini 7335 isopolem 7342 isosolem 7344 weniso 7351 smoiso 8362 supisolem 9468 ordiso2 9510 cantnflt 9667 cantnfp1lem3 9675 cantnflem1b 9681 cantnflem1 9684 wemapwe 9692 cnfcomlem 9694 cnfcom 9695 cnfcom3lem 9698 fpwwe2lem5 10630 fpwwe2lem6 10631 fpwwe2lem8 10633 leisorel 14421 seqcoll 14425 seqcoll2 14426 isercoll 15614 ordthmeolem 23305 iccpnfhmeo 24461 xrhmeo 24462 dvcnvrelem1 25534 dvcvx 25537 isoun 31923 erdszelem8 34189 erdsze2lem2 34195 cantnfresb 42074 fourierdlem20 44843 fourierdlem46 44868 fourierdlem50 44872 fourierdlem63 44885 fourierdlem64 44886 fourierdlem65 44887 fourierdlem76 44898 fourierdlem79 44901 fourierdlem102 44924 fourierdlem103 44925 fourierdlem104 44926 fourierdlem114 44936 |
Copyright terms: Public domain | W3C validator |