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 ontoA↔F=∅∧A=∅

Proof

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