Theorem fmtnorn

Description: A Fermat number is a function value of the enumeration of the Fermat numbers. (Contributed by AV, 3-Aug-2021)

	Ref	Expression
Assertion	fmtnorn	⊢ ( 𝐹 ∈ ran FermatNo ↔ ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		ovex	⊢ ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) ∈ V
2		df-fmtno	⊢ FermatNo = ( 𝑛 ∈ ℕ0 ↦ ( ( 2 ↑ ( 2 ↑ 𝑛 ) ) + 1 ) )
3	1 2	fnmpti	⊢ FermatNo Fn ℕ0
4		fvelrnb	⊢ ( FermatNo Fn ℕ0 → ( 𝐹 ∈ ran FermatNo ↔ ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = 𝐹 ) )
5	3 4	ax-mp	⊢ ( 𝐹 ∈ ran FermatNo ↔ ∃ 𝑛 ∈ ℕ0 ( FermatNo ‘ 𝑛 ) = 𝐹 )