dfrdg2 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dfrdg2		Structured version Unicode version

Theorem dfrdg2 27556

Description: Alternate definition of the recursive function generator when

is a set. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

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

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem dfrdg2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rdgeq2 6860	. . 3
2		ifeq1 3788	. . . . . . . . 9
3	2	eqeq2d 2448	. . . . . . . 8
4	3	ralbidv 2729	. . . . . . 7
5	4	anbi2d 703	. . . . . 6 $/\$ $/\$
6	5	rexbidv 2730	. . . . 5 $/\$ $/\$
7	6	abbidv 2551	. . . 4 $/\$ $/\$
8	7	unieqd 4094	. . 3 $/\$ $/\$
9	1, 8	eqeq12d 2451	. 2 $/\$ $/\$
10		df-rdg 6858	. . 3 recs
11		df-recs 6824	. . 3 recs $/\$
12		vex 2969	. . . . . . . . . . . . 13
13	12	resex 5143	. . . . . . . . . . . 12
14		eqeq1 2443	. . . . . . . . . . . . . . 15
15		relres 5131	. . . . . . . . . . . . . . . 16
16		reldm0 5049	. . . . . . . . . . . . . . . 16
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15
18	14, 17	syl6bb 261	. . . . . . . . . . . . . 14
19		dmeq 5032	. . . . . . . . . . . . . . . 16
20		limeq 4723	. . . . . . . . . . . . . . . 16
21	19, 20	syl 16	. . . . . . . . . . . . . . 15
22		rneq 5057	. . . . . . . . . . . . . . . . 17
23		df-ima 4845	. . . . . . . . . . . . . . . . 17
24	22, 23	syl6eqr 2487	. . . . . . . . . . . . . . . 16
25	24	unieqd 4094	. . . . . . . . . . . . . . 15
26		id 22	. . . . . . . . . . . . . . . . 17
27	19	unieqd 4094	. . . . . . . . . . . . . . . . 17
28	26, 27	fveq12d 5690	. . . . . . . . . . . . . . . 16
29	28	fveq2d 5688	. . . . . . . . . . . . . . 15
30	21, 25, 29	ifbieq12d 3809	. . . . . . . . . . . . . 14
31	18, 30	ifbieq2d 3807	. . . . . . . . . . . . 13
32		eqid 2437	. . . . . . . . . . . . 13
33		vex 2969	. . . . . . . . . . . . . 14
34		imaexg 6510	. . . . . . . . . . . . . . . . 17
35	12, 34	ax-mp 5	. . . . . . . . . . . . . . . 16
36	35	uniex 6371	. . . . . . . . . . . . . . 15
37		fvex 5694	. . . . . . . . . . . . . . 15
38	36, 37	ifex 3851	. . . . . . . . . . . . . 14
39	33, 38	ifex 3851	. . . . . . . . . . . . 13
40	31, 32, 39	fvmpt 5767	. . . . . . . . . . . 12
41	13, 40	ax-mp 5	. . . . . . . . . . 11
42		dmres 5124	. . . . . . . . . . . . 13
43		onelss 4753	. . . . . . . . . . . . . . . . 17
44	43	imp 429	. . . . . . . . . . . . . . . 16 $/\$
45	44	3adant2 1007	. . . . . . . . . . . . . . 15 $/\$ $/\$
46		fndm 5503	. . . . . . . . . . . . . . . 16
47	46	3ad2ant2 1010	. . . . . . . . . . . . . . 15 $/\$ $/\$
48	45, 47	sseqtr4d 3386	. . . . . . . . . . . . . 14 $/\$ $/\$
49		df-ss 3335	. . . . . . . . . . . . . 14
50	48, 49	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$
51	42, 50	syl5eq 2481	. . . . . . . . . . . 12 $/\$ $/\$
52		eqeq1 2443	. . . . . . . . . . . . . 14
53		limeq 4723	. . . . . . . . . . . . . . 15
54		unieq 4092	. . . . . . . . . . . . . . . . 17
55	54	fveq2d 5688	. . . . . . . . . . . . . . . 16
56	55	fveq2d 5688	. . . . . . . . . . . . . . 15
57	53, 56	ifbieq2d 3807	. . . . . . . . . . . . . 14
58	52, 57	ifbieq2d 3807	. . . . . . . . . . . . 13
59		onelon 4736	. . . . . . . . . . . . . . . 16 $/\$
60		eloni 4721	. . . . . . . . . . . . . . . 16
61	59, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$
62	61	3adant2 1007	. . . . . . . . . . . . . 14 $/\$ $/\$
63		ordzsl 6451	. . . . . . . . . . . . . . 15 $\/$ $\/$
64		iftrue 3790	. . . . . . . . . . . . . . . . 17
65		iftrue 3790	. . . . . . . . . . . . . . . . 17
66	64, 65	eqtr4d 2472	. . . . . . . . . . . . . . . 16
67		vex 2969	. . . . . . . . . . . . . . . . . . . . . . 23
68	67	sucid 4790	. . . . . . . . . . . . . . . . . . . . . 22
69		fvres 5697	. . . . . . . . . . . . . . . . . . . . . 22
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
71		eloni 4721	. . . . . . . . . . . . . . . . . . . . . . 23
72		ordunisuc 6438	. . . . . . . . . . . . . . . . . . . . . . 23
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
74	73	fveq2d 5688	. . . . . . . . . . . . . . . . . . . . 21
75	73	fveq2d 5688	. . . . . . . . . . . . . . . . . . . . 21
76	70, 74, 75	3eqtr4a 2495	. . . . . . . . . . . . . . . . . . . 20
77	76	fveq2d 5688	. . . . . . . . . . . . . . . . . . 19
78		nsuceq0 4791	. . . . . . . . . . . . . . . . . . . . . 22
79		df-ne 2602	. . . . . . . . . . . . . . . . . . . . . 22
80	78, 79	mpbi 208	. . . . . . . . . . . . . . . . . . . . 21
81	80	iffalsei 3793	. . . . . . . . . . . . . . . . . . . 20
82		nlimsucg 6448	. . . . . . . . . . . . . . . . . . . . 21
83		iffalse 3792	. . . . . . . . . . . . . . . . . . . . 21
84	67, 82, 83	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
85	81, 84	eqtri 2457	. . . . . . . . . . . . . . . . . . 19
86	80	iffalsei 3793	. . . . . . . . . . . . . . . . . . . 20
87		iffalse 3792	. . . . . . . . . . . . . . . . . . . . 21
88	67, 82, 87	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
89	86, 88	eqtri 2457	. . . . . . . . . . . . . . . . . . 19
90	77, 85, 89	3eqtr4g 2494	. . . . . . . . . . . . . . . . . 18
91		eqeq1 2443	. . . . . . . . . . . . . . . . . . . 20
92		limeq 4723	. . . . . . . . . . . . . . . . . . . . 21
93		reseq2 5097	. . . . . . . . . . . . . . . . . . . . . . 23
94		unieq 4092	. . . . . . . . . . . . . . . . . . . . . . 23
95	93, 94	fveq12d 5690	. . . . . . . . . . . . . . . . . . . . . 22
96	95	fveq2d 5688	. . . . . . . . . . . . . . . . . . . . 21
97	92, 96	ifbieq2d 3807	. . . . . . . . . . . . . . . . . . . 20
98	91, 97	ifbieq2d 3807	. . . . . . . . . . . . . . . . . . 19
99	94	fveq2d 5688	. . . . . . . . . . . . . . . . . . . . . 22
100	99	fveq2d 5688	. . . . . . . . . . . . . . . . . . . . 21
101	92, 100	ifbieq2d 3807	. . . . . . . . . . . . . . . . . . . 20
102	91, 101	ifbieq2d 3807	. . . . . . . . . . . . . . . . . . 19
103	98, 102	eqeq12d 2451	. . . . . . . . . . . . . . . . . 18
104	90, 103	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17
105	104	rexlimiv 2829	. . . . . . . . . . . . . . . 16
106		iftrue 3790	. . . . . . . . . . . . . . . . . 18
107		df-lim 4716	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
108	107	simp2bi 1004	. . . . . . . . . . . . . . . . . . . 20
109	108	neneqd 2618	. . . . . . . . . . . . . . . . . . 19
110		iffalse 3792	. . . . . . . . . . . . . . . . . . 19
111	109, 110	syl 16	. . . . . . . . . . . . . . . . . 18
112		iftrue 3790	. . . . . . . . . . . . . . . . . 18
113	106, 111, 112	3eqtr4d 2479	. . . . . . . . . . . . . . . . 17
114		iffalse 3792	. . . . . . . . . . . . . . . . . 18
115	109, 114	syl 16	. . . . . . . . . . . . . . . . 17
116	113, 115	eqtr4d 2472	. . . . . . . . . . . . . . . 16
117	66, 105, 116	3jaoi 1281	. . . . . . . . . . . . . . 15 $\/$ $\/$
118	63, 117	sylbi 195	. . . . . . . . . . . . . 14
119	62, 118	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
120	58, 119	sylan9eqr 2491	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	51, 120	mpdan 668	. . . . . . . . . . 11 $/\$ $/\$
122	41, 121	syl5eq 2481	. . . . . . . . . 10 $/\$ $/\$
123	122	eqeq2d 2448	. . . . . . . . 9 $/\$ $/\$
124	123	3expa 1187	. . . . . . . 8 $/\$ $/\$
125	124	ralbidva 2725	. . . . . . 7 $/\$
126	125	pm5.32da 641	. . . . . 6 $/\$ $/\$
127	126	rexbiia 2742	. . . . 5 $/\$ $/\$
128	127	abbii 2549	. . . 4 $/\$ $/\$
129	128	unieqi 4093	. . 3 $/\$ $/\$
130	10, 11, 129	3eqtri 2461	. 2 $/\$
131	9, 130	vtoclg 3023	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $\/$ w3o 964 $/\$ w3a 965

wceq 1369

wcel 1756

cab 2423

wne 2600

wral 2709

wrex 2710

cvv 2966

cin 3320

wss 3321

c0 3630

cif 3784

cuni 4084

cmpt 4343

word 4710

con0 4711

wlim 4712

csuc 4713

cdm 4832

crn 4833

cres 4834

cima 4835

wrel 4837

wfn 5406

cfv 5411 recscrecs 6823

crdg 6857

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2418 ax-sep 4406 ax-nul 4414 ax-pr 4524 ax-un 6367

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2424 df-cleq 2430 df-clel 2433 df-nfc 2562 df-ne 2602 df-ral 2714 df-rex 2715 df-rab 2718 df-v 2968 df-sbc 3180 df-dif 3324 df-un 3326 df-in 3328 df-ss 3335 df-pss 3337 df-nul 3631 df-if 3785 df-pw 3855 df-sn 3871 df-pr 3873 df-tp 3875 df-op 3877 df-uni 4085 df-br 4286 df-opab 4344 df-mpt 4345 df-tr 4379 df-eprel 4624 df-id 4628 df-po 4633 df-so 4634 df-fr 4671 df-we 4673 df-ord 4714 df-on 4715 df-lim 4716 df-suc 4717 df-xp 4838 df-rel 4839 df-cnv 4840 df-co 4841 df-dm 4842 df-rn 4843 df-res 4844 df-ima 4845 df-iota 5374 df-fun 5413 df-fn 5414 df-fv 5419 df-recs 6824 df-rdg 6858

This theorem is referenced by: dfrdg3 27557

W3C validator