Metamath Proof Explorer

Theorem seqcl

Description: Closure properties of the recursive sequence builder. (Contributed by Mario Carneiro, 2-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

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

Proof

Step Hyp Ref Expression
1 seqcl.1 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
2 seqcl.2 ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}\right)\right)\to {F}\left({x}\right)\in {S}$
3 seqcl.3
4 fveq2 ${⊢}{x}={M}\to {F}\left({x}\right)={F}\left({M}\right)$
5 4 eleq1d ${⊢}{x}={M}\to \left({F}\left({x}\right)\in {S}↔{F}\left({M}\right)\in {S}\right)$
6 2 ralrimiva ${⊢}{\phi }\to \forall {x}\in \left({M}\dots {N}\right)\phantom{\rule{.4em}{0ex}}{F}\left({x}\right)\in {S}$
7 eluzfz1 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in \left({M}\dots {N}\right)$
8 1 7 syl ${⊢}{\phi }\to {M}\in \left({M}\dots {N}\right)$
9 5 6 8 rspcdva ${⊢}{\phi }\to {F}\left({M}\right)\in {S}$
10 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
11 1 10 syl ${⊢}{\phi }\to {M}\in ℤ$
12 fzp1ss ${⊢}{M}\in ℤ\to \left({M}+1\dots {N}\right)\subseteq \left({M}\dots {N}\right)$
13 11 12 syl ${⊢}{\phi }\to \left({M}+1\dots {N}\right)\subseteq \left({M}\dots {N}\right)$
14 13 sselda ${⊢}\left({\phi }\wedge {x}\in \left({M}+1\dots {N}\right)\right)\to {x}\in \left({M}\dots {N}\right)$
15 14 2 syldan ${⊢}\left({\phi }\wedge {x}\in \left({M}+1\dots {N}\right)\right)\to {F}\left({x}\right)\in {S}$
16 9 3 1 15 seqcl2