Description: An isomorphism is a one-to-one onto function. (Contributed by NM, 27-Apr-2004)
Ref | Expression | ||
---|---|---|---|
Assertion | isof1o | |- ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-isom | |- ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) ) |
|
2 | 1 | simplbi | |- ( H Isom R , S ( A , B ) -> H : A -1-1-onto-> B ) |