Theorem f1domg

Description: The domain of a one-to-one function is dominated by its codomain. (Contributed by NM, 4-Sep-2004)

	Ref	Expression
Assertion	f1domg	|- ( B e. C -> ( F : A -1-1-> B -> A ~<_ B ) )

Proof

Step	Hyp	Ref	Expression
1		f1f	|- ( F : A -1-1-> B -> F : A --> B )
2		f1dmex	|- ( ( F : A -1-1-> B /\ B e. C ) -> A e. _V )
3		fex	|- ( ( F : A --> B /\ A e. _V ) -> F e. _V )
4	1 2 3	syl2an2r	|- ( ( F : A -1-1-> B /\ B e. C ) -> F e. _V )
5	4	expcom	|- ( B e. C -> ( F : A -1-1-> B -> F e. _V ) )
6		f1eq1	|- ( f = F -> ( f : A -1-1-> B <-> F : A -1-1-> B ) )
7	6	spcegv	|- ( F e. _V -> ( F : A -1-1-> B -> E. f f : A -1-1-> B ) )
8	5 7	syli	|- ( B e. C -> ( F : A -1-1-> B -> E. f f : A -1-1-> B ) )
9		brdomg	|- ( B e. C -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
10	8 9	sylibrd	|- ( B e. C -> ( F : A -1-1-> B -> A ~<_ B ) )