Theorem isof1o 5899

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2486   class class class wbr 4059  –1-1-onto→wf1o 5289  ‘cfv 5290   Isom wiso 5291

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 5299

This theorem is referenced by:  isocnv2  5904  isores1  5906  isoini  5910  isoini2  5911  isoselem  5912  isose  5913  isopolem  5914  isosolem  5916  smoiso  6411  isotilem  7134  supisolem  7136  supisoex  7137  supisoti  7138  ordiso2  7163  leisorel  11019  zfz1isolemiso  11021  seq3coll  11024  summodclem2a  11807  prodmodclem2a  12002