Metamath Proof Explorer


Theorem seqexw

Description: Weak version of seqex that holds without ax-rep . A sequence builder exists when its binary operation input exists and its starting index is an integer. (Contributed by Rohan Ridenour, 14-Aug-2023)

Ref Expression
Hypotheses seqexw.1 + ˙ V
seqexw.2 M
Assertion seqexw seq M + ˙ F V

Proof

Step Hyp Ref Expression
1 seqexw.1 + ˙ V
2 seqexw.2 M
3 seqfn M seq M + ˙ F Fn M
4 2 3 ax-mp seq M + ˙ F Fn M
5 fnfun seq M + ˙ F Fn M Fun seq M + ˙ F
6 4 5 ax-mp Fun seq M + ˙ F
7 4 fndmi dom seq M + ˙ F = M
8 fvex M V
9 7 8 eqeltri dom seq M + ˙ F V
10 1 rnex ran + ˙ V
11 prex F M V
12 10 11 unex ran + ˙ F M V
13 fveq2 y = M seq M + ˙ F y = seq M + ˙ F M
14 13 eleq1d y = M seq M + ˙ F y ran + ˙ F M seq M + ˙ F M ran + ˙ F M
15 fveq2 y = z seq M + ˙ F y = seq M + ˙ F z
16 15 eleq1d y = z seq M + ˙ F y ran + ˙ F M seq M + ˙ F z ran + ˙ F M
17 fveq2 y = z + 1 seq M + ˙ F y = seq M + ˙ F z + 1
18 17 eleq1d y = z + 1 seq M + ˙ F y ran + ˙ F M seq M + ˙ F z + 1 ran + ˙ F M
19 fveq2 y = x seq M + ˙ F y = seq M + ˙ F x
20 19 eleq1d y = x seq M + ˙ F y ran + ˙ F M seq M + ˙ F x ran + ˙ F M
21 seq1 M seq M + ˙ F M = F M
22 ssun2 F M ran + ˙ F M
23 fvex F M V
24 23 prid2 F M F M
25 22 24 sselii F M ran + ˙ F M
26 21 25 eqeltrdi M seq M + ˙ F M ran + ˙ F M
27 seqp1 z M seq M + ˙ F z + 1 = seq M + ˙ F z + ˙ F z + 1
28 27 adantr z M seq M + ˙ F z ran + ˙ F M seq M + ˙ F z + 1 = seq M + ˙ F z + ˙ F z + 1
29 df-ov seq M + ˙ F z + ˙ F z + 1 = + ˙ seq M + ˙ F z F z + 1
30 snsspr1 F M
31 unss2 F M ran + ˙ ran + ˙ F M
32 30 31 ax-mp ran + ˙ ran + ˙ F M
33 fvrn0 + ˙ seq M + ˙ F z F z + 1 ran + ˙
34 32 33 sselii + ˙ seq M + ˙ F z F z + 1 ran + ˙ F M
35 29 34 eqeltri seq M + ˙ F z + ˙ F z + 1 ran + ˙ F M
36 35 a1i z M seq M + ˙ F z ran + ˙ F M seq M + ˙ F z + ˙ F z + 1 ran + ˙ F M
37 28 36 eqeltrd z M seq M + ˙ F z ran + ˙ F M seq M + ˙ F z + 1 ran + ˙ F M
38 37 ex z M seq M + ˙ F z ran + ˙ F M seq M + ˙ F z + 1 ran + ˙ F M
39 14 16 18 20 26 38 uzind4 x M seq M + ˙ F x ran + ˙ F M
40 39 rgen x M seq M + ˙ F x ran + ˙ F M
41 fnfvrnss seq M + ˙ F Fn M x M seq M + ˙ F x ran + ˙ F M ran seq M + ˙ F ran + ˙ F M
42 4 40 41 mp2an ran seq M + ˙ F ran + ˙ F M
43 12 42 ssexi ran seq M + ˙ F V
44 funexw Fun seq M + ˙ F dom seq M + ˙ F V ran seq M + ˙ F V seq M + ˙ F V
45 6 9 43 44 mp3an seq M + ˙ F V