dfrdg2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem dfrdg2 3939

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

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

Distinct variable groups:

**Proof of Theorem dfrdg2**
Step	Hyp	Ref	Expression
1		df-rdg 3938	. 2 $/\$
2		eqif 2381	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$
3	2	anbi2i 482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $/\$
4		orcom 246	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
5	4	anbi2i 482	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
6		andi 606	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
7		ioran 306	. . . . . . . . . . . . . . . . 17 $\/$ $/\$
8	7	anbi1i 483	. . . . . . . . . . . . . . . 16 $\/$ $/\$ $/\$ $/\$
9		anass 441	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
10	8, 9	bitr 173	. . . . . . . . . . . . . . 15 $\/$ $/\$ $/\$ $/\$
11		dmeq 3317	. . . . . . . . . . . . . . . . . . . . 21
12		dm0 3329	. . . . . . . . . . . . . . . . . . . . 21
13	11, 12	syl6eq 1526	. . . . . . . . . . . . . . . . . . . 20
14		nlim0 3033	. . . . . . . . . . . . . . . . . . . . 21
15		limeq 2966	. . . . . . . . . . . . . . . . . . . . 21
16	14, 15	mtbiri 719	. . . . . . . . . . . . . . . . . . . 20
17	13, 16	syl 10	. . . . . . . . . . . . . . . . . . 19
18	17	con2i 97	. . . . . . . . . . . . . . . . . 18
19	18	pm4.71ri 640	. . . . . . . . . . . . . . . . 17 $/\$
20	19	anbi1i 483	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
21		anass 441	. . . . . . . . . . . . . . . 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 2381	. . . . . . . . . . 11 $/\$ $\/$ $/\$
28		3orass 780	. . . . . . . . . . 11 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
29	26, 27, 28	3bitr4 183	. . . . . . . . . 10 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
30	29	opabbii 2676	. . . . . . . . 9 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
31	30	fveq1i 3731	. . . . . . . 8 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
32	31	eqeq2i 1488	. . . . . . 7 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
33	32	ralbii 1670	. . . . . 6 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$