Theorem isof1o 5943

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2508   class class class wbr 4086  –1-1-onto→wf1o 5323  ‘cfv 5324   Isom wiso 5325

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 5333

This theorem is referenced by:  isocnv2  5948  isores1  5950  isoini  5954  isoini2  5955  isoselem  5956  isose  5957  isopolem  5958  isosolem  5960  smoiso  6463  isotilem  7196  supisolem  7198  supisoex  7199  supisoti  7200  ordiso2  7225  leisorel  11091  zfz1isolemiso  11093  seq3coll  11096  summodclem2a  11932  prodmodclem2a  12127