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