Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > isoeq4 | Structured version Visualization version GIF version |
Description: Equality theorem for isomorphisms. (Contributed by NM, 17-May-2004.) |
Ref | Expression |
---|---|
isoeq4 | ⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oeq2 6607 | . . 3 ⊢ (𝐴 = 𝐶 → (𝐻:𝐴–1-1-onto→𝐵 ↔ 𝐻:𝐶–1-1-onto→𝐵)) | |
2 | raleq 3407 | . . . 4 ⊢ (𝐴 = 𝐶 → (∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
3 | 2 | raleqbi1dv 3405 | . . 3 ⊢ (𝐴 = 𝐶 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)) ↔ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) |
4 | 1, 3 | anbi12d 632 | . 2 ⊢ (𝐴 = 𝐶 → ((𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))) ↔ (𝐻:𝐶–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))) |
5 | df-isom 6366 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
6 | df-isom 6366 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵) ↔ (𝐻:𝐶–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐶 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
7 | 4, 5, 6 | 3bitr4g 316 | 1 ⊢ (𝐴 = 𝐶 → (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ 𝐻 Isom 𝑅, 𝑆 (𝐶, 𝐵))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1537 ∀wral 3140 class class class wbr 5068 –1-1-onto→wf1o 6356 ‘cfv 6357 Isom wiso 6358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-ext 2795 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-cleq 2816 df-clel 2895 df-ral 3145 df-fn 6360 df-f 6361 df-f1 6362 df-fo 6363 df-f1o 6364 df-isom 6366 |
This theorem is referenced by: oieu 9005 oiid 9007 finnisoeu 9541 iunfictbso 9542 fz1isolem 13822 isercolllem3 15025 summolem2a 15074 prodmolem2a 15290 erdszelem1 32440 erdsze 32451 erdsze2lem1 32452 erdsze2lem2 32453 fzisoeu 41574 fourierdlem36 42435 fourierdlem112 42510 fourierdlem113 42511 |
Copyright terms: Public domain | W3C validator |