![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > isoeq5 | Structured version Visualization version GIF version |
Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
Ref | Expression |
---|---|
isoeq5 | ⊢ (𝐵 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oeq3 6824 | . . 3 ⊢ (𝐵 = 𝐶 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻:𝐴–1-1-onto→𝐶)) | |
2 | 1 | anbi1d 631 | . 2 ⊢ (𝐵 = 𝐶 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))) |
3 | df-isom 6553 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
4 | df-isom 6553 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐶) ↔ (𝐻:𝐴–1-1-onto→𝐶 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
5 | 2, 3, 4 | 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 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-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-v 3477 df-in 3956 df-ss 3966 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-isom 6553 |
This theorem is referenced by: isores3 7332 ordiso 9511 ordtypelem9 9521 ordtypelem10 9522 oiid 9536 iunfictbso 10109 ltweuz 13926 fz1isolem 14422 dvgt0lem2 25520 erdszelem1 34182 erdsze 34193 erdsze2lem1 34194 erdsze2lem2 34195 isoeq145d 42170 alephiso3 42310 fourierdlem50 44872 fourierdlem89 44911 fourierdlem90 44912 fourierdlem91 44913 fourierdlem96 44918 fourierdlem97 44919 fourierdlem98 44920 fourierdlem99 44921 fourierdlem100 44922 fourierdlem108 44930 fourierdlem110 44932 fourierdlem112 44934 fourierdlem113 44935 |
Copyright terms: Public domain | W3C validator |