Theorem isof1o 7316

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3051   class class class wbr 5119  –1-1-onto→wf1o 6530  ‘cfv 6531   Isom wiso 6532

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 6540

This theorem is referenced by:  isores1  7327  isomin  7330  isoini  7331  isoini2  7332  isofrlem  7333  isoselem  7334  isofr  7335  isose  7336  isofr2  7337  isopolem  7338  isosolem  7340  weniso  7347  weisoeq  7348  weisoeq2  7349  wemoiso  7972  wemoiso2  7973  smoiso  8376  smoiso2  8383  supisolem  9486  supisoex  9487  supiso  9488  ordiso2  9529  ordtypelem10  9541  oiexg  9549  oien  9552  oismo  9554  cantnfle  9685  cantnflt2  9687  cantnfp1lem3  9694  cantnflem1b  9700  cantnflem1d  9702  cantnflem1  9703  cantnffval2  9709  cantnff1o  9710  wemapwe  9711  cnfcom3lem  9717  infxpenlem  10027  iunfictbso  10128  dfac12lem2  10159  cofsmo  10283  isf34lem3  10389  isf34lem5  10392  hsmexlem1  10440  fpwwe2lem5  10649  fpwwe2lem6  10650  fpwwe2lem8  10652  pwfseqlem5  10677  fz1isolem  14479  seqcoll  14482  seqcoll2  14483  isercolllem2  15682  isercoll  15684  summolem2a  15731  prodmolem2a  15950  gsumval3lem1  19886  gsumval3  19888  ordthmeolem  23739  dvne0f1  25969  dvcvx  25977  isoun  32679  nsgqusf1o  33431  erdsze2lem1  35225  fourierdlem20  46156  fourierdlem50  46185  fourierdlem51  46186  fourierdlem52  46187  fourierdlem63  46198  fourierdlem64  46199  fourierdlem65  46200  fourierdlem76  46211  fourierdlem102  46237  fourierdlem114  46249