| 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 6501 | . 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 3054 class class class wbr 5079 –1-1-onto→wf1o 6491 ‘cfv 6492 Isom wiso 6493 |
| 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 6501 |
| This theorem is referenced by: isores1 7285 isomin 7288 isoini 7289 isoini2 7290 isofrlem 7291 isoselem 7292 isofr 7293 isose 7294 isofr2 7295 isopolem 7296 isosolem 7298 weniso 7305 weisoeq 7306 weisoeq2 7307 wemoiso 7922 wemoiso2 7923 smoiso 8299 smoiso2 8306 supisolem 9384 supisoex 9385 supiso 9386 ordiso2 9427 ordtypelem10 9439 oiexg 9447 oien 9450 oismo 9452 cantnfle 9590 cantnflt2 9592 cantnfp1lem3 9599 cantnflem1b 9605 cantnflem1d 9607 cantnflem1 9608 cantnffval2 9614 cantnff1o 9615 wemapwe 9616 cnfcom3lem 9622 infxpenlem 9933 iunfictbso 10034 dfac12lem2 10065 cofsmo 10189 isf34lem3 10295 isf34lem5 10298 hsmexlem1 10346 fpwwe2lem5 10556 fpwwe2lem6 10557 fpwwe2lem8 10559 pwfseqlem5 10584 fz1isolem 14421 seqcoll 14424 seqcoll2 14425 isercolllem2 15626 isercoll 15628 summolem2a 15675 prodmolem2a 15897 gsumval3lem1 19878 gsumval3 19880 ordthmeolem 23791 dvne0f1 26004 dvcvx 26012 addonbday 28296 isoun 32801 nsgqusf1o 33506 erdsze2lem1 35438 fourierdlem20 46577 fourierdlem50 46606 fourierdlem51 46607 fourierdlem52 46608 fourierdlem63 46619 fourierdlem64 46620 fourierdlem65 46621 fourierdlem76 46632 fourierdlem102 46658 fourierdlem114 46670 |
| Copyright terms: Public domain | W3C validator |