Theorem isof1o 5888

Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)

Assertion

Ref	Expression
isof1o	⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)

Proof of Theorem isof1o

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-isom 5288	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
2	1	simplbi 274	1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2485   class class class wbr 4050  –1-1-onto→wf1o 5278  ‘cfv 5279   Isom wiso 5280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-isom 5288

This theorem is referenced by:  isocnv2  5893  isores1  5895  isoini  5899  isoini2  5900  isoselem  5901  isose  5902  isopolem  5903  isosolem  5905  smoiso  6400  isotilem  7122  supisolem  7124  supisoex  7125  supisoti  7126  ordiso2  7151  leisorel  10999  zfz1isolemiso  11001  seq3coll  11004  summodclem2a  11762  prodmodclem2a  11957