# Metamath Proof Explorer

## Theorem seqf

Description: Range of the recursive sequence builder (special case of seqf2 ). (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypotheses seqf.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
seqf.2 ${⊢}{\phi }\to {M}\in ℤ$
seqf.3 ${⊢}\left({\phi }\wedge {x}\in {Z}\right)\to {F}\left({x}\right)\in {S}$
seqf.4
Assertion seqf

### Proof

Step Hyp Ref Expression
1 seqf.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 seqf.2 ${⊢}{\phi }\to {M}\in ℤ$
3 seqf.3 ${⊢}\left({\phi }\wedge {x}\in {Z}\right)\to {F}\left({x}\right)\in {S}$
4 seqf.4
5 fveq2 ${⊢}{x}={M}\to {F}\left({x}\right)={F}\left({M}\right)$
6 5 eleq1d ${⊢}{x}={M}\to \left({F}\left({x}\right)\in {S}↔{F}\left({M}\right)\in {S}\right)$
7 3 ralrimiva ${⊢}{\phi }\to \forall {x}\in {Z}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {S}$
8 uzid ${⊢}{M}\in ℤ\to {M}\in {ℤ}_{\ge {M}}$
9 2 8 syl ${⊢}{\phi }\to {M}\in {ℤ}_{\ge {M}}$
10 9 1 eleqtrrdi ${⊢}{\phi }\to {M}\in {Z}$
11 6 7 10 rspcdva ${⊢}{\phi }\to {F}\left({M}\right)\in {S}$
12 peano2uzr ${⊢}\left({M}\in ℤ\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}\in {ℤ}_{\ge {M}}$
13 2 12 sylan ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}\in {ℤ}_{\ge {M}}$
14 13 1 eleqtrrdi ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {x}\in {Z}$
15 14 3 syldan ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {F}\left({x}\right)\in {S}$
16 11 4 1 2 15 seqf2