Theorem isof1o 5857

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2475   class class class wbr 4034  –1-1-onto→wf1o 5258  ‘cfv 5259   Isom wiso 5260

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 5268

This theorem is referenced by:  isocnv2  5862  isores1  5864  isoini  5868  isoini2  5869  isoselem  5870  isose  5871  isopolem  5872  isosolem  5874  smoiso  6369  isotilem  7081  supisolem  7083  supisoex  7084  supisoti  7085  ordiso2  7110  leisorel  10946  zfz1isolemiso  10948  seq3coll  10951  summodclem2a  11563  prodmodclem2a  11758