Theorem f1domfi2

Description: If the domain of a one-to-one function is finite, then the function's domain is dominated by its codomain when the latter is a set. This theorem is proved without using the Axiom of Power Sets (unlike f1dom2g ). (Contributed by BTernaryTau, 24-Nov-2024)

	Ref	Expression
Assertion	f1domfi2	|- ( ( A e. Fin /\ B e. V /\ F : A -1-1-> B ) -> A ~<_ B )

Proof

Step	Hyp	Ref	Expression
1		f1fn	|- ( F : A -1-1-> B -> F Fn A )
2		fnfi	|- ( ( F Fn A /\ A e. Fin ) -> F e. Fin )
3	1 2	sylan	|- ( ( F : A -1-1-> B /\ A e. Fin ) -> F e. Fin )
4	3	ancoms	|- ( ( A e. Fin /\ F : A -1-1-> B ) -> F e. Fin )
5	4	3adant2	|- ( ( A e. Fin /\ B e. V /\ F : A -1-1-> B ) -> F e. Fin )
6		f1dom3g	|- ( ( F e. Fin /\ B e. V /\ F : A -1-1-> B ) -> A ~<_ B )
7	5 6	syld3an1	|- ( ( A e. Fin /\ B e. V /\ F : A -1-1-> B ) -> A ~<_ B )