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	⊢ ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ¬ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		f1ofo	⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –onto→ 𝐵 )
2		fofi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝑓 : 𝐴 –onto→ 𝐵 ) → 𝐵 ∈ Fin )
3	2	ex	⊢ ( 𝐴 ∈ Fin → ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ Fin ) )
4	1 3	syl5	⊢ ( 𝐴 ∈ Fin → ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝐵 ∈ Fin ) )
5	4	exlimdv	⊢ ( 𝐴 ∈ Fin → ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝐵 ∈ Fin ) )
6	5	con3dimp	⊢ ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ¬ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )