Theorem isof1o 7174

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

Syntax hints:   → wi 4   ↔ wb 205  ∀wral 3063   class class class wbr 5070  –1-1-onto→wf1o 6417  ‘cfv 6418   Isom wiso 6419

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 396  df-isom 6427

This theorem is referenced by:  isores1  7185  isomin  7188  isoini  7189  isoini2  7190  isofrlem  7191  isoselem  7192  isofr  7193  isose  7194  isofr2  7195  isopolem  7196  isosolem  7198  weniso  7205  weisoeq  7206  weisoeq2  7207  wemoiso  7789  wemoiso2  7790  smoiso  8164  smoiso2  8171  supisolem  9162  supisoex  9163  supiso  9164  ordiso2  9204  ordtypelem10  9216  oiexg  9224  oien  9227  oismo  9229  cantnfle  9359  cantnflt2  9361  cantnfp1lem3  9368  cantnflem1b  9374  cantnflem1d  9376  cantnflem1  9377  cantnffval2  9383  cantnff1o  9384  wemapwe  9385  cnfcom3lem  9391  infxpenlem  9700  iunfictbso  9801  dfac12lem2  9831  cofsmo  9956  isf34lem3  10062  isf34lem5  10065  hsmexlem1  10113  fpwwe2lem5  10322  fpwwe2lem6  10323  fpwwe2lem8  10325  pwfseqlem5  10350  fz1isolem  14103  seqcoll  14106  seqcoll2  14107  isercolllem2  15305  isercoll  15307  summolem2a  15355  prodmolem2a  15572  gsumval3lem1  19421  gsumval3  19423  ordthmeolem  22860  dvne0f1  25081  dvcvx  25089  isoun  30936  nsgqusf1o  31503  erdsze2lem1  33065  fourierdlem20  43558  fourierdlem50  43587  fourierdlem51  43588  fourierdlem52  43589  fourierdlem63  43600  fourierdlem64  43601  fourierdlem65  43602  fourierdlem76  43613  fourierdlem102  43639  fourierdlem114  43651