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

Metamath Proof Explorer

Theorem fo00

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

Ref Expression
Assertion fo00 ( 𝐹 : ∅ –onto→ 𝐴 ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )

Proof

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