Metamath Proof Explorer

Theorem dff1o4

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 dff1o4 ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ F -1 Fn B

Proof

Step Hyp Ref Expression
1 dff1o2 ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B
2 3anass ⊢ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B
3 df-rn ⊢ ran ⁡ F = dom ⁡ F -1
4 3 eqeq1i ⊢ ran ⁡ F = B ↔ dom ⁡ F -1 = B
5 4 anbi2i ⊢ Fun ⁡ F -1 ∧ ran ⁡ F = B ↔ Fun ⁡ F -1 ∧ dom ⁡ F -1 = B
6 df-fn ⊢ F -1 Fn B ↔ Fun ⁡ F -1 ∧ dom ⁡ F -1 = B
7 5 6 bitr4i ⊢ Fun ⁡ F -1 ∧ ran ⁡ F = B ↔ F -1 Fn B
8 7 anbi2i ⊢ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B ↔ F Fn A ∧ F -1 Fn B
9 1 2 8 3bitri ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ F -1 Fn B