Theorem isof1o 7252

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3047   class class class wbr 5086  –1-1-onto→wf1o 6475  ‘cfv 6476   Isom wiso 6477

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 207  df-an 396  df-isom 6485

This theorem is referenced by:  isores1  7263  isomin  7266  isoini  7267  isoini2  7268  isofrlem  7269  isoselem  7270  isofr  7271  isose  7272  isofr2  7273  isopolem  7274  isosolem  7276  weniso  7283  weisoeq  7284  weisoeq2  7285  wemoiso  7900  wemoiso2  7901  smoiso  8277  smoiso2  8284  supisolem  9353  supisoex  9354  supiso  9355  ordiso2  9396  ordtypelem10  9408  oiexg  9416  oien  9419  oismo  9421  cantnfle  9556  cantnflt2  9558  cantnfp1lem3  9565  cantnflem1b  9571  cantnflem1d  9573  cantnflem1  9574  cantnffval2  9580  cantnff1o  9581  wemapwe  9582  cnfcom3lem  9588  infxpenlem  9899  iunfictbso  10000  dfac12lem2  10031  cofsmo  10155  isf34lem3  10261  isf34lem5  10264  hsmexlem1  10312  fpwwe2lem5  10521  fpwwe2lem6  10522  fpwwe2lem8  10524  pwfseqlem5  10549  fz1isolem  14363  seqcoll  14366  seqcoll2  14367  isercolllem2  15568  isercoll  15570  summolem2a  15617  prodmolem2a  15836  gsumval3lem1  19812  gsumval3  19814  ordthmeolem  23711  dvne0f1  25939  dvcvx  25947  isoun  32675  nsgqusf1o  33373  erdsze2lem1  35239  fourierdlem20  46165  fourierdlem50  46194  fourierdlem51  46195  fourierdlem52  46196  fourierdlem63  46207  fourierdlem64  46208  fourierdlem65  46209  fourierdlem76  46220  fourierdlem102  46246  fourierdlem114  46258