Theorem isof1o 3893

Description: An isomorphism is a one-to-one onto function.

Assertion

Ref	Expression
isof1o	|- (H Isom R, S (A, B) -> H:A-1-1-onto->B)

Proof of Theorem isof1o

Step	Hyp	Ref	Expression
1		df-iso 3199	. 2 |- (H Isom R, S (A, B) <-> (H:A-1-1-onto->B /\ A.x e. A A.y e. A (xRy <-> (H` x)S(H` y))))
2	1	pm3.26bi 322	1 |- (H Isom R, S (A, B) -> H:A-1-1-onto->B)

Syntax hints:   -> wi 3   <-> wb 146  A.wral 1645   class class class wbr 2619  -1-1-onto->wf1o 3181  ` cfv 3182   Isom wiso 3183

This theorem is referenced by:  isomin 3899  isoini 3900  isofrlem 3901  isowe 3903

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-iso 3199

Copyright terms: Public domain