Theorem isof1o 6802

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

Syntax hints:   → wi 4   ↔ wb 198  ∀wral 3090   class class class wbr 4844  –1-1-onto→wf1o 6101  ‘cfv 6102   Isom wiso 6103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199  df-an 386  df-isom 6111

This theorem is referenced by:  isores1  6813  isomin  6816  isoini  6817  isoini2  6818  isofrlem  6819  isoselem  6820  isofr  6821  isose  6822  isofr2  6823  isopolem  6824  isosolem  6826  weniso  6833  weisoeq  6834  weisoeq2  6835  wemoiso  7387  wemoiso2  7388  smoiso  7699  smoiso2  7706  supisolem  8622  supisoex  8623  supiso  8624  ordiso2  8663  ordtypelem10  8675  oiexg  8683  oien  8686  oismo  8688  cantnfle  8819  cantnflt2  8821  cantnfp1lem3  8828  cantnflem1b  8834  cantnflem1d  8836  cantnflem1  8837  cantnffval2  8843  cantnff1o  8844  wemapwe  8845  cnfcom3lem  8851  infxpenlem  9123  iunfictbso  9224  dfac12lem2  9255  cofsmo  9380  isf34lem3  9486  isf34lem5  9489  hsmexlem1  9537  fpwwe2lem6  9746  fpwwe2lem7  9747  fpwwe2lem9  9749  pwfseqlem5  9774  fz1isolem  13493  seqcoll  13496  seqcoll2  13497  isercolllem2  14736  isercoll  14738  summolem2a  14786  prodmolem2a  15000  gsumval3lem1  18620  gsumval3  18622  ordthmeolem  21932  dvne0f1  24115  dvcvx  24123  isoun  29996  erdsze2lem1  31701  fourierdlem20  41082  fourierdlem50  41111  fourierdlem51  41112  fourierdlem52  41113  fourierdlem63  41124  fourierdlem64  41125  fourierdlem65  41126  fourierdlem76  41137  fourierdlem102  41163  fourierdlem114  41175