Metamath Proof Explorer

Theorem fo00

Description: Onto mapping of the empty set. (Contributed by NM, 22-Mar-2006)

Ref Expression
Assertion fo00 ⊢ F : ∅ ⟶ onto A ↔ F = ∅ ∧ A = ∅

Proof

Step Hyp Ref Expression
1 fofn ⊢ F : ∅ ⟶ onto A → F Fn ∅
2 fn0 ⊢ F Fn ∅ ↔ F = ∅
3 f10 ⊢ ∅ : ∅ ⟶ 1-1 A
4 f1eq1 ⊢ F = ∅ → F : ∅ ⟶ 1-1 A ↔ ∅ : ∅ ⟶ 1-1 A
5 3 4 mpbiri ⊢ F = ∅ → F : ∅ ⟶ 1-1 A
6 2 5 sylbi ⊢ F Fn ∅ → F : ∅ ⟶ 1-1 A
7 1 6 syl ⊢ F : ∅ ⟶ onto A → F : ∅ ⟶ 1-1 A
8 7 ancri ⊢ F : ∅ ⟶ onto A → F : ∅ ⟶ 1-1 A ∧ F : ∅ ⟶ onto A
9 df-f1o ⊢ F : ∅ ⟶ 1-1 onto A ↔ F : ∅ ⟶ 1-1 A ∧ F : ∅ ⟶ onto A
10 8 9 sylibr ⊢ F : ∅ ⟶ onto A → F : ∅ ⟶ 1-1 onto A
11 f1ofo ⊢ F : ∅ ⟶ 1-1 onto A → F : ∅ ⟶ onto A
12 10 11 impbii ⊢ F : ∅ ⟶ onto A ↔ F : ∅ ⟶ 1-1 onto A
13 f1o00 ⊢ F : ∅ ⟶ 1-1 onto A ↔ F = ∅ ∧ A = ∅
14 12 13 bitri ⊢ F : ∅ ⟶ onto A ↔ F = ∅ ∧ A = ∅