Metamath Proof Explorer

Theorem dff1o3

Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998) (Proof shortened by Andrew Salmon, 22-Oct-2011)

Ref Expression
Assertion dff1o3 ⊢ F : A ⟶ 1-1 onto B ↔ F : A ⟶ onto B ∧ Fun ⁡ F -1

Proof

Step Hyp Ref Expression
1 3anan32 ⊢ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B ↔ F Fn A ∧ ran ⁡ F = B ∧ Fun ⁡ F -1
2 dff1o2 ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B
3 df-fo ⊢ F : A ⟶ onto B ↔ F Fn A ∧ ran ⁡ F = B
4 3 anbi1i ⊢ F : A ⟶ onto B ∧ Fun ⁡ F -1 ↔ F Fn A ∧ ran ⁡ F = B ∧ Fun ⁡ F -1
5 1 2 4 3bitr4i ⊢ F : A ⟶ 1-1 onto B ↔ F : A ⟶ onto B ∧ Fun ⁡ F -1