Theorem isof1o 5988

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2522   class class class wbr 4115  –1-1-onto→wf1o 5358  ‘cfv 5359   Isom wiso 5360

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 5368

This theorem is referenced by:  isocnv2  5993  isores1  5995  isoini  5999  isoini2  6000  isoselem  6001  isose  6002  isopolem  6003  isosolem  6005  smoiso  6548  isotilem  7312  supisolem  7314  supisoex  7315  supisoti  7316  ordiso2  7341  leisorel  11239  zfz1isolemiso  11241  seq3coll  11244  summodclem2a  12098  prodmodclem2a  12293