Theorem seqzrn2 6557

Description: Range of a sequence generated by the arbitrary-based recursive sequence builder.

Hypotheses

Ref	Expression
seqzrn.1	|- S e. V
seqzrn.2	|- F e. V

Assertion

Ref	Expression
seqzrn2	|- (((M e. ZZ /\ (F` M) e. C) /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> ran (<.M, S>. seq F) (_ C)

Proof of Theorem seqzrn2

Step	Hyp	Ref	Expression
1		fnfvrnss 3836	. . 3 |- (((<.M, S>. seq F) Fn (ZZ>` M) /\ A.n e. (ZZ>` M)((<.M, S>. seq F)` n) e. C) -> ran (<.M, S>. seq F) (_ C)
2		seqzrn.1	. . . 4 |- S e. V
3		seqzrn.2	. . . 4 |- F e. V
4	2, 3	seqzfn 6540	. . 3 |- (M e. ZZ -> (<.M, S>. seq F) Fn (ZZ>` M))
5		fveq2 3730	. . . . . . . 8 |- (j = M -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq F)` M))
6	5	eleq1d 1543	. . . . . . 7 |- (j = M -> (((<.M, S>. seq F)` j) e. C <-> ((<.M, S>. seq F)` M) e. C))
7	6	imbi2d 614	. . . . . 6 |- (j = M -> ((((F` M) e. C /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> ((<.M, S>. seq F)` j) e. C) <-> (((F` M) e. C /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> ((<.M, S>. seq F)` M) e. C)))
8		fveq2 3730	. . . . . . . 8 |- (j = m -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq F)` m))
9	8	eleq1d 1543	. . . . . . 7 |- (j = m -> (((<.M, S>. seq F)` j) e. C <-> ((<.M, S>. seq F)` m) e. C))
10	9	imbi2d 614	. . . . . 6 |- (j = m -> ((((F` M) e. C /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> ((<.M, S>. seq F)` j) e. C) <-> (((F` M) e. C /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> ((<.M, S>. seq F)` m) e. C)))
11		fveq2 3730	. . . . . . . 8 |- (j = (m + 1) -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq F)` (m + 1)))
12	11	eleq1d 1543	. . . . . . 7 |- (j = (m + 1) -> (((<.M, S>. seq F)` j) e. C <-> ((<.M, S>. seq F)` (m + 1)) e. C))
13	12	imbi2d 614	. . . . . 6 |- (j = (m + 1) -> ((((F` M) e. C /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> ((<.M, S>. seq F)` j) e. C) <-> (((F` M) e. C /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> ((<.M, S>. seq F)` (m + 1)) e. C)))
14		fveq2 3730	. . . . . . . 8 |- (j = n -> ((<.M, S>. seq F)` j) = ((<.M, S>. seq F)` n))
15	14	eleq1d 1543	. . . . . . 7 |- (j = n -> (((<.M, S>. seq F)` j) e. C <-> ((<.M, S>. seq F)` n) e. C))
16	15	imbi2d 614	. . . . . 6 |- (j = n -> ((((F` M) e. C /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> ((<.M, S>. seq F)` j) e. C) <-> (((F` M) e. C /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> ((<.M, S>. seq F)` n) e. C)))
17	2, 3	seqz1 6548	. . . . . . . 8 |- (M e. ZZ -> ((<.M, S>. seq F)` M) = (F` M))
18	17	eleq1d 1543	. . . . . . 7 |- (M e. ZZ -> (((<.M, S>. seq F)` M) e. C <-> (F` M) e. C))
19		pm3.26 319	. . . . . . 7 |- (((F` M) e. C /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> (F` M) e. C)
20	18, 19	syl5bir 210	. . . . . 6 |- (M e. ZZ -> (((F` M) e. C /\ ((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ S:(C X. B)-->C)) -> ((<.M, S>. seq F)` M) e. C))
21		ffvelrn 3820	. . . . . . . . . . . . . . 15 |- (((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ (m + 1) e. (ZZ>` (M + 1))) -> ((F |` (ZZ>` (M + 1)))` (m + 1)) e. B)
22		fvres 3740	. . . . . . . . . . . . . . . . 17 |- ((m + 1) e. (ZZ>` (M + 1)) -> ((F |` (ZZ>` (M + 1)))` (m + 1)) = (F` (m + 1)))
23	22	eleq1d 1543	. . . . . . . . . . . . . . . 16 |- ((m + 1) e. (ZZ>` (M + 1)) -> (((F |` (ZZ>` (M + 1)))` (m + 1)) e. B <-> (F` (m + 1)) e. B))
24	23	adantl 390	. . . . . . . . . . . . . . 15 |- (((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ (m + 1) e. (ZZ>` (M + 1))) -> (((F |` (ZZ>` (M + 1)))` (m + 1)) e. B <-> (F` (m + 1)) e. B))
25	21, 24	mpbid 195	. . . . . . . . . . . . . 14 |- (((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ (m + 1) e. (ZZ>` (M + 1))) -> (F` (m + 1)) e. B)
26		eluzp1p1t 6436	. . . . . . . . . . . . . 14 |- (m e. (ZZ>` M) -> (m + 1) e. (ZZ>` (M + 1)))
27	25, 26	sylan2 453	. . . . . . . . . . . . 13 |- (((F |` (ZZ>` (M + 1))):(ZZ>` (M + 1))-->B /\ m e. (ZZ>` M)) -> (F` (m + 1)) e. B)
28	2, 3	seqzp1 6549	. . . . . . . . . . . . . . . . 17 |- (m e. (ZZ>` M) -> ((<.M, S>. seq F)` (m + 1)) = (((<.M, S>. seq F)` m)S(F` (m + 1))))
29	28	eleq1d 1543	. . . . . . . . . . . . . . . 16 |- (m e. (ZZ>` M) -> (((<.M, S>. seq F)` (m + 1)) e. C <-> (((<.M, S>. seq F)` m)S(F` (m + 1))) e. C))
30		opreq1 3974	. . . . . . . . . . . . . . . . . . . . 21 |- (y = ((<.M, S>. seq F)` m) -> (ySv) = (((<.M, S>. seq F)` m)Sv))
31	30	eleq1d 1543	. . . . . . . . . . . . . . . . . . . 20 |- (y = ((<.M, S>. seq F)` m) -> ((ySv) e. C <-> (((<.M, S>. seq F)` m)Sv) e. C))
32		opreq2 3975	. . . . . . . . . . . . . . . . . . . . 21 |- (v = (F` (m + 1)) -> (((<.M, S>. seq F)` m)Sv) = (((<.M, S>. seq F)` m)S(F` (m + 1))))
33	32	eleq1d 1543	. . . . . . . . . . . . . . . . . . . 20 |- (v = (F` (m + 1)) -> ((((<.M, S>. seq F)` m)Sv) e. C <-> (((<.M, S>. seq F)` m)S(F` (m + 1))) e. C))
34	31, 33	rcla42v 1883	. . . . . . . . . . . . . . . . . . 19 |- ((((<.M, S>. seq F)` m) e. C /\ (F` (m + 1)) e. B) -> (A.y e. C A.v e. B (ySv) e. C -> (((<.M, S>. seq F)` m)S(F` (m + 1))) e. C))
35	34	ancoms 438	. . . . . . . . . . . . . . . . . 18 |- (((F` (m + 1)) e. B /\ ((<.M, S>. seq F)` m) e. C) -> (A.y e. C A.v e. B (ySv) e. C -> (((<.M, S>. seq F)` m)S(F` (m + 1)))