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 biimpi ⊢ F Fn ∅ → F = ∅
4 3 adantr ⊢ F Fn ∅ ∧ F -1 Fn A → F = ∅
5 cnveq ⊢ F = ∅ → F -1 = ∅ -1
6 cnv0 ⊢ ∅ -1 = ∅
7 5 6 eqtrdi ⊢ F = ∅ → F -1 = ∅
8 2 7 sylbi ⊢ F Fn ∅ → F -1 = ∅
9 8 fneq1d ⊢ F Fn ∅ → F -1 Fn A ↔ ∅ Fn A
10 9 biimpa ⊢ F Fn ∅ ∧ F -1 Fn A → ∅ Fn A
11 10 fndmd ⊢ F Fn ∅ ∧ F -1 Fn A → dom ⁡ ∅ = A
12 dm0 ⊢ dom ⁡ ∅ = ∅
13 11 12 eqtr3di ⊢ F Fn ∅ ∧ F -1 Fn A → A = ∅
14 4 13 jca ⊢ F Fn ∅ ∧ F -1 Fn A → F = ∅ ∧ A = ∅
15 2 biimpri ⊢ F = ∅ → F Fn ∅
16 15 adantr ⊢ F = ∅ ∧ A = ∅ → F Fn ∅
17 eqid ⊢ ∅ = ∅
18 fn0 ⊢ ∅ Fn ∅ ↔ ∅ = ∅
19 17 18 mpbir ⊢ ∅ Fn ∅
20 7 fneq1d ⊢ F = ∅ → F -1 Fn A ↔ ∅ Fn A
21 fneq2 ⊢ A = ∅ → ∅ Fn A ↔ ∅ Fn ∅
22 20 21 sylan9bb ⊢ F = ∅ ∧ A = ∅ → F -1 Fn A ↔ ∅ Fn ∅
23 19 22 mpbiri ⊢ F = ∅ ∧ A = ∅ → F -1 Fn A
24 16 23 jca ⊢ F = ∅ ∧ A = ∅ → F Fn ∅ ∧ F -1 Fn A
25 14 24 impbii ⊢ F Fn ∅ ∧ F -1 Fn A ↔ F = ∅ ∧ A = ∅
26 1 25 bitri ⊢ F : ∅ ⟶ 1-1 onto A ↔ F = ∅ ∧ A = ∅