Theorem isof1o 7320

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3062   class class class wbr 5149  –1-1-onto→wf1o 6543  ‘cfv 6544   Isom wiso 6545

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 206  df-an 398  df-isom 6553

This theorem is referenced by:  isores1  7331  isomin  7334  isoini  7335  isoini2  7336  isofrlem  7337  isoselem  7338  isofr  7339  isose  7340  isofr2  7341  isopolem  7342  isosolem  7344  weniso  7351  weisoeq  7352  weisoeq2  7353  wemoiso  7960  wemoiso2  7961  smoiso  8362  smoiso2  8369  supisolem  9468  supisoex  9469  supiso  9470  ordiso2  9510  ordtypelem10  9522  oiexg  9530  oien  9533  oismo  9535  cantnfle  9666  cantnflt2  9668  cantnfp1lem3  9675  cantnflem1b  9681  cantnflem1d  9683  cantnflem1  9684  cantnffval2  9690  cantnff1o  9691  wemapwe  9692  cnfcom3lem  9698  infxpenlem  10008  iunfictbso  10109  dfac12lem2  10139  cofsmo  10264  isf34lem3  10370  isf34lem5  10373  hsmexlem1  10421  fpwwe2lem5  10630  fpwwe2lem6  10631  fpwwe2lem8  10633  pwfseqlem5  10658  fz1isolem  14422  seqcoll  14425  seqcoll2  14426  isercolllem2  15612  isercoll  15614  summolem2a  15661  prodmolem2a  15878  gsumval3lem1  19773  gsumval3  19775  ordthmeolem  23305  dvne0f1  25529  dvcvx  25537  isoun  31954  nsgqusf1o  32558  erdsze2lem1  34225  fourierdlem20  44891  fourierdlem50  44920  fourierdlem51  44921  fourierdlem52  44922  fourierdlem63  44933  fourierdlem64  44934  fourierdlem65  44935  fourierdlem76  44946  fourierdlem102  44972  fourierdlem114  44984