Metamath Proof Explorer

Theorem dff1o2

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

Ref Expression
Assertion dff1o2 ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B

Proof

Step Hyp Ref Expression
1 df-f1o ⊢ F : A ⟶ 1-1 onto B ↔ F : A ⟶ 1-1 B ∧ F : A ⟶ onto B
2 df-f1 ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ Fun ⁡ F -1
3 df-fo ⊢ F : A ⟶ onto B ↔ F Fn A ∧ ran ⁡ F = B
4 2 3 anbi12i ⊢ F : A ⟶ 1-1 B ∧ F : A ⟶ onto B ↔ F : A ⟶ B ∧ Fun ⁡ F -1 ∧ F Fn A ∧ ran ⁡ F = B
5 anass ⊢ F : A ⟶ B ∧ Fun ⁡ F -1 ∧ F Fn A ∧ ran ⁡ F = B ↔ F : A ⟶ B ∧ Fun ⁡ F -1 ∧ F Fn A ∧ ran ⁡ F = B
6 3anan12 ⊢ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B ↔ Fun ⁡ F -1 ∧ F Fn A ∧ ran ⁡ F = B
7 6 anbi1i ⊢ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B ∧ F : A ⟶ B ↔ Fun ⁡ F -1 ∧ F Fn A ∧ ran ⁡ F = B ∧ F : A ⟶ B
8 eqimss ⊢ ran ⁡ F = B → ran ⁡ F ⊆ B
9 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B
10 9 biimpri ⊢ F Fn A ∧ ran ⁡ F ⊆ B → F : A ⟶ B
11 8 10 sylan2 ⊢ F Fn A ∧ ran ⁡ F = B → F : A ⟶ B
12 11 3adant2 ⊢ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B → F : A ⟶ B
13 12 pm4.71i ⊢ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B ∧ F : A ⟶ B
14 ancom ⊢ F : A ⟶ B ∧ Fun ⁡ F -1 ∧ F Fn A ∧ ran ⁡ F = B ↔ Fun ⁡ F -1 ∧ F Fn A ∧ ran ⁡ F = B ∧ F : A ⟶ B
15 7 13 14 3bitr4ri ⊢ F : A ⟶ B ∧ Fun ⁡ F -1 ∧ F Fn A ∧ ran ⁡ F = B ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B
16 5 15 bitri ⊢ F : A ⟶ B ∧ Fun ⁡ F -1 ∧ F Fn A ∧ ran ⁡ F = B ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B
17 4 16 bitri ⊢ F : A ⟶ 1-1 B ∧ F : A ⟶ onto B ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B
18 1 17 bitri ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ Fun ⁡ F -1 ∧ ran ⁡ F = B