Theorem isof1o 3899

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 3205	. 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 1648   class class class wbr 2624  -1-1-onto->wf1o 3187  ` cfv 3188   Isom wiso 3189

This theorem is referenced by:  isomin 3905  isoini 3906  isofrlem 3907  isowe 3909

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 3205

Copyright terms: Public domain