Theorem isof1o 5937

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 5327	. 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 4083  –1-1-onto→wf1o 5317  ‘cfv 5318   Isom wiso 5319

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 5327

This theorem is referenced by:  isocnv2  5942  isores1  5944  isoini  5948  isoini2  5949  isoselem  5950  isose  5951  isopolem  5952  isosolem  5954  smoiso  6454  isotilem  7181  supisolem  7183  supisoex  7184  supisoti  7185  ordiso2  7210  leisorel  11067  zfz1isolemiso  11069  seq3coll  11072  summodclem2a  11900  prodmodclem2a  12095