Theorem isof1o 5947

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

Syntax hints:   → wi 4   ↔ wb 105  ∀wral 2510   class class class wbr 4088  –1-1-onto→wf1o 5325  ‘cfv 5326   Isom wiso 5327

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 5335

This theorem is referenced by:  isocnv2  5952  isores1  5954  isoini  5958  isoini2  5959  isoselem  5960  isose  5961  isopolem  5962  isosolem  5964  smoiso  6467  isotilem  7204  supisolem  7206  supisoex  7207  supisoti  7208  ordiso2  7233  leisorel  11100  zfz1isolemiso  11102  seq3coll  11105  summodclem2a  11941  prodmodclem2a  12136