This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐹 : ∅ –1-1-onto→ 𝐴 ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )

Proof

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