Metamath Proof Explorer

Theorem f1o00

Description: One-to-one onto mapping of the empty set. (Contributed by NM, 15-Apr-1998)

Ref Expression
Assertion f1o00 ⊢ F : ∅ ⟶ 1-1 onto A ↔ F = ∅ ∧ A = ∅

Proof

Step Hyp Ref Expression
1 dff1o4 ⊢ F : ∅ ⟶ 1-1 onto A ↔ F Fn ∅ ∧ F -1 Fn A
2 fn0 ⊢ F Fn ∅ ↔ F = ∅
3 2 birani ⊢ F Fn ∅ ∧ F -1 Fn A → F = ∅
4 cnveq ⊢ F = ∅ → F -1 = ∅ -1
5 cnv0 ⊢ ∅ -1 = ∅
6 4 5 eqtrdi ⊢ F = ∅ → F -1 = ∅
7 2 6 sylbi ⊢ F Fn ∅ → F -1 = ∅
8 7 fneq1d ⊢ F Fn ∅ → F -1 Fn A ↔ ∅ Fn A
9 8 biimpa ⊢ F Fn ∅ ∧ F -1 Fn A → ∅ Fn A
10 9 fndmd ⊢ F Fn ∅ ∧ F -1 Fn A → dom ⁡ ∅ = A
11 dm0 ⊢ dom ⁡ ∅ = ∅
12 10 11 eqtr3di ⊢ F Fn ∅ ∧ F -1 Fn A → A = ∅
13 3 12 jca ⊢ F Fn ∅ ∧ F -1 Fn A → F = ∅ ∧ A = ∅
14 2 biranri ⊢ F = ∅ ∧ A = ∅ → F Fn ∅
15 eqid ⊢ ∅ = ∅
16 fn0 ⊢ ∅ Fn ∅ ↔ ∅ = ∅
17 15 16 mpbir ⊢ ∅ Fn ∅
18 6 fneq1d ⊢ F = ∅ → F -1 Fn A ↔ ∅ Fn A
19 fneq2 ⊢ A = ∅ → ∅ Fn A ↔ ∅ Fn ∅
20 18 19 sylan9bb ⊢ F = ∅ ∧ A = ∅ → F -1 Fn A ↔ ∅ Fn ∅
21 17 20 mpbiri ⊢ F = ∅ ∧ A = ∅ → F -1 Fn A
22 14 21 jca ⊢ F = ∅ ∧ A = ∅ → F Fn ∅ ∧ F -1 Fn A
23 13 22 impbii ⊢ F Fn ∅ ∧ F -1 Fn A ↔ F = ∅ ∧ A = ∅
24 1 23 bitri ⊢ F : ∅ ⟶ 1-1 onto A ↔ F = ∅ ∧ A = ∅