Theorem isof1o 5924

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2508   class class class wbr 4082  –1-1-onto→wf1o 5313  ‘cfv 5314   Isom wiso 5315

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 5323

This theorem is referenced by:  isocnv2  5929  isores1  5931  isoini  5935  isoini2  5936  isoselem  5937  isose  5938  isopolem  5939  isosolem  5941  smoiso  6438  isotilem  7161  supisolem  7163  supisoex  7164  supisoti  7165  ordiso2  7190  leisorel  11046  zfz1isolemiso  11048  seq3coll  11051  summodclem2a  11878  prodmodclem2a  12073