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 5813 | . . 3 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
2 | 1 | simprbi 479 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) |
3 | breq1 4586 | . . . 4 ⊢ (𝑥 = 𝐶 → (𝑥𝑅𝑦 ↔ 𝐶𝑅𝑦)) | |
4 | fveq2 6103 | . . . . 5 ⊢ (𝑥 = 𝐶 → (𝐻‘𝑥) = (𝐻‘𝐶)) | |
5 | 4 | breq1d 4593 | . . . 4 ⊢ (𝑥 = 𝐶 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦))) |
6 | 3, 5 | bibi12d 334 | . . 3 ⊢ (𝑥 = 𝐶 → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝐶𝑅𝑦 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦)))) |
7 | breq2 4587 | . . . 4 ⊢ (𝑦 = 𝐷 → (𝐶𝑅𝑦 ↔ 𝐶𝑅𝐷)) | |
8 | fveq2 6103 | . . . . 5 ⊢ (𝑦 = 𝐷 → (𝐻‘𝑦) = (𝐻‘𝐷)) | |
9 | 8 | breq2d 4595 | . . . 4 ⊢ (𝑦 = 𝐷 → ((𝐻‘𝐶)𝑆(𝐻‘𝑦) ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))) |
10 | 7, 9 | bibi12d 334 | . . 3 ⊢ (𝑦 = 𝐷 → ((𝐶𝑅𝑦 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝑦)) ↔ (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))) |
11 | 6, 10 | rspc2v 3293 | . 2 ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷)))) |
12 | 2, 11 | mpan9 485 | 1 ⊢ ((𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 ↔ (𝐻‘𝐶)𝑆(𝐻‘𝐷))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∀wral 2896 class class class wbr 4583 –1-1-onto→wf1o 5803 ‘cfv 5804 Isom wiso 5805 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-br 4584 df-iota 5768 df-fv 5812 df-isom 5813 |
This theorem is referenced by: soisores 6477 isomin 6487 isoini 6488 isopolem 6495 isosolem 6497 weniso 6504 smoiso 7346 supisolem 8262 ordiso2 8303 cantnflt 8452 cantnfp1lem3 8460 cantnflem1b 8466 cantnflem1 8469 wemapwe 8477 cnfcomlem 8479 cnfcom 8480 cnfcom3lem 8483 fpwwe2lem6 9336 fpwwe2lem7 9337 fpwwe2lem9 9339 leisorel 13101 seqcoll 13105 seqcoll2 13106 isercoll 14246 ordthmeolem 21414 iccpnfhmeo 22552 xrhmeo 22553 dvcnvrelem1 23584 dvcvx 23587 isoun 28862 erdszelem8 30434 erdsze2lem2 30440 fourierdlem20 39020 fourierdlem46 39045 fourierdlem50 39049 fourierdlem63 39062 fourierdlem64 39063 fourierdlem65 39064 fourierdlem76 39075 fourierdlem79 39078 fourierdlem102 39101 fourierdlem103 39102 fourierdlem104 39103 fourierdlem114 39113 |
Copyright terms: Public domain | W3C validator |