Theorem isof1o 5769

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wral 2442   class class class wbr 3976  –1-1-onto→wf1o 5181  ‘cfv 5182   Isom wiso 5183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-isom 5191

This theorem is referenced by:  isocnv2  5774  isores1  5776  isoini  5780  isoini2  5781  isoselem  5782  isose  5783  isopolem  5784  isosolem  5786  smoiso  6261  isotilem  6962  supisolem  6964  supisoex  6965  supisoti  6966  ordiso2  6991  leisorel  10736  zfz1isolemiso  10738  seq3coll  10741  summodclem2a  11308  prodmodclem2a  11503