Theorem isof1o 6013

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∀wral 2528   class class class wbr 4130  –1-1-onto→wf1o 5376  ‘cfv 5377   Isom wiso 5378

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-isom 5386

This theorem is used by:  isocnv2  6018  isores1  6020  isoini  6024  isoini2  6025  isoselem  6026  isose  6027  isopolem  6028  isosolem  6030  smoiso  6573  isotilem  7346  supisolem  7348  supisoex  7349  supisoti  7350  ordiso2  7375  leisorel  11289  zfz1isolemiso  11291  seq3coll  11294  summodclem2a  12148  prodmodclem2a  12343