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 \in Fin \land \neg B \in Fin) \to \neg \exists f f : A \underset{1-1 onto}{⟶} B$

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

Metamath Proof Explorer