Theorem isof1o 7327

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 6549	. 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 3081   class class class wbr 5111  –1-1-onto→wf1o 6539  ‘cfv 6540   Isom wiso 6541

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 6549

This theorem is used by:  isores1  7338  isomin  7341  isoini  7342  isoini2  7343  isofrlem  7344  isoselem  7345  isofr  7346  isose  7347  isofr2  7348  isopolem  7349  isosolem  7351  weniso  7360  weisoeq  7361  weisoeq2  7362  wemoiso  7972  wemoiso2  7973  smoiso  8351  smoiso2  8358  supisolem  9437  supisoex  9438  supiso  9439  ordiso2  9480  ordtypelem10  9492  oiexg  9500  oien  9503  oismo  9505  cantnfle  9643  cantnflt2  9645  cantnfp1lem3  9652  cantnflem1b  9658  cantnflem1d  9660  cantnflem1  9661  cantnffval2  9667  cantnff1o  9668  wemapwe  9669  cnfcom3lem  9675  infxpenlem  10009  iunfictbso  10110  dfac12lem2  10140  cofsmo  10264  isf34lem3  10370  isf34lem5  10373  hsmexlem1  10421  fpwwe2lem5  10631  fpwwe2lem6  10632  fpwwe2lem8  10634  pwfseqlem5  10659  fz1isolem  14511  seqcoll  14514  seqcoll2  14515  isercolllem2  15736  isercoll  15738  summolem2a  15784  prodmolem2a  16006  gsumval3lem1  19998  gsumval3  20000  ordthmeolem  23987  dvne0f1  26200  dvcvx  26208  addonbday  28501  isoun  33076  nsgqusf1o  33748  ordtypeon  35498  wevonprcf1o  35613  erdsze2lem1  35708  fourierdlem20  46874  fourierdlem50  46903  fourierdlem51  46904  fourierdlem52  46905  fourierdlem63  46916  fourierdlem64  46917  fourierdlem65  46918  fourierdlem76  46929  fourierdlem102  46955  fourierdlem114  46967