![]() |
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 6132 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
2 | 1 | simplbi 493 | 1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∀wral 3117 class class class wbr 4873 –1-1-onto→wf1o 6122 ‘cfv 6123 Isom wiso 6124 |
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 199 df-an 387 df-isom 6132 |
This theorem is referenced by: isores1 6839 isomin 6842 isoini 6843 isoini2 6844 isofrlem 6845 isoselem 6846 isofr 6847 isose 6848 isofr2 6849 isopolem 6850 isosolem 6852 weniso 6859 weisoeq 6860 weisoeq2 6861 wemoiso 7413 wemoiso2 7414 smoiso 7725 smoiso2 7732 supisolem 8648 supisoex 8649 supiso 8650 ordiso2 8689 ordtypelem10 8701 oiexg 8709 oien 8712 oismo 8714 cantnfle 8845 cantnflt2 8847 cantnfp1lem3 8854 cantnflem1b 8860 cantnflem1d 8862 cantnflem1 8863 cantnffval2 8869 cantnff1o 8870 wemapwe 8871 cnfcom3lem 8877 infxpenlem 9149 iunfictbso 9250 dfac12lem2 9281 cofsmo 9406 isf34lem3 9512 isf34lem5 9515 hsmexlem1 9563 fpwwe2lem6 9772 fpwwe2lem7 9773 fpwwe2lem9 9775 pwfseqlem5 9800 fz1isolem 13534 seqcoll 13537 seqcoll2 13538 isercolllem2 14773 isercoll 14775 summolem2a 14823 prodmolem2a 15037 gsumval3lem1 18659 gsumval3 18661 ordthmeolem 21975 dvne0f1 24174 dvcvx 24182 isoun 30027 erdsze2lem1 31731 fourierdlem20 41138 fourierdlem50 41167 fourierdlem51 41168 fourierdlem52 41169 fourierdlem63 41180 fourierdlem64 41181 fourierdlem65 41182 fourierdlem76 41193 fourierdlem102 41219 fourierdlem114 41231 |
Copyright terms: Public domain | W3C validator |