Theorem isof1o 5980

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 5361	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
2	1	simplbi 274	1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴–1-1-onto→𝐵)

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2520   class class class wbr 4109  –1-1-onto→wf1o 5351  ‘cfv 5352   Isom wiso 5353

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 5361

This theorem is referenced by:  isocnv2  5985  isores1  5987  isoini  5991  isoini2  5992  isoselem  5993  isose  5994  isopolem  5995  isosolem  5997  smoiso  6533  isotilem  7297  supisolem  7299  supisoex  7300  supisoti  7301  ordiso2  7326  leisorel  11209  zfz1isolemiso  11211  seq3coll  11214  summodclem2a  12067  prodmodclem2a  12262