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 5205 | . 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 3987 –1-1-onto→wf1o 5195 ‘cfv 5196 Isom wiso 5197 |
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 5205 |
This theorem is referenced by: isocnv2 5789 isores1 5791 isoini 5795 isoini2 5796 isoselem 5797 isose 5798 isopolem 5799 isosolem 5801 smoiso 6279 isotilem 6981 supisolem 6983 supisoex 6984 supisoti 6985 ordiso2 7010 leisorel 10765 zfz1isolemiso 10767 seq3coll 10770 summodclem2a 11337 prodmodclem2a 11532 |
Copyright terms: Public domain | W3C validator |