| 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 6570 | . 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 206 ∀wral 3061 class class class wbr 5143 –1-1-onto→wf1o 6560 ‘cfv 6561 Isom wiso 6562 |
| 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 207 df-an 396 df-isom 6570 |
| This theorem is referenced by: isores1 7354 isomin 7357 isoini 7358 isoini2 7359 isofrlem 7360 isoselem 7361 isofr 7362 isose 7363 isofr2 7364 isopolem 7365 isosolem 7367 weniso 7374 weisoeq 7375 weisoeq2 7376 wemoiso 7998 wemoiso2 7999 smoiso 8402 smoiso2 8409 supisolem 9513 supisoex 9514 supiso 9515 ordiso2 9555 ordtypelem10 9567 oiexg 9575 oien 9578 oismo 9580 cantnfle 9711 cantnflt2 9713 cantnfp1lem3 9720 cantnflem1b 9726 cantnflem1d 9728 cantnflem1 9729 cantnffval2 9735 cantnff1o 9736 wemapwe 9737 cnfcom3lem 9743 infxpenlem 10053 iunfictbso 10154 dfac12lem2 10185 cofsmo 10309 isf34lem3 10415 isf34lem5 10418 hsmexlem1 10466 fpwwe2lem5 10675 fpwwe2lem6 10676 fpwwe2lem8 10678 pwfseqlem5 10703 fz1isolem 14500 seqcoll 14503 seqcoll2 14504 isercolllem2 15702 isercoll 15704 summolem2a 15751 prodmolem2a 15970 gsumval3lem1 19923 gsumval3 19925 ordthmeolem 23809 dvne0f1 26051 dvcvx 26059 isoun 32711 nsgqusf1o 33444 erdsze2lem1 35208 fourierdlem20 46142 fourierdlem50 46171 fourierdlem51 46172 fourierdlem52 46173 fourierdlem63 46184 fourierdlem64 46185 fourierdlem65 46186 fourierdlem76 46197 fourierdlem102 46223 fourierdlem114 46235 |
| Copyright terms: Public domain | W3C validator |