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 ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴1-1-onto𝐵 )

Proof

Step Hyp Ref Expression
1 df-isom ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ↔ ( 𝐻 : 𝐴1-1-onto𝐵 ∧ ∀ 𝑥𝐴𝑦𝐴 ( 𝑥 𝑅 𝑦 ↔ ( 𝐻𝑥 ) 𝑆 ( 𝐻𝑦 ) ) ) )
2 1 simplbi ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → 𝐻 : 𝐴1-1-onto𝐵 )