Theorem fmtnoinf

Description: The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021)

	Ref	Expression
Assertion	fmtnoinf	⊢ ran FermatNo ∉ Fin

Proof

Step	Hyp	Ref	Expression
1		fmtnof1	⊢ FermatNo : ℕ0 –1-1→ ℕ
2		f1f	⊢ ( FermatNo : ℕ0 –1-1→ ℕ → FermatNo : ℕ0 ⟶ ℕ )
3		fdm	⊢ ( FermatNo : ℕ0 ⟶ ℕ → dom FermatNo = ℕ0 )
4		nnssnn0	⊢ ℕ ⊆ ℕ0
5		nnnfi	⊢ ¬ ℕ ∈ Fin
6		ssfi	⊢ ( ( ℕ0 ∈ Fin ∧ ℕ ⊆ ℕ0 ) → ℕ ∈ Fin )
7	6	expcom	⊢ ( ℕ ⊆ ℕ0 → ( ℕ0 ∈ Fin → ℕ ∈ Fin ) )
8	7	con3d	⊢ ( ℕ ⊆ ℕ0 → ( ¬ ℕ ∈ Fin → ¬ ℕ0 ∈ Fin ) )
9	4 5 8	mp2	⊢ ¬ ℕ0 ∈ Fin
10		eleq1	⊢ ( dom FermatNo = ℕ0 → ( dom FermatNo ∈ Fin ↔ ℕ0 ∈ Fin ) )
11	9 10	mtbiri	⊢ ( dom FermatNo = ℕ0 → ¬ dom FermatNo ∈ Fin )
12	3 11	syl	⊢ ( FermatNo : ℕ0 ⟶ ℕ → ¬ dom FermatNo ∈ Fin )
13		ffun	⊢ ( FermatNo : ℕ0 ⟶ ℕ → Fun FermatNo )
14		fundmfibi	⊢ ( Fun FermatNo → ( FermatNo ∈ Fin ↔ dom FermatNo ∈ Fin ) )
15	13 14	syl	⊢ ( FermatNo : ℕ0 ⟶ ℕ → ( FermatNo ∈ Fin ↔ dom FermatNo ∈ Fin ) )
16	12 15	mtbird	⊢ ( FermatNo : ℕ0 ⟶ ℕ → ¬ FermatNo ∈ Fin )
17	1 2 16	mp2b	⊢ ¬ FermatNo ∈ Fin
18		nn0ex	⊢ ℕ0 ∈ V
19		f1dmvrnfibi	⊢ ( ( ℕ0 ∈ V ∧ FermatNo : ℕ0 –1-1→ ℕ ) → ( FermatNo ∈ Fin ↔ ran FermatNo ∈ Fin ) )
20	19	notbid	⊢ ( ( ℕ0 ∈ V ∧ FermatNo : ℕ0 –1-1→ ℕ ) → ( ¬ FermatNo ∈ Fin ↔ ¬ ran FermatNo ∈ Fin ) )
21	18 1 20	mp2an	⊢ ( ¬ FermatNo ∈ Fin ↔ ¬ ran FermatNo ∈ Fin )
22	17 21	mpbi	⊢ ¬ ran FermatNo ∈ Fin
23	22	nelir	⊢ ran FermatNo ∉ Fin