Theorem isof1o 7266

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3048   class class class wbr 5095  –1-1-onto→wf1o 6488  ‘cfv 6489   Isom wiso 6490

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 6498

This theorem is referenced by:  isores1  7277  isomin  7280  isoini  7281  isoini2  7282  isofrlem  7283  isoselem  7284  isofr  7285  isose  7286  isofr2  7287  isopolem  7288  isosolem  7290  weniso  7297  weisoeq  7298  weisoeq2  7299  wemoiso  7914  wemoiso2  7915  smoiso  8291  smoiso2  8298  supisolem  9369  supisoex  9370  supiso  9371  ordiso2  9412  ordtypelem10  9424  oiexg  9432  oien  9435  oismo  9437  cantnfle  9572  cantnflt2  9574  cantnfp1lem3  9581  cantnflem1b  9587  cantnflem1d  9589  cantnflem1  9590  cantnffval2  9596  cantnff1o  9597  wemapwe  9598  cnfcom3lem  9604  infxpenlem  9915  iunfictbso  10016  dfac12lem2  10047  cofsmo  10171  isf34lem3  10277  isf34lem5  10280  hsmexlem1  10328  fpwwe2lem5  10537  fpwwe2lem6  10538  fpwwe2lem8  10540  pwfseqlem5  10565  fz1isolem  14375  seqcoll  14378  seqcoll2  14379  isercolllem2  15580  isercoll  15582  summolem2a  15629  prodmolem2a  15848  gsumval3lem1  19825  gsumval3  19827  ordthmeolem  23736  dvne0f1  25964  dvcvx  25972  isoun  32707  nsgqusf1o  33425  erdsze2lem1  35319  fourierdlem20  46287  fourierdlem50  46316  fourierdlem51  46317  fourierdlem52  46318  fourierdlem63  46329  fourierdlem64  46330  fourierdlem65  46331  fourierdlem76  46342  fourierdlem102  46368  fourierdlem114  46380