dfrdg2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem dfrdg2 3933

Description: Alternate definition of a recursive definition generator. (This was the original definition, but it was later replaced with the slightly shorter df-rdg 3932.)

**Assertion**
Ref	Expression
dfrdg2	$/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$

Distinct variable groups:

**Proof of Theorem dfrdg2**
Step	Hyp	Ref	Expression
1		df-rdg 3932	. 2 $/\$
2		eqif 2377	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$
3	2	anbi2i 480	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $/\$
4		orcom 246	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
5	4	anbi2i 480	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
6		andi 604	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
7		ioran 306	. . . . . . . . . . . . . . . . 17 $\/$ $/\$
8	7	anbi1i 481	. . . . . . . . . . . . . . . 16 $\/$ $/\$ $/\$ $/\$
9		anass 439	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
10	8, 9	bitr 173	. . . . . . . . . . . . . . 15 $\/$ $/\$ $/\$ $/\$
11		dmeq 3311	. . . . . . . . . . . . . . . . . . . . 21
12		dm0 3323	. . . . . . . . . . . . . . . . . . . . 21
13	11, 12	syl6eq 1523	. . . . . . . . . . . . . . . . . . . 20
14		nlim0 3027	. . . . . . . . . . . . . . . . . . . . 21
15		limeq 2960	. . . . . . . . . . . . . . . . . . . . 21
16	14, 15	mtbiri 717	. . . . . . . . . . . . . . . . . . . 20
17	13, 16	syl 10	. . . . . . . . . . . . . . . . . . 19
18	17	con2i 97	. . . . . . . . . . . . . . . . . 18
19	18	pm4.71ri 638	. . . . . . . . . . . . . . . . 17 $/\$
20	19	anbi1i 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
21		anass 439	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
22	20, 21	bitr 173	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
23	10, 22	orbi12i 257	. . . . . . . . . . . . . 14 $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
24	6, 23	bitr4 176	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
25	3, 5, 24	3bitr 177	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $\/$ $/\$
26	25	orbi2i 255	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
27		eqif 2377	. . . . . . . . . . 11 $/\$ $\/$ $/\$
28		3orass 778	. . . . . . . . . . 11 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
29	26, 27, 28	3bitr4 183	. . . . . . . . . 10 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
30	29	opabbii 2671	. . . . . . . . 9 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
31	30	fveq1i 3725	. . . . . . . 8 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
32	31	eqeq2i 1485	. . . . . . 7 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
33	32	ralbii 1667	. . . . . 6 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$