Theorem isof1o 5600

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

Syntax hints:   → wi 4   ↔ wb 104  ∀wral 2360   class class class wbr 3851  –1-1-onto→wf1o 5027  ‘cfv 5028   Isom wiso 5029

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

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

This theorem is referenced by:  isocnv2  5605  isores1  5607  isoini  5611  isoini2  5612  isoselem  5613  isose  5614  isopolem  5615  isosolem  5617  smoiso  6081  isotilem  6755  supisolem  6757  supisoex  6758  supisoti  6759  ordiso2  6782  leisorel  10303  zfz1isolemiso  10305  iseqcoll  10308  isummolem2a  10832