![]() |
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 6558 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
2 | 1 | simplbi 496 | 1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wral 3050 class class class wbr 5149 –1-1-onto→wf1o 6548 ‘cfv 6549 Isom wiso 6550 |
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 206 df-an 395 df-isom 6558 |
This theorem is referenced by: isores1 7341 isomin 7344 isoini 7345 isoini2 7346 isofrlem 7347 isoselem 7348 isofr 7349 isose 7350 isofr2 7351 isopolem 7352 isosolem 7354 weniso 7361 weisoeq 7362 weisoeq2 7363 wemoiso 7978 wemoiso2 7979 smoiso 8383 smoiso2 8390 supisolem 9498 supisoex 9499 supiso 9500 ordiso2 9540 ordtypelem10 9552 oiexg 9560 oien 9563 oismo 9565 cantnfle 9696 cantnflt2 9698 cantnfp1lem3 9705 cantnflem1b 9711 cantnflem1d 9713 cantnflem1 9714 cantnffval2 9720 cantnff1o 9721 wemapwe 9722 cnfcom3lem 9728 infxpenlem 10038 iunfictbso 10139 dfac12lem2 10169 cofsmo 10294 isf34lem3 10400 isf34lem5 10403 hsmexlem1 10451 fpwwe2lem5 10660 fpwwe2lem6 10661 fpwwe2lem8 10663 pwfseqlem5 10688 fz1isolem 14458 seqcoll 14461 seqcoll2 14462 isercolllem2 15648 isercoll 15650 summolem2a 15697 prodmolem2a 15914 gsumval3lem1 19872 gsumval3 19874 ordthmeolem 23749 dvne0f1 25989 dvcvx 25997 isoun 32563 nsgqusf1o 33228 erdsze2lem1 34941 fourierdlem20 45650 fourierdlem50 45679 fourierdlem51 45680 fourierdlem52 45681 fourierdlem63 45692 fourierdlem64 45693 fourierdlem65 45694 fourierdlem76 45705 fourierdlem102 45731 fourierdlem114 45743 |
Copyright terms: Public domain | W3C validator |