Theorem f1o00

Description: One-to-one onto mapping of the empty set. (Contributed by NM, 15-Apr-1998)

	Ref	Expression
Assertion	f1o00	|- ( F : (/) -1-1-onto-> A <-> ( F = (/) /\ A = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		dff1o4	|- ( F : (/) -1-1-onto-> A <-> ( F Fn (/) /\ `' F Fn A ) )
2		fn0	|- ( F Fn (/) <-> F = (/) )
3	2	birani	|- ( ( F Fn (/) /\ `' F Fn A ) -> F = (/) )
4		cnveq	|- ( F = (/) -> `' F = `' (/) )
5		cnv0	|- `' (/) = (/)
6	4 5	eqtrdi	|- ( F = (/) -> `' F = (/) )
7	2 6	sylbi	|- ( F Fn (/) -> `' F = (/) )
8	7	fneq1d	|- ( F Fn (/) -> ( `' F Fn A <-> (/) Fn A ) )
9	8	biimpa	|- ( ( F Fn (/) /\ `' F Fn A ) -> (/) Fn A )
10	9	fndmd	|- ( ( F Fn (/) /\ `' F Fn A ) -> dom (/) = A )
11		dm0	|- dom (/) = (/)
12	10 11	eqtr3di	|- ( ( F Fn (/) /\ `' F Fn A ) -> A = (/) )
13	3 12	jca	|- ( ( F Fn (/) /\ `' F Fn A ) -> ( F = (/) /\ A = (/) ) )
14	2	biranri	|- ( ( F = (/) /\ A = (/) ) -> F Fn (/) )
15		eqid	|- (/) = (/)
16		fn0	|- ( (/) Fn (/) <-> (/) = (/) )
17	15 16	mpbir	|- (/) Fn (/)
18	6	fneq1d	|- ( F = (/) -> ( `' F Fn A <-> (/) Fn A ) )
19		fneq2	|- ( A = (/) -> ( (/) Fn A <-> (/) Fn (/) ) )
20	18 19	sylan9bb	|- ( ( F = (/) /\ A = (/) ) -> ( `' F Fn A <-> (/) Fn (/) ) )
21	17 20	mpbiri	|- ( ( F = (/) /\ A = (/) ) -> `' F Fn A )
22	14 21	jca	|- ( ( F = (/) /\ A = (/) ) -> ( F Fn (/) /\ `' F Fn A ) )
23	13 22	impbii	|- ( ( F Fn (/) /\ `' F Fn A ) <-> ( F = (/) /\ A = (/) ) )
24	1 23	bitri	|- ( F : (/) -1-1-onto-> A <-> ( F = (/) /\ A = (/) ) )