Theorem isof1o 7317

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3062   class class class wbr 5148  –1-1-onto→wf1o 6540  ‘cfv 6541   Isom wiso 6542

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 398  df-isom 6550

This theorem is referenced by:  isores1  7328  isomin  7331  isoini  7332  isoini2  7333  isofrlem  7334  isoselem  7335  isofr  7336  isose  7337  isofr2  7338  isopolem  7339  isosolem  7341  weniso  7348  weisoeq  7349  weisoeq2  7350  wemoiso  7957  wemoiso2  7958  smoiso  8359  smoiso2  8366  supisolem  9465  supisoex  9466  supiso  9467  ordiso2  9507  ordtypelem10  9519  oiexg  9527  oien  9530  oismo  9532  cantnfle  9663  cantnflt2  9665  cantnfp1lem3  9672  cantnflem1b  9678  cantnflem1d  9680  cantnflem1  9681  cantnffval2  9687  cantnff1o  9688  wemapwe  9689  cnfcom3lem  9695  infxpenlem  10005  iunfictbso  10106  dfac12lem2  10136  cofsmo  10261  isf34lem3  10367  isf34lem5  10370  hsmexlem1  10418  fpwwe2lem5  10627  fpwwe2lem6  10628  fpwwe2lem8  10630  pwfseqlem5  10655  fz1isolem  14419  seqcoll  14422  seqcoll2  14423  isercolllem2  15609  isercoll  15611  summolem2a  15658  prodmolem2a  15875  gsumval3lem1  19768  gsumval3  19770  ordthmeolem  23297  dvne0f1  25521  dvcvx  25529  isoun  31911  nsgqusf1o  32516  erdsze2lem1  34183  fourierdlem20  44830  fourierdlem50  44859  fourierdlem51  44860  fourierdlem52  44861  fourierdlem63  44872  fourierdlem64  44873  fourierdlem65  44874  fourierdlem76  44885  fourierdlem102  44911  fourierdlem114  44923