Theorem fodmrnu

Description: An onto function has unique domain and range. (Contributed by NM, 5-Nov-2006)

	Ref	Expression
Assertion	fodmrnu	|- ( ( F : A -onto-> B /\ F : C -onto-> D ) -> ( A = C /\ B = D ) )

Proof

Step	Hyp	Ref	Expression
1		fofn	|- ( F : A -onto-> B -> F Fn A )
2		fofn	|- ( F : C -onto-> D -> F Fn C )
3		fndmu	|- ( ( F Fn A /\ F Fn C ) -> A = C )
4	1 2 3	syl2an	|- ( ( F : A -onto-> B /\ F : C -onto-> D ) -> A = C )
5		forn	|- ( F : A -onto-> B -> ran F = B )
6		forn	|- ( F : C -onto-> D -> ran F = D )
7	5 6	sylan9req	|- ( ( F : A -onto-> B /\ F : C -onto-> D ) -> B = D )
8	4 7	jca	|- ( ( F : A -onto-> B /\ F : C -onto-> D ) -> ( A = C /\ B = D ) )