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  7347  supisolem  7349  supisoex  7350  supisoti  7351  ordiso2  7376  leisorel  11305  zfz1isolemiso  11307  seq3coll  11310  summodclem2a  12167  prodmodclem2a  12362