Theorem isof1o 6473

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

Syntax hints:   → wi 4   ↔ wb 195  ∀wral 2896   class class class wbr 4583  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805

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 196  df-an 385  df-isom 5813

This theorem is referenced by:  isores1  6484  isomin  6487  isoini  6488  isoini2  6489  isofrlem  6490  isoselem  6491  isofr  6492  isose  6493  isofr2  6494  isopolem  6495  isosolem  6497  weniso  6504  weisoeq  6505  weisoeq2  6506  wemoiso  7044  wemoiso2  7045  smoiso  7346  smoiso2  7353  supisolem  8262  supisoex  8263  supiso  8264  ordiso2  8303  ordtypelem10  8315  oiexg  8323  oien  8326  oismo  8328  cantnfle  8451  cantnflt2  8453  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1d  8468  cantnflem1  8469  cantnffval2  8475  cantnff1o  8476  wemapwe  8477  cnfcom3lem  8483  infxpenlem  8719  iunfictbso  8820  dfac12lem2  8849  cofsmo  8974  isf34lem3  9080  isf34lem5  9083  hsmexlem1  9131  fpwwe2lem6  9336  fpwwe2lem7  9337  fpwwe2lem9  9339  pwfseqlem5  9364  fz1isolem  13102  seqcoll  13105  seqcoll2  13106  isercolllem2  14244  isercoll  14246  summolem2a  14293  prodmolem2a  14503  gsumval3lem1  18129  gsumval3  18131  ordthmeolem  21414  dvne0f1  23579  dvcvx  23587  isoun  28862  erdsze2lem1  30439  fourierdlem20  39020  fourierdlem50  39049  fourierdlem51  39050  fourierdlem52  39051  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem76  39075  fourierdlem102  39101  fourierdlem114  39113