HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem seq1rn2 6321
Description: Range of the recursive sequence builder.
Hypotheses
Ref Expression
seq111.1 |- S e. V
seq111.2 |- F e. V
Assertion
Ref Expression
seq1rn2 |- (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ran ( S seq1 F) (_ C)
Proof of Theorem seq1rn2
StepHypRef Expression
1 fveq2 3724 . . . . . . 7 |- (y = 1 -> ((S seq1 F)` y) = ((S seq1 F)` 1))
21eleq1d 1540 . . . . . 6 |- (y = 1 -> (((S seq1 F)` y) e. C <-> ((S seq1 F)` 1) e. C))
32imbi2d 612 . . . . 5 |- (y = 1 -> ((((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((S seq1 F)` y) e. C) <-> (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((S seq1 F)` 1) e. C)))
4 fveq2 3724 . . . . . . 7 |- (y = z -> ((S seq1 F)` y) = ((S seq1 F)` z))
54eleq1d 1540 . . . . . 6 |- (y = z -> (((S seq1 F)` y) e. C <-> ((S seq1 F)` z) e. C))
65imbi2d 612 . . . . 5 |- (y = z -> ((((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((S seq1 F)` y) e. C) <-> (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((S seq1 F)` z) e. C)))
7 fveq2 3724 . . . . . . 7 |- (y = (z + 1) -> ((S seq1 F)` y) = ((S seq1 F)` (z + 1)))
87eleq1d 1540 . . . . . 6 |- (y = (z + 1) -> (((S seq1 F)` y) e. C <-> ((S seq1 F)` (z + 1)) e. C))
98imbi2d 612 . . . . 5 |- (y = (z + 1) -> ((((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((S seq1 F)` y) e. C) <-> (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((S seq1 F)` (z + 1)) e. C)))
10 fveq2 3724 . . . . . . 7 |- (y = x -> ((S seq1 F)` y) = ((S seq1 F)` x))
1110eleq1d 1540 . . . . . 6 |- (y = x -> (((S seq1 F)` y) e. C <-> ((S seq1 F)` x) e. C))
1211imbi2d 612 . . . . 5 |- (y = x -> ((((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((S seq1 F)` y) e. C) <-> (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((S seq1 F)` x) e. C)))
13 pm3.26 319 . . . . . . 7 |- (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D) -> (F` 1) e. C)
14 seq111.1 . . . . . . . 8 |- S e. V
15 seq111.2 . . . . . . . 8 |- F e. V
1614, 15seq11 6317 . . . . . . 7 |- ((S seq1 F)` 1) = (F` 1)
1713, 16syl5eqel 1552 . . . . . 6 |- (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D) -> ((S seq1 F)` 1) e. C)
18173adant3 799 . . . . 5 |- (((F` 1) e. C /\ (F |` (NN \ {1})):(NN \ {1})-->D /\ S:(C X. D)-->C) -> ((S seq1 F)` 1) e. C)
19 ffvelrn 3814 . . . . . . . . . . . . . 14 |- (((F |` (NN \ {1})):(NN \ {1})-->D /\ (z + 1) e. (NN \ {1})) -> ((F |` (NN \ {1}))` (z + 1)) e. D)
20 fvres 3734 . . . . . . . . . . . . . . . 16 |- ((z + 1) e. (NN \ {1}) -> ((F |` (NN \ {1}))` (z + 1)) = (F` (z + 1)))
2120eleq1d 1540 . . . . . . . . . . . . . . 15 |- ((z + 1) e. (NN \ {1}) -> (((F |` (NN \ {1}))` (z + 1)) e. D <-> (F` (z + 1)) e. D))
2221adantl 388 . . . . . . . . . . . . . 14 |- (((F |` (NN \ {1})):(NN \ {1})-->D /\ (z + 1) e. (NN \ {1})) -> (((F |` (NN \ {1}))` (z + 1)) e. D <-> (F` (z + 1)) e. D))
2319, 22mpbid 195 . . . . . . . . . . . . 13 |- (((F |` (NN \ {1})):(NN \ {1})-->D /\ (z + 1) e. (NN \ {1})) -> (F` (z + 1)) e. D)
24 seq1lem2 6310 . . . . . . . . . . . . 13 |- (z e. NN -> (z + 1) e. (NN \ {1}))
2523, 24sylan2 451 . . . . . . . . . . . 12 |- (((F |` (NN \ {1})):(NN \ {1})-->D /\ z e. NN) -> (F` (z + 1)) e. D)
2614, 15seq1p1 6318 . . . . . . . . . . . . . . . 16 |- (z e. NN -> ((S seq1 F)` (z + 1)) = (((S seq1 F)` z)S(F` (z + 1))))
2726eleq1d 1540 . . . . . . . . . . . . . . 15 |- (z e. NN -> (((S seq1 F)` (z + 1)) e. C <-> (((S seq1 F)` z)S(F` (z + 1))) e. C))
28 opreq1 3968 . . . . . . . . . . . . . . . . . . . 20 |- (w = ((S seq1 F)` z) -> (wSv) = (((S seq1 F)` z)Sv))
2928eleq1d 1540 . . . . . . . . . . . . . . . . . . 19 |- (w = ((S seq1 F)` z) -> ((wSv) e. C <-> (((S seq1 F)` z)Sv) e. C))
30 opreq2 3969 . . . . . . . . . . . . . . . . . . . 20 |- (v = (F` (z + 1)) -> (((S seq1 F)` z)Sv) = (((S seq1 F)` z)S(F` (z + 1))))
3130eleq1d 1540 . . . . . . . . . . . . . . . . . . 19 |- (v = (F` (z + 1)) -> ((((S seq1 F)` z)Sv) e. C <-> (((S seq1 F)` z)S(F` (z + 1))) e. C))
3229, 31rcla42v 1880 . . . . . . . . . . . . . . . . . 18 |- ((((S seq1 F)` z) e. C /\ (F` (z + 1)) e. D) -> (A.w e. C A.v e. D (wSv) e. C -> (((S seq1 F)` z)S(F` (z + 1))) e. C))
3332ancoms 436 . . . . . . . . . . . . . . . . 17 |- (((F` (z + 1)) e. D /\ ((S seq1 F)` z) e. C) -> (A.w e. C A.v e. D (wSv) e. C -> (((S seq1 F)` z)S(F` (z + 1))) e. C))
34 ffnoprval 4014 . . . . . . . . . . . . . . . . . 18 |- (S:(C X. D)-->C <-> (S Fn (C X. D) /\ A.w e. C A.v e. D (wSv) e. C))
3534pm3.27bi 326 . . . . . . . . . . . . . . . . 17 |- (S:(C X. D)-->C -> A.w e. C A.v e. D (wSv) e. C)
3633, 35syl5 21 . . . . . . . . . . . . . . . 16 |- (((F` (z + 1)) e. D /\ ((S seq1 F)` z) e. C) -> (S:(C X. D)-->C -> (((S seq1 F)` z)S(F` (z + 1))) e. C))
3736imp 350 . . . . . . . . . . . . . . 15 |- ((((F` (z + 1)) e. D /\ ((S seq1 F)` z) e. C) /\ S:(C X. D)-->C) -> (((S seq1 F)` z)S(F` (z + 1))) e. C)
3827, 37syl5bir 210 . . . . . . . . . . . . . 14 |- (z e. NN -> ((((F` (z + 1)) e. D /\ ((S seq1 F)` z) e. C) /\ S:(C X. D)-->C) -> ((S seq1 F)` (z + 1)) e. C))
3938exp4c 380 . . . . . . . . . . . . 13 |- (z e. NN -> ((F` (z + 1)) e. D -> (((S seq1 F)` z) e. C -> (S:(C X. D)-->C -> ((S seq1 F)` (z + 1)) e. C))))
4039adantl 388 . . . . . . . . . . . 12 |- (((F |` (NN \ {1})):(NN \ {1})-->D /\ z e. NN) -> ((F` (z + 1)) e. D -> (((S seq1