This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isof1o

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

Proof

Step Hyp Ref Expression
1 df-isom ⊢ H Isom R , S A B ↔ H : A ⟶ 1-1 onto B ∧ ∀ x ∈ A ∀ y ∈ A x R y ↔ H ⁡ x S H ⁡ y
2 1 simplbi ⊢ H Isom R , S A B → H : A ⟶ 1-1 onto B