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