Theorem seqrn 4673

Description: Range of the infinite sequence builder.

Hypotheses

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

Assertion

Ref	Expression
seqrn	|- (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ran (SseqF) (_ C)

Proof of Theorem seqrn

Step	Hyp	Ref	Expression
1		fveq2 2832	. . . . . . 7 |- (y = 1 -> ((SseqF)` y) = ((SseqF)` 1))
2	1	eleq1d 1155	. . . . . 6 |- (y = 1 -> (((SseqF)` y) e. C <-> ((SseqF)` 1) e. C))
3	2	imbi2d 464	. . . . 5 |- (y = 1 -> ((((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((SseqF)` y) e. C) <-> (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((SseqF)` 1) e. C)))
4		fveq2 2832	. . . . . . 7 |- (y = z -> ((SseqF)` y) = ((SseqF)` z))
5	4	eleq1d 1155	. . . . . 6 |- (y = z -> (((SseqF)` y) e. C <-> ((SseqF)` z) e. C))
6	5	imbi2d 464	. . . . 5 |- (y = z -> ((((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((SseqF)` y) e. C) <-> (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((SseqF)` z) e. C)))
7		fveq2 2832	. . . . . . 7 |- (y = (z + 1) -> ((SseqF)` y) = ((SseqF)` (z + 1)))
8	7	eleq1d 1155	. . . . . 6 |- (y = (z + 1) -> (((SseqF)` y) e. C <-> ((SseqF)` (z + 1)) e. C))
9	8	imbi2d 464	. . . . 5 |- (y = (z + 1) -> ((((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((SseqF)` y) e. C) <-> (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((SseqF)` (z + 1)) e. C)))
10		fveq2 2832	. . . . . . 7 |- (y = x -> ((SseqF)` y) = ((SseqF)` x))
11	10	eleq1d 1155	. . . . . 6 |- (y = x -> (((SseqF)` y) e. C <-> ((SseqF)` x) e. C))
12	11	imbi2d 464	. . . . 5 |- (y = x -> ((((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((SseqF)` y) e. C) <-> (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((SseqF)` x) e. C)))
13		pm3.26 256	. . . . . . 7 |- (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D) -> (F` 1) e. C)
14		seq1.1	. . . . . . . . 9 |- S e. V
15		seq1.2	. . . . . . . . 9 |- F e. V
16	14, 15	seq1 4670	. . . . . . . 8 |- ((SseqF)` 1) = (F` 1)
17	16	eleq1i 1152	. . . . . . 7 |- (((SseqF)` 1) e. C <-> (F` 1) e. C)
18	13, 17	sylibr 175	. . . . . 6 |- (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D) -> ((SseqF)` 1) e. C)
19	18	3adant3 599	. . . . 5 |- (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((SseqF)` 1) e. C)
20		ffvrn 2890	. . . . . . . . . . . . . . 15 |- (((F |` (NN \ {1})):(NN \ {1})-->D /\ (z + 1) e. (NN \ {1})) -> ((F |` (NN \ {1}))` (z + 1)) e. D)
21		fvres 2840	. . . . . . . . . . . . . . . . 17 |- ((z + 1) e. (NN \ {1}) -> ((F |` (NN \ {1}))` (z + 1)) = (F` (z + 1)))
22	21	eleq1d 1155	. . . . . . . . . . . . . . . 16 |- ((z + 1) e. (NN \ {1}) -> (((F |` (NN \ {1}))` (z + 1)) e. D <-> (F` (z + 1)) e. D))
23	22	adantl 305	. . . . . . . . . . . . . . 15 |- (((F |` (NN \ {1})):(NN \ {1})-->D /\ (z + 1) e. (NN \ {1})) -> (((F |` (NN \ {1}))` (z + 1)) e. D <-> (F` (z + 1)) e. D))
24	20, 23	mpbid 170	. . . . . . . . . . . . . 14 |- (((F |` (NN \ {1})):(NN \ {1})-->D /\ (z + 1) e. (NN \ {1})) -> (F` (z + 1)) e. D)
25		seqlem2 4663	. . . . . . . . . . . . . 14 |- (z e. NN -> (z + 1) e. (NN \ {1}))
26	24, 25	sylan2 346	. . . . . . . . . . . . 13 |- (((F |` (NN \ {1})):(NN \ {1})-->D /\ z e. NN) -> (F` (z + 1)) e. D)
27	14, 15	seqsuc 4671	. . . . . . . . . . . . . . . . . 18 |- (z e. NN -> ((SseqF)` (z + 1)) = (((SseqF)` z)S(F` (z + 1))))
28	27	eleq1d 1155	. . . . . . . . . . . . . . . . 17 |- (z e. NN -> (((SseqF)` (z + 1)) e. C <-> (((SseqF)` z)S(F` (z + 1))) e. C))
29		ffnoprval 3041	. . . . . . . . . . . . . . . . . . . 20 |- (S:(C X. D)-->C <-> (S Fn (C X. D) /\ A.w e. C A.v e. D (wSv) e. C))
30	29	pm3.27bd 263	. . . . . . . . . . . . . . . . . . 19 |- (S:(C X. D)-->C -> A.w e. C A.v e. D (wSv) e. C)
31		opreq1 3006	. . . . . . . . . . . . . . . . . . . . 21 |- (w = ((SseqF)` z) -> (wSv) = (((SseqF)` z)Sv))
32	31	eleq1d 1155	. . . . . . . . . . . . . . . . . . . 20 |- (w = ((SseqF)` z) -> ((wSv) e. C <-> (((SseqF)` z)Sv) e. C))
33		opreq2 3007	. . . . . . . . . . . . . . . . . . . . 21 |- (v = (F` (z + 1)) -> (((SseqF)` z)Sv) = (((SseqF)` z)S(F` (z + 1))))
34	33	eleq1d 1155	. . . . . . . . . . . . . . . . . . . 20 |- (v = (F` (z + 1)) -> ((((SseqF)` z)Sv) e. C <-> (((SseqF)` z)S(F` (z + 1))) e. C))
35	32, 34	rcla42v 1404	. . . . . . . . . . . . . . . . . . 19 |- (A.w e. C A.v e. D (wSv) e. C -> ((((SseqF)` z) e. C /\ (F` (z + 1)) e. D) -> (((SseqF)` z)S(F` (z + 1))) e. C))
36	30, 35	syl 12	. . . . . . . . . . . . . . . . . 18 |- (S:(C X. D)-->C -> ((((SseqF)` z) e. C /\ (F` (z + 1)) e. D) -> (((SseqF)` z)S(F` (z + 1))) e. C))
37	36	imp 277	. . . . . . . . . . . . . . . . 17 |- ((S:(C X. D)-->C /\ (((SseqF)` z) e. C /\ (F` (z + 1)) e. D)) -> (((SseqF)` z)S(F` (z + 1))) e. C)
38	28, 37	syl5bir 184	. . . . . . . . . . . . . . . 16 |- (z e. NN -> ((S:(C X. D)-->C /\ (((SseqF)` z) e. C /\ (F` (z + 1)) e. D)) -> ((SseqF)` (z + 1)) e. C))
39	38	exp4d 298	. . . . . . . . . . . . . . 15 |- (z e. NN -> (S:(C X. D)-->C -> (((SseqF)` z) e. C -> ((F` (z + 1)) e. D -> ((SseqF)` (z + 1)) e. C))))
40	39	com24 37	. . . . . . . . . . . . . 14 |- (z e. NN -> ((F` (z + 1)) e. D -> (((SseqF)` z) e. C -> (S:(C X. D)-->C -> ((SseqF)` (z + 1)) e. C))))
41	40	adantl 305	. . . . . . . . . . . . 13 |- (((F |` (NN \ {1})):(NN \ {1})-->D /\ z e. NN) -> ((F` (z + 1)) e. D -> (((SseqF)` z) e. C -> (S:(C X. D)-->C -> ((SseqF)` (z