Theorem isof1o 7302

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wral 3075   class class class wbr 5097  –1-1-onto→wf1o 6515  ‘cfv 6516   Isom wiso 6517

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 209  df-an 400  df-isom 6525

This theorem is referenced by:  isores1  7313  isomin  7316  isoini  7317  isoini2  7318  isofrlem  7319  isoselem  7320  isofr  7321  isose  7322  isofr2  7323  isopolem  7324  isosolem  7326  weniso  7333  weisoeq  7334  weisoeq2  7335  wemoiso  7949  wemoiso2  7950  smoiso  8327  smoiso2  8334  supisolem  9414  supisoex  9415  supiso  9416  ordiso2  9457  ordtypelem10  9469  oiexg  9477  oien  9480  oismo  9482  cantnfle  9620  cantnflt2  9622  cantnfp1lem3  9629  cantnflem1b  9635  cantnflem1d  9637  cantnflem1  9638  cantnffval2  9644  cantnff1o  9645  wemapwe  9646  cnfcom3lem  9652  infxpenlem  9963  iunfictbso  10064  dfac12lem2  10095  cofsmo  10220  isf34lem3  10326  isf34lem5  10329  hsmexlem1  10377  fpwwe2lem5  10587  fpwwe2lem6  10588  fpwwe2lem8  10590  pwfseqlem5  10615  fz1isolem  14468  seqcoll  14471  seqcoll2  14472  isercolllem2  15684  isercoll  15686  summolem2a  15733  prodmolem2a  15955  gsumval3lem1  19936  gsumval3  19938  ordthmeolem  23849  dvne0f1  26062  dvcvx  26070  addonbday  28360  isoun  32865  nsgqusf1o  33563  ordtypeon  35347  wevonprcf1o  35417  erdsze2lem1  35514  fourierdlem20  46662  fourierdlem50  46691  fourierdlem51  46692  fourierdlem52  46693  fourierdlem63  46704  fourierdlem64  46705  fourierdlem65  46706  fourierdlem76  46717  fourierdlem102  46743  fourierdlem114  46755