seqzfval - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem seqzfval 6469

Description: Value of the arbitrary-based recursive sequence builder operation.

**Hypotheses**
Ref	Expression
seq0val.1
seq0val.2

**Assertion**
Ref	Expression
seqzfval

**Proof of Theorem seqzfval**
Step	Hyp	Ref	Expression
1		seq0val.1	. . . . . . 7
2		op2ndg 4072	. . . . . . 7 $/\$
3	1, 2	mpan2 694	. . . . . 6
4		op1stg 4071	. . . . . . . 8
5	4	opreq2d 3961	. . . . . . 7
6	5	opreq2d 3961	. . . . . 6
7	3, 6	opreq12d 3963	. . . . 5
8	4	opreq1d 3960	. . . . 5
9	7, 8	opreq12d 3963	. . . 4
10		reseq1 3352	. . . 4
11	9, 10	syl 10	. . 3
12	4	breq1d 2619	. . . . 5
13	12	rabbisdv 1798	. . . 4
14		reseq2 3353	. . . 4
15	13, 14	syl 10	. . 3
16	11, 15	eqtrd 1499	. 2
17		opex 2772	. . 3
18		seq0val.2	. . 3
19		oprex 3968	. . . . 5
20		resexg 3378	. . . . 5
21	19, 20	ax-mp 7	. . . 4
22		fveq2 3709	. . . . . . . 8
23		fveq2 3709	. . . . . . . . . 10
24	23	opreq2d 3961	. . . . . . . . 9
25	24	opreq2d 3961	. . . . . . . 8
26	22, 25	opreq12d 3963	. . . . . . 7
27	23	opreq1d 3960	. . . . . . 7
28	26, 27	opreq12d 3963	. . . . . 6
29		reseq1 3352	. . . . . 6
30	28, 29	syl 10	. . . . 5
31	23	breq1d 2619	. . . . . . 7
32	31	rabbisdv 1798	. . . . . 6
33		reseq2 3353	. . . . . 6
34	32, 33	syl 10	. . . . 5