| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > isof1o | Structured version Visualization version GIF version | ||
| Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.) |
| Ref | Expression |
|---|---|
| isof1o | ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-isom 6494 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
| 2 | 1 | simplbi 497 | 1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 207 ∀wral 3053 class class class wbr 5072 –1-1-onto→wf1o 6484 ‘cfv 6485 Isom wiso 6486 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 208 df-an 397 df-isom 6494 |
| This theorem is referenced by: isores1 7278 isomin 7281 isoini 7282 isoini2 7283 isofrlem 7284 isoselem 7285 isofr 7286 isose 7287 isofr2 7288 isopolem 7289 isosolem 7291 weniso 7298 weisoeq 7299 weisoeq2 7300 wemoiso 7915 wemoiso2 7916 smoiso 8292 smoiso2 8299 supisolem 9377 supisoex 9378 supiso 9379 ordiso2 9420 ordtypelem10 9432 oiexg 9440 oien 9443 oismo 9445 cantnfle 9583 cantnflt2 9585 cantnfp1lem3 9592 cantnflem1b 9598 cantnflem1d 9600 cantnflem1 9601 cantnffval2 9607 cantnff1o 9608 wemapwe 9609 cnfcom3lem 9615 infxpenlem 9926 iunfictbso 10027 dfac12lem2 10058 cofsmo 10182 isf34lem3 10288 isf34lem5 10291 hsmexlem1 10339 fpwwe2lem5 10549 fpwwe2lem6 10550 fpwwe2lem8 10552 pwfseqlem5 10577 fz1isolem 14414 seqcoll 14417 seqcoll2 14418 isercolllem2 15619 isercoll 15621 summolem2a 15668 prodmolem2a 15890 gsumval3lem1 19871 gsumval3 19873 ordthmeolem 23784 dvne0f1 25997 dvcvx 26005 addonbday 28289 isoun 32794 nsgqusf1o 33499 erdsze2lem1 35431 fourierdlem20 46570 fourierdlem50 46599 fourierdlem51 46600 fourierdlem52 46601 fourierdlem63 46612 fourierdlem64 46613 fourierdlem65 46614 fourierdlem76 46625 fourierdlem102 46651 fourierdlem114 46663 |
| Copyright terms: Public domain | W3C validator |