Theorem isof1o 7362

Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004.)

Assertion

Ref	Expression
isof1o	⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴⟶1-1onto𝐵)

Proof of Theorem isof1o

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-isom 6575	. 2 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) ↔ (𝐻:𝐴⟶1-1onto𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ↔ (𝐻‘𝑥)𝑆(𝐻‘𝑦))))
2	1	simplbi 502	1 ⊢ (𝐻 Isom 𝑅, 𝑆 (𝐴, 𝐵) → 𝐻:𝐴⟶1-1onto𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wral 3080   class class class wbr 5108  ⟶1-1ontowf1o 6565  ‘cfv 6566   Isom wiso 6567

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-isom 6575

This theorem is used by:  isores1  7373  isomin  7376  isoini  7377  isoini2  7378  isofrlem  7379  isoselem  7380  isofr  7381  isose  7382  isofr2  7383  isopolem  7384  isosolem  7386  weniso  7395  weisoeq  7396  weisoeq2  7397  wemoiso  8019  wemoiso2  8020  smoiso  8408  smoiso2  8415  supisolem  9503  supisoex  9504  supiso  9505  ordiso2  9546  ordtypelem10  9558  oiexg  9566  oien  9569  oismo  9571  cantnfle  9709  cantnflt2  9711  cantnfp1lem3  9718  cantnflem1b  9724  cantnflem1d  9726  cantnflem1  9727  cantnffval2  9733  cantnff1o  9734  wemapwe  9735  cnfcom3lem  9741  infxpenlem  10131  iunfictbso  10232  dfac12lem2  10262  cofsmo  10386  isf34lem3  10492  isf34lem5  10495  hsmexlem1  10543  fpwwe2lem5  10759  fpwwe2lem6  10760  fpwwe2lem8  10762  pwfseqlem5  10787  fz1isolem  14647  seqcoll  14650  seqcoll2  14651  isercolllem2  15877  isercoll  15879  summolem2a  15925  prodmolem2a  16145  gsumval3lem1  20170  gsumval3  20172  ordthmeolem  24175  dvne0f1  26387  dvcvx  26395  addonbday  28722  isoun  33392  nsgqusf1o  34071  ordtypeon  35843  j00smo  36046  maxssj0  36047  j0ltalephlem  36048  j0ltaleph  36049  jf1  36051  jf1o  36052  j0le  36060  k3n0j0lt  36061  jltalephlem  36066  jltaleph  36067  wevonprcf1o  36083  vonf1onprcf1ac  36085  erdsze2lem1  36176  fourierdlem20  47410  fourierdlem50  47439  fourierdlem51  47440  fourierdlem52  47441  fourierdlem63  47452  fourierdlem64  47453  fourierdlem65  47454  fourierdlem76  47465  fourierdlem102  47491  fourierdlem114  47503