Theorem isof1o 7343

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wral 3059   class class class wbr 5148  –1-1-onto→wf1o 6562  ‘cfv 6563   Isom wiso 6564

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 6572

This theorem is referenced by:  isores1  7354  isomin  7357  isoini  7358  isoini2  7359  isofrlem  7360  isoselem  7361  isofr  7362  isose  7363  isofr2  7364  isopolem  7365  isosolem  7367  weniso  7374  weisoeq  7375  weisoeq2  7376  wemoiso  7997  wemoiso2  7998  smoiso  8401  smoiso2  8408  supisolem  9511  supisoex  9512  supiso  9513  ordiso2  9553  ordtypelem10  9565  oiexg  9573  oien  9576  oismo  9578  cantnfle  9709  cantnflt2  9711  cantnfp1lem3  9718  cantnflem1b  9724  cantnflem1d  9726  cantnflem1  9727  cantnffval2  9733  cantnff1o  9734  wemapwe  9735  cnfcom3lem  9741  infxpenlem  10051  iunfictbso  10152  dfac12lem2  10183  cofsmo  10307  isf34lem3  10413  isf34lem5  10416  hsmexlem1  10464  fpwwe2lem5  10673  fpwwe2lem6  10674  fpwwe2lem8  10676  pwfseqlem5  10701  fz1isolem  14497  seqcoll  14500  seqcoll2  14501  isercolllem2  15699  isercoll  15701  summolem2a  15748  prodmolem2a  15967  gsumval3lem1  19938  gsumval3  19940  ordthmeolem  23825  dvne0f1  26066  dvcvx  26074  isoun  32717  nsgqusf1o  33424  erdsze2lem1  35188  fourierdlem20  46083  fourierdlem50  46112  fourierdlem51  46113  fourierdlem52  46114  fourierdlem63  46125  fourierdlem64  46126  fourierdlem65  46127  fourierdlem76  46138  fourierdlem102  46164  fourierdlem114  46176