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	$$⊢\left(A\in \mathrm{Fin}\wedge \neg B\in \mathrm{Fin}\right)\to \neg \exists ff:A\underset{1-1\; onto}{⟶}B$$

Proof

Step	Hyp	Ref	Expression
1		f1ofo	$$⊢f:A\underset{1-1\; onto}{⟶}B\to f:A\underset{onto}{⟶}B$$
2		fofi	$$⊢\left(A\in \mathrm{Fin}\wedge f:A\underset{onto}{⟶}B\right)\to B\in \mathrm{Fin}$$
3	2	ex	$$⊢A\in \mathrm{Fin}\to \left(f:A\underset{onto}{⟶}B\to B\in \mathrm{Fin}\right)$$
4	1 3	syl5	$$⊢A\in \mathrm{Fin}\to \left(f:A\underset{1-1\; onto}{⟶}B\to B\in \mathrm{Fin}\right)$$
5	4	exlimdv	$$⊢A\in \mathrm{Fin}\to \left(\exists ff:A\underset{1-1\; onto}{⟶}B\to B\in \mathrm{Fin}\right)$$
6	5	con3dimp	$$⊢\left(A\in \mathrm{Fin}\wedge \neg B\in \mathrm{Fin}\right)\to \neg \exists ff:A\underset{1-1\; onto}{⟶}B$$