Metamath Proof Explorer

Theorem dff1o6

Description: A one-to-one onto function in terms of function values. (Contributed by NM, 29-Mar-2008)

Ref Expression
Assertion dff1o6 ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ ran ⁡ F = B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y

Proof

Step Hyp Ref Expression
1 df-f1o ⊢ F : A ⟶ 1-1 onto B ↔ F : A ⟶ 1-1 B ∧ F : A ⟶ onto B
2 dff13 ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y
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 ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y ∧ F Fn A ∧ ran ⁡ F = B
5 df-3an ⊢ F Fn A ∧ ran ⁡ F = B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y ↔ F Fn A ∧ ran ⁡ F = B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y
6 eqimss ⊢ ran ⁡ F = B → ran ⁡ F ⊆ B
7 6 anim2i ⊢ F Fn A ∧ ran ⁡ F = B → F Fn A ∧ ran ⁡ F ⊆ B
8 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B
9 7 8 sylibr ⊢ F Fn A ∧ ran ⁡ F = B → F : A ⟶ B
10 9 pm4.71ri ⊢ F Fn A ∧ ran ⁡ F = B ↔ F : A ⟶ B ∧ F Fn A ∧ ran ⁡ F = B
11 10 anbi1i ⊢ F Fn A ∧ ran ⁡ F = B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y ↔ F : A ⟶ B ∧ F Fn A ∧ ran ⁡ F = B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y
12 an32 ⊢ F : A ⟶ B ∧ F Fn A ∧ ran ⁡ F = B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y ↔ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y ∧ F Fn A ∧ ran ⁡ F = B
13 5 11 12 3bitrri ⊢ F : A ⟶ B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y ∧ F Fn A ∧ ran ⁡ F = B ↔ F Fn A ∧ ran ⁡ F = B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y
14 1 4 13 3bitri ⊢ F : A ⟶ 1-1 onto B ↔ F Fn A ∧ ran ⁡ F = B ∧ ∀ x ∈ A ∀ y ∈ A F ⁡ x = F ⁡ y → x = y