Theorem isof1o 6573

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

Syntax hints:   → wi 4   ↔ wb 196  ∀wral 2912   class class class wbr 4653  –1-1-onto→wf1o 5887  ‘cfv 5888   Isom wiso 5889

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 197  df-an 386  df-isom 5897

This theorem is referenced by:  isores1  6584  isomin  6587  isoini  6588  isoini2  6589  isofrlem  6590  isoselem  6591  isofr  6592  isose  6593  isofr2  6594  isopolem  6595  isosolem  6597  weniso  6604  weisoeq  6605  weisoeq2  6606  wemoiso  7153  wemoiso2  7154  smoiso  7459  smoiso2  7466  supisolem  8379  supisoex  8380  supiso  8381  ordiso2  8420  ordtypelem10  8432  oiexg  8440  oien  8443  oismo  8445  cantnfle  8568  cantnflt2  8570  cantnfp1lem3  8577  cantnflem1b  8583  cantnflem1d  8585  cantnflem1  8586  cantnffval2  8592  cantnff1o  8593  wemapwe  8594  cnfcom3lem  8600  infxpenlem  8836  iunfictbso  8937  dfac12lem2  8966  cofsmo  9091  isf34lem3  9197  isf34lem5  9200  hsmexlem1  9248  fpwwe2lem6  9457  fpwwe2lem7  9458  fpwwe2lem9  9460  pwfseqlem5  9485  fz1isolem  13245  seqcoll  13248  seqcoll2  13249  isercolllem2  14396  isercoll  14398  summolem2a  14446  prodmolem2a  14664  gsumval3lem1  18306  gsumval3  18308  ordthmeolem  21604  dvne0f1  23775  dvcvx  23783  isoun  29479  erdsze2lem1  31185  fourierdlem20  40344  fourierdlem50  40373  fourierdlem51  40374  fourierdlem52  40375  fourierdlem63  40386  fourierdlem64  40387  fourierdlem65  40388  fourierdlem76  40399  fourierdlem102  40425  fourierdlem114  40437