seqzfval - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem seqzfval 6477

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 4078	. . . . . . 7 $/\$
3	1, 2	mpan2 695	. . . . . 6
4		op1stg 4077	. . . . . . . 8
5	4	opreq2d 3967	. . . . . . 7
6	5	opreq2d 3967	. . . . . 6
7	3, 6	opreq12d 3969	. . . . 5
8	4	opreq1d 3966	. . . . 5
9	7, 8	opreq12d 3969	. . . 4
10		reseq1 3360	. . . 4
11	9, 10	syl 10	. . 3
12	4	breq1d 2624	. . . . 5
13	12	rabbisdv 1803	. . . 4
14		reseq2 3361	. . . 4
15	13, 14	syl 10	. . 3
16	11, 15	eqtrd 1504	. 2
17		opex 2777	. . 3
18		seq0val.2	. . 3
19		oprex 3974	. . . . 5
20		resexg 3386	. . . . 5
21	19, 20	ax-mp 7	. . . 4
22		fveq2 3715	. . . . . . . 8
23		fveq2 3715	. . . . . . . . . 10
24	23	opreq2d 3967	. . . . . . . . 9
25	24	opreq2d 3967	. . . . . . . 8
26	22, 25	opreq12d 3969	. . . . . . 7
27	23	opreq1d 3966	. . . . . . 7
28	26, 27	opreq12d 3969	. . . . . 6
29		reseq1 3360	. . . . . 6
30	28, 29	syl 10	. . . . 5
31	23	breq1d 2624	. . . . . . 7
32	31	rabbisdv 1803	. . . . . 6
33		reseq2 3361	. . . . . 6
34	32, 33	syl 10	. . . . 5