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		dm0	⊢ dom ∅ = ∅
6		cnveq	⊢ ( 𝐹 = ∅ → ◡ 𝐹 = ◡ ∅ )
7		cnv0	⊢ ◡ ∅ = ∅
8	6 7	syl6eq	⊢ ( 𝐹 = ∅ → ◡ 𝐹 = ∅ )
9	2 8	sylbi	⊢ ( 𝐹 Fn ∅ → ◡ 𝐹 = ∅ )
10	9	fneq1d	⊢ ( 𝐹 Fn ∅ → ( ◡ 𝐹 Fn 𝐴 ↔ ∅ Fn 𝐴 ) )
11	10	biimpa	⊢ ( ( 𝐹 Fn ∅ ∧ ◡ 𝐹 Fn 𝐴 ) → ∅ Fn 𝐴 )
12	11	fndmd	⊢ ( ( 𝐹 Fn ∅ ∧ ◡ 𝐹 Fn 𝐴 ) → dom ∅ = 𝐴 )
13	5 12	syl5reqr	⊢ ( ( 𝐹 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	8	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→ 𝐴 ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )