Metamath Proof Explorer

Theorem f11o

Description: Relationship between one-to-one and one-to-one onto function. (Contributed by NM, 4-Apr-1998)

Ref Expression
Hypothesis f11o.1 ⊢ F ∈ V
Assertion f11o ⊢ F : A ⟶ 1-1 B ↔ ∃ x F : A ⟶ 1-1 onto x ∧ x ⊆ B

Proof

Step Hyp Ref Expression
1 f11o.1 ⊢ F ∈ V
2 1 ffoss ⊢ F : A ⟶ B ↔ ∃ x F : A ⟶ onto x ∧ x ⊆ B
3 2 anbi1i ⊢ F : A ⟶ B ∧ Fun ⁡ F -1 ↔ ∃ x F : A ⟶ onto x ∧ x ⊆ B ∧ Fun ⁡ F -1
4 df-f1 ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ Fun ⁡ F -1
5 dff1o3 ⊢ F : A ⟶ 1-1 onto x ↔ F : A ⟶ onto x ∧ Fun ⁡ F -1
6 5 anbi1i ⊢ F : A ⟶ 1-1 onto x ∧ x ⊆ B ↔ F : A ⟶ onto x ∧ Fun ⁡ F -1 ∧ x ⊆ B
7 an32 ⊢ F : A ⟶ onto x ∧ Fun ⁡ F -1 ∧ x ⊆ B ↔ F : A ⟶ onto x ∧ x ⊆ B ∧ Fun ⁡ F -1
8 6 7 bitri ⊢ F : A ⟶ 1-1 onto x ∧ x ⊆ B ↔ F : A ⟶ onto x ∧ x ⊆ B ∧ Fun ⁡ F -1
9 8 exbii ⊢ ∃ x F : A ⟶ 1-1 onto x ∧ x ⊆ B ↔ ∃ x F : A ⟶ onto x ∧ x ⊆ B ∧ Fun ⁡ F -1
10 19.41v ⊢ ∃ x F : A ⟶ onto x ∧ x ⊆ B ∧ Fun ⁡ F -1 ↔ ∃ x F : A ⟶ onto x ∧ x ⊆ B ∧ Fun ⁡ F -1
11 9 10 bitri ⊢ ∃ x F : A ⟶ 1-1 onto x ∧ x ⊆ B ↔ ∃ x F : A ⟶ onto x ∧ x ⊆ B ∧ Fun ⁡ F -1
12 3 4 11 3bitr4i ⊢ F : A ⟶ 1-1 B ↔ ∃ x F : A ⟶ 1-1 onto x ∧ x ⊆ B