Theorem isof1o 5958

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2511   class class class wbr 4093  –1-1-onto→wf1o 5332  ‘cfv 5333   Isom wiso 5334

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 5342

This theorem is referenced by:  isocnv2  5963  isores1  5965  isoini  5969  isoini2  5970  isoselem  5971  isose  5972  isopolem  5973  isosolem  5975  smoiso  6511  isotilem  7248  supisolem  7250  supisoex  7251  supisoti  7252  ordiso2  7277  leisorel  11147  zfz1isolemiso  11149  seq3coll  11152  summodclem2a  12005  prodmodclem2a  12200