Theorem isof1o 5851

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2472   class class class wbr 4030  –1-1-onto→wf1o 5254  ‘cfv 5255   Isom wiso 5256

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 5264

This theorem is referenced by:  isocnv2  5856  isores1  5858  isoini  5862  isoini2  5863  isoselem  5864  isose  5865  isopolem  5866  isosolem  5868  smoiso  6357  isotilem  7067  supisolem  7069  supisoex  7070  supisoti  7071  ordiso2  7096  leisorel  10911  zfz1isolemiso  10913  seq3coll  10916  summodclem2a  11527  prodmodclem2a  11722