Theorem isof1o 6613

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

Syntax hints:   → wi 4   ↔ wb 196  ∀wral 2941   class class class wbr 4685  –1-1-onto→wf1o 5925  ‘cfv 5926   Isom wiso 5927

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 197  df-an 385  df-isom 5935

This theorem is referenced by:  isores1  6624  isomin  6627  isoini  6628  isoini2  6629  isofrlem  6630  isoselem  6631  isofr  6632  isose  6633  isofr2  6634  isopolem  6635  isosolem  6637  weniso  6644  weisoeq  6645  weisoeq2  6646  wemoiso  7195  wemoiso2  7196  smoiso  7504  smoiso2  7511  supisolem  8420  supisoex  8421  supiso  8422  ordiso2  8461  ordtypelem10  8473  oiexg  8481  oien  8484  oismo  8486  cantnfle  8606  cantnflt2  8608  cantnfp1lem3  8615  cantnflem1b  8621  cantnflem1d  8623  cantnflem1  8624  cantnffval2  8630  cantnff1o  8631  wemapwe  8632  cnfcom3lem  8638  infxpenlem  8874  iunfictbso  8975  dfac12lem2  9004  cofsmo  9129  isf34lem3  9235  isf34lem5  9238  hsmexlem1  9286  fpwwe2lem6  9495  fpwwe2lem7  9496  fpwwe2lem9  9498  pwfseqlem5  9523  fz1isolem  13283  seqcoll  13286  seqcoll2  13287  isercolllem2  14440  isercoll  14442  summolem2a  14490  prodmolem2a  14708  gsumval3lem1  18352  gsumval3  18354  ordthmeolem  21652  dvne0f1  23820  dvcvx  23828  isoun  29607  erdsze2lem1  31311  fourierdlem20  40662  fourierdlem50  40691  fourierdlem51  40692  fourierdlem52  40693  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem76  40717  fourierdlem102  40743  fourierdlem114  40755