Theorem isof1o 6016

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105  ∀wral 2528   class class class wbr 4131  –1-1-onto→wf1o 5379  ‘cfv 5380   Isom wiso 5381

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-isom 5389

This theorem is used by:  isocnv2  6021  isores1  6023  isoini  6027  isoini2  6028  isoselem  6029  isose  6030  isopolem  6031  isosolem  6033  smoiso  6577  isotilem  7352  supisolem  7354  supisoex  7355  supisoti  7356  ordiso2  7381  leisorel  11311  zfz1isolemiso  11313  seq3coll  11316  summodclem2a  12173  prodmodclem2a  12368