Theorem isof1o 7298

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3044   class class class wbr 5107  –1-1-onto→wf1o 6510  ‘cfv 6511   Isom wiso 6512

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 6520

This theorem is referenced by:  isores1  7309  isomin  7312  isoini  7313  isoini2  7314  isofrlem  7315  isoselem  7316  isofr  7317  isose  7318  isofr2  7319  isopolem  7320  isosolem  7322  weniso  7329  weisoeq  7330  weisoeq2  7331  wemoiso  7952  wemoiso2  7953  smoiso  8331  smoiso2  8338  supisolem  9425  supisoex  9426  supiso  9427  ordiso2  9468  ordtypelem10  9480  oiexg  9488  oien  9491  oismo  9493  cantnfle  9624  cantnflt2  9626  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1d  9641  cantnflem1  9642  cantnffval2  9648  cantnff1o  9649  wemapwe  9650  cnfcom3lem  9656  infxpenlem  9966  iunfictbso  10067  dfac12lem2  10098  cofsmo  10222  isf34lem3  10328  isf34lem5  10331  hsmexlem1  10379  fpwwe2lem5  10588  fpwwe2lem6  10589  fpwwe2lem8  10591  pwfseqlem5  10616  fz1isolem  14426  seqcoll  14429  seqcoll2  14430  isercolllem2  15632  isercoll  15634  summolem2a  15681  prodmolem2a  15900  gsumval3lem1  19835  gsumval3  19837  ordthmeolem  23688  dvne0f1  25917  dvcvx  25925  isoun  32625  nsgqusf1o  33387  erdsze2lem1  35190  fourierdlem20  46125  fourierdlem50  46154  fourierdlem51  46155  fourierdlem52  46156  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem76  46180  fourierdlem102  46206  fourierdlem114  46218