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 5207 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
2 | 1 | simplbi 272 | 1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wral 2448 class class class wbr 3989 –1-1-onto→wf1o 5197 ‘cfv 5198 Isom wiso 5199 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-isom 5207 |
This theorem is referenced by: isocnv2 5791 isores1 5793 isoini 5797 isoini2 5798 isoselem 5799 isose 5800 isopolem 5801 isosolem 5803 smoiso 6281 isotilem 6983 supisolem 6985 supisoex 6986 supisoti 6987 ordiso2 7012 leisorel 10772 zfz1isolemiso 10774 seq3coll 10777 summodclem2a 11344 prodmodclem2a 11539 |
Copyright terms: Public domain | W3C validator |