Theorem isof1o 7324

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3076   class class class wbr 5103  –1-1-onto→wf1o 6532  ‘cfv 6533   Isom wiso 6534

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-isom 6542

This theorem is used by:  isores1  7335  isomin  7338  isoini  7339  isoini2  7340  isofrlem  7341  isoselem  7342  isofr  7343  isose  7344  isofr2  7345  isopolem  7346  isosolem  7348  weniso  7357  weisoeq  7358  weisoeq2  7359  wemoiso  7970  wemoiso2  7971  smoiso  8351  smoiso2  8358  supisolem  9444  supisoex  9445  supiso  9446  ordiso2  9487  ordtypelem10  9499  oiexg  9507  oien  9510  oismo  9512  cantnfle  9650  cantnflt2  9652  cantnfp1lem3  9659  cantnflem1b  9665  cantnflem1d  9667  cantnflem1  9668  cantnffval2  9674  cantnff1o  9675  wemapwe  9676  cnfcom3lem  9682  infxpenlem  10016  iunfictbso  10117  dfac12lem2  10147  cofsmo  10271  isf34lem3  10377  isf34lem5  10380  hsmexlem1  10428  fpwwe2lem5  10644  fpwwe2lem6  10645  fpwwe2lem8  10647  pwfseqlem5  10672  fz1isolem  14526  seqcoll  14529  seqcoll2  14530  isercolllem2  15753  isercoll  15755  summolem2a  15801  prodmolem2a  16021  gsumval3lem1  20032  gsumval3  20034  ordthmeolem  24027  dvne0f1  26239  dvcvx  26247  addonbday  28544  isoun  33174  nsgqusf1o  33845  ordtypeon  35595  wevonprcf1o  35710  erdsze2lem1  35782  fourierdlem20  46955  fourierdlem50  46984  fourierdlem51  46985  fourierdlem52  46986  fourierdlem63  46997  fourierdlem64  46998  fourierdlem65  46999  fourierdlem76  47010  fourierdlem102  47036  fourierdlem114  47048