![]() |
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 5024 | . 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦)))) | |
2 | 1 | simplbi 268 | 1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 ∀wral 2359 class class class wbr 3845 –1-1-onto→wf1o 5014 ‘cfv 5015 Isom wiso 5016 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 df-isom 5024 |
This theorem is referenced by: isocnv2 5591 isores1 5593 isoini 5597 isoini2 5598 isoselem 5599 isose 5600 isopolem 5601 isosolem 5603 smoiso 6067 isotilem 6701 supisolem 6703 supisoex 6704 supisoti 6705 ordiso2 6728 leisorel 10242 zfz1isolemiso 10244 iseqcoll 10247 isummolem2a 10771 |
Copyright terms: Public domain | W3C validator |