dfrdg2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem dfrdg2 4234

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

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

Distinct variable groups:

**Proof of Theorem dfrdg2**
Step	Hyp	Ref	Expression
1		df-rdg 4233	. 2 $/\$
2		eqif 2431	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$
3	2	anbi2i 483	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\/$ $/\$
4		orcom 244	. . . . . . . . . . . . . 14 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
5	4	anbi2i 483	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$
6		andi 607	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
7		ioran 304	. . . . . . . . . . . . . . . . 17 $\/$ $/\$
8	7	anbi1i 484	. . . . . . . . . . . . . . . 16 $\/$ $/\$ $/\$ $/\$
9		anass 441	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
10	8, 9	bitri 171	. . . . . . . . . . . . . . 15 $\/$ $/\$ $/\$ $/\$
11		dmeq 3402	. . . . . . . . . . . . . . . . . . . . 21
12		dm0 3414	. . . . . . . . . . . . . . . . . . . . 21
13	11, 12	syl6eq 1566	. . . . . . . . . . . . . . . . . . . 20
14		nlim0 3031	. . . . . . . . . . . . . . . . . . . . 21
15		limeq 2987	. . . . . . . . . . . . . . . . . . . . 21
16	14, 15	mtbiri 722	. . . . . . . . . . . . . . . . . . . 20
17	13, 16	syl 10	. . . . . . . . . . . . . . . . . . 19
18	17	con2i 97	. . . . . . . . . . . . . . . . . 18
19	18	pm4.71ri 641	. . . . . . . . . . . . . . . . 17 $/\$
20	19	anbi1i 484	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
21		anass 441	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$
22	20, 21	bitri 171	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
23	10, 22	orbi12i 255	. . . . . . . . . . . . . 14 $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$
24	6, 23	bitr4i 174	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
25	3, 5, 24	3bitri 175	. . . . . . . . . . . 12 $/\$ $\/$ $/\$ $\/$ $/\$
26	25	orbi2i 253	. . . . . . . . . . 11 $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
27		eqif 2431	. . . . . . . . . . 11 $/\$ $\/$ $/\$
28		3orass 784	. . . . . . . . . . 11 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
29	26, 27, 28	3bitr4i 181	. . . . . . . . . 10 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
30	29	opabbii 2745	. . . . . . . . 9 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
31	30	fveq1i 3836	. . . . . . . 8 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
32	31	eqeq2i 1528	. . . . . . 7 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
33	32	ralbii 1713	. . . . . 6 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
34	33	anbi2i 483	. . . . 5 $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
35	34	rexbii 1714	. . . 4 $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
36	35	abbii 1618	. . 3 $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
37	36	unieqi 2577	. 2 $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
38	1, 37	eqtri 1538	1 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 2 $\/$ wo 220 $/\$ wa 221 $\/$ w3o 780

wceq 992

cab 1505

wral 1691

wrex 1692

c0 2332

cif 2415

cuni 2569

copab 2740

con0 2975

wlim 2976

cdm 3251

crn 3252

cres 3253

wfn 3258

cfv 3263

crdg 4232

This theorem is referenced by: rdgval 4241

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 998 ax-gen 999 ax-8 1000 ax-10 1002 ax-11 1003 ax-12 1004 ax-13 1005 ax-14 1006 ax-17 1007 ax-4 1009 ax-5o 1011 ax-6o 1014 ax-9o 1159 ax-10o 1177 ax-16 1247 ax-11o 1255 ax-ext 1500 ax-sep 2777 ax-pow 2818 ax-pr 2855

This theorem depends on definitions: df-bi 145 df-or 222 df-an 223 df-3or 782 df-3an 783 df-ex 1017 df-sb 1209 df-eu 1421 df-mo 1422 df-clab 1506 df-cleq 1511 df-clel 1514 df-ne 1630 df-ral 1695 df-rex 1696 df-v 1858 df-dif 2101 df-un 2102 df-in 2103 df-ss 2105 df-nul 2333 df-if 2416 df-pw 2459 df-sn 2470 df-pr 2471 df-op 2474 df-uni 2570 df-br 2693 df-opab 2741 df-tr 2755 df-po 2918 df-so 2929 df-fr 2947 df-we 2962 df-ord 2978 df-lim 2980 df-cnv 3267 df-dm 3269 df-rn 3270 df-res 3271 df-ima 3272 df-fv 3279 df-rdg 4233