Theorem isof1o 5784

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wral 2448   class class class wbr 3987  –1-1-onto→wf1o 5195  ‘cfv 5196   Isom wiso 5197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116  df-isom 5205

This theorem is referenced by:  isocnv2  5789  isores1  5791  isoini  5795  isoini2  5796  isoselem  5797  isose  5798  isopolem  5799  isosolem  5801  smoiso  6279  isotilem  6981  supisolem  6983  supisoex  6984  supisoti  6985  ordiso2  7010  leisorel  10765  zfz1isolemiso  10767  seq3coll  10770  summodclem2a  11337  prodmodclem2a  11532