Theorem isof1o 7330

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3050   class class class wbr 5149  –1-1-onto→wf1o 6548  ‘cfv 6549   Isom wiso 6550

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 206  df-an 395  df-isom 6558

This theorem is referenced by:  isores1  7341  isomin  7344  isoini  7345  isoini2  7346  isofrlem  7347  isoselem  7348  isofr  7349  isose  7350  isofr2  7351  isopolem  7352  isosolem  7354  weniso  7361  weisoeq  7362  weisoeq2  7363  wemoiso  7978  wemoiso2  7979  smoiso  8383  smoiso2  8390  supisolem  9498  supisoex  9499  supiso  9500  ordiso2  9540  ordtypelem10  9552  oiexg  9560  oien  9563  oismo  9565  cantnfle  9696  cantnflt2  9698  cantnfp1lem3  9705  cantnflem1b  9711  cantnflem1d  9713  cantnflem1  9714  cantnffval2  9720  cantnff1o  9721  wemapwe  9722  cnfcom3lem  9728  infxpenlem  10038  iunfictbso  10139  dfac12lem2  10169  cofsmo  10294  isf34lem3  10400  isf34lem5  10403  hsmexlem1  10451  fpwwe2lem5  10660  fpwwe2lem6  10661  fpwwe2lem8  10663  pwfseqlem5  10688  fz1isolem  14458  seqcoll  14461  seqcoll2  14462  isercolllem2  15648  isercoll  15650  summolem2a  15697  prodmolem2a  15914  gsumval3lem1  19872  gsumval3  19874  ordthmeolem  23749  dvne0f1  25989  dvcvx  25997  isoun  32563  nsgqusf1o  33228  erdsze2lem1  34941  fourierdlem20  45650  fourierdlem50  45679  fourierdlem51  45680  fourierdlem52  45681  fourierdlem63  45692  fourierdlem64  45693  fourierdlem65  45694  fourierdlem76  45705  fourierdlem102  45731  fourierdlem114  45743