![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > isof1o | 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 5037 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
2 | 1 | simplbi 269 | 1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wral 2360 class class class wbr 3851 –1-1-onto→wf1o 5027 ‘cfv 5028 Isom wiso 5029 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-isom 5037 |
This theorem is referenced by: isocnv2 5605 isores1 5607 isoini 5611 isoini2 5612 isoselem 5613 isose 5614 isopolem 5615 isosolem 5617 smoiso 6081 isotilem 6755 supisolem 6757 supisoex 6758 supisoti 6759 ordiso2 6782 leisorel 10303 zfz1isolemiso 10305 iseqcoll 10308 isummolem2a 10832 |
Copyright terms: Public domain | W3C validator |