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	biimpi	|- ( F Fn (/) -> F = (/) )
4	3	adantr	|- ( ( F Fn (/) /\ `' F Fn A ) -> F = (/) )
5		cnveq	|- ( F = (/) -> `' F = `' (/) )
6		cnv0	|- `' (/) = (/)
7	5 6	eqtrdi	|- ( F = (/) -> `' F = (/) )
8	2 7	sylbi	|- ( F Fn (/) -> `' F = (/) )
9	8	fneq1d	|- ( F Fn (/) -> ( `' F Fn A <-> (/) Fn A ) )
10	9	biimpa	|- ( ( F Fn (/) /\ `' F Fn A ) -> (/) Fn A )
11	10	fndmd	|- ( ( F Fn (/) /\ `' F Fn A ) -> dom (/) = A )
12		dm0	|- dom (/) = (/)
13	11 12	eqtr3di	|- ( ( F Fn (/) /\ `' F Fn A ) -> A = (/) )
14	4 13	jca	|- ( ( F Fn (/) /\ `' F Fn A ) -> ( F = (/) /\ A = (/) ) )
15	2	biimpri	|- ( F = (/) -> F Fn (/) )
16	15	adantr	|- ( ( F = (/) /\ A = (/) ) -> F Fn (/) )
17		eqid	|- (/) = (/)
18		fn0	|- ( (/) Fn (/) <-> (/) = (/) )
19	17 18	mpbir	|- (/) Fn (/)
20	7	fneq1d	|- ( F = (/) -> ( `' F Fn A <-> (/) Fn A ) )
21		fneq2	|- ( A = (/) -> ( (/) Fn A <-> (/) Fn (/) ) )
22	20 21	sylan9bb	|- ( ( F = (/) /\ A = (/) ) -> ( `' F Fn A <-> (/) Fn (/) ) )
23	19 22	mpbiri	|- ( ( F = (/) /\ A = (/) ) -> `' F Fn A )
24	16 23	jca	|- ( ( F = (/) /\ A = (/) ) -> ( F Fn (/) /\ `' F Fn A ) )
25	14 24	impbii	|- ( ( F Fn (/) /\ `' F Fn A ) <-> ( F = (/) /\ A = (/) ) )
26	1 25	bitri	|- ( F : (/) -1-1-onto-> A <-> ( F = (/) /\ A = (/) ) )