Theorem fiinfnf1o

Description: There is no bijection between a finite set and an infinite set. (Contributed by Alexander van der Vekens, 25-Dec-2017)

	Ref	Expression
Assertion	fiinfnf1o	|- ( ( A e. Fin /\ -. B e. Fin ) -> -. E. f f : A -1-1-onto-> B )

Proof

Step	Hyp	Ref	Expression
1		f1ofo	|- ( f : A -1-1-onto-> B -> f : A -onto-> B )
2		fofi	|- ( ( A e. Fin /\ f : A -onto-> B ) -> B e. Fin )
3	2	ex	|- ( A e. Fin -> ( f : A -onto-> B -> B e. Fin ) )
4	1 3	syl5	|- ( A e. Fin -> ( f : A -1-1-onto-> B -> B e. Fin ) )
5	4	exlimdv	|- ( A e. Fin -> ( E. f f : A -1-1-onto-> B -> B e. Fin ) )
6	5	con3dimp	|- ( ( A e. Fin /\ -. B e. Fin ) -> -. E. f f : A -1-1-onto-> B )