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	birani	⊢ ( ( 𝐹 Fn ∅ ∧ ◡ 𝐹 Fn 𝐴 ) → 𝐹 = ∅ )
4		cnveq	⊢ ( 𝐹 = ∅ → ◡ 𝐹 = ◡ ∅ )
5		cnv0	⊢ ◡ ∅ = ∅
6	4 5	eqtrdi	⊢ ( 𝐹 = ∅ → ◡ 𝐹 = ∅ )
7	2 6	sylbi	⊢ ( 𝐹 Fn ∅ → ◡ 𝐹 = ∅ )
8	7	fneq1d	⊢ ( 𝐹 Fn ∅ → ( ◡ 𝐹 Fn 𝐴 ↔ ∅ Fn 𝐴 ) )
9	8	biimpa	⊢ ( ( 𝐹 Fn ∅ ∧ ◡ 𝐹 Fn 𝐴 ) → ∅ Fn 𝐴 )
10	9	fndmd	⊢ ( ( 𝐹 Fn ∅ ∧ ◡ 𝐹 Fn 𝐴 ) → dom ∅ = 𝐴 )
11		dm0	⊢ dom ∅ = ∅
12	10 11	eqtr3di	⊢ ( ( 𝐹 Fn ∅ ∧ ◡ 𝐹 Fn 𝐴 ) → 𝐴 = ∅ )
13	3 12	jca	⊢ ( ( 𝐹 Fn ∅ ∧ ◡ 𝐹 Fn 𝐴 ) → ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )
14	2	biranri	⊢ ( ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) → 𝐹 Fn ∅ )
15		eqid	⊢ ∅ = ∅
16		fn0	⊢ ( ∅ Fn ∅ ↔ ∅ = ∅ )
17	15 16	mpbir	⊢ ∅ Fn ∅
18	6	fneq1d	⊢ ( 𝐹 = ∅ → ( ◡ 𝐹 Fn 𝐴 ↔ ∅ Fn 𝐴 ) )
19		fneq2	⊢ ( 𝐴 = ∅ → ( ∅ Fn 𝐴 ↔ ∅ Fn ∅ ) )
20	18 19	sylan9bb	⊢ ( ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) → ( ◡ 𝐹 Fn 𝐴 ↔ ∅ Fn ∅ ) )
21	17 20	mpbiri	⊢ ( ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) → ◡ 𝐹 Fn 𝐴 )
22	14 21	jca	⊢ ( ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) → ( 𝐹 Fn ∅ ∧ ◡ 𝐹 Fn 𝐴 ) )
23	13 22	impbii	⊢ ( ( 𝐹 Fn ∅ ∧ ◡ 𝐹 Fn 𝐴 ) ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )
24	1 23	bitri	⊢ ( 𝐹 : ∅ –1-1-onto→ 𝐴 ↔ ( 𝐹 = ∅ ∧ 𝐴 = ∅ ) )