![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isoeq1 | Structured version Visualization version GIF version |
Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
Ref | Expression |
---|---|
isoeq1 | ⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oeq1 6818 | . . 3 ⊢ (𝐻 = 𝐺 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐺:𝐴–1-1-onto→𝐵)) | |
2 | fveq1 6887 | . . . . . 6 ⊢ (𝐻 = 𝐺 → (𝐻‘𝑥) = (𝐺‘𝑥)) | |
3 | fveq1 6887 | . . . . . 6 ⊢ (𝐻 = 𝐺 → (𝐻‘𝑦) = (𝐺‘𝑦)) | |
4 | 2, 3 | breq12d 5160 | . . . . 5 ⊢ (𝐻 = 𝐺 → ((𝐻‘𝑥)𝑆(𝐻‘𝑦) ↔ (𝐺‘𝑥)𝑆(𝐺‘𝑦))) |
5 | 4 | bibi2d 343 | . . . 4 ⊢ (𝐻 = 𝐺 → ((𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ (𝑥𝑅𝑦 ↔ (𝐺‘𝑥)𝑆(𝐺‘𝑦)))) |
6 | 5 | 2ralbidv 3219 | . . 3 ⊢ (𝐻 = 𝐺 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐺‘𝑥)𝑆(𝐺‘𝑦)))) |
7 | 1, 6 | anbi12d 632 | . 2 ⊢ (𝐻 = 𝐺 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐺:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐺‘𝑥)𝑆(𝐺‘𝑦))))) |
8 | df-isom 6549 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
9 | df-isom 6549 | . 2 ⊢ (𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐺:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐺‘𝑥)𝑆(𝐺‘𝑦)))) | |
10 | 7, 8, 9 | 3bitr4g 314 | 1 ⊢ (𝐻 = 𝐺 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐺 Isom 𝑅, 𝑆 (𝐴, 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 = wceq 1542 ∀wral 3062 class class class wbr 5147 –1-1-onto→wf1o 6539 ‘cfv 6540 Isom wiso 6541 |
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 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 |
This theorem is referenced by: isores1 7326 wemoiso 7955 wemoiso2 7956 ordiso 9507 oieu 9530 finnisoeu 10104 iunfictbso 10105 infrenegsup 12193 ltweuz 13922 fz1isolem 14418 isercolllem2 15608 isercoll 15610 dvgt0lem2 25502 efcvx 25943 relogiso 26088 logccv 26153 erdszelem1 34120 erdsze 34131 erdsze2lem2 34133 isoeq145d 42103 fzisoeu 43945 fourierdlem36 44794 fourierdlem96 44853 fourierdlem97 44854 fourierdlem98 44855 fourierdlem99 44856 fourierdlem105 44862 fourierdlem106 44863 fourierdlem108 44865 fourierdlem110 44867 fourierdlem112 44869 fourierdlem113 44870 fourierdlem115 44872 rrx2plordisom 47311 |
Copyright terms: Public domain | W3C validator |