Theorem isof1o 5586

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

Syntax hints:   → wi 4   ↔ wb 103  ∀wral 2359   class class class wbr 3845  –1-1-onto→wf1o 5014  ‘cfv 5015   Isom wiso 5016

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

This theorem depends on definitions:  df-bi 115  df-isom 5024

This theorem is referenced by:  isocnv2  5591  isores1  5593  isoini  5597  isoini2  5598  isoselem  5599  isose  5600  isopolem  5601  isosolem  5603  smoiso  6067  isotilem  6701  supisolem  6703  supisoex  6704  supisoti  6705  ordiso2  6728  leisorel  10242  zfz1isolemiso  10244  iseqcoll  10247  isummolem2a  10771