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 27612

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 6871	. . 3
2		ifeq1 3798	. . . . . . . . 9
3	2	eqeq2d 2454	. . . . . . . 8
4	3	ralbidv 2738	. . . . . . 7
5	4	anbi2d 703	. . . . . 6 $/\$ $/\$
6	5	rexbidv 2739	. . . . 5 $/\$ $/\$
7	6	abbidv 2560	. . . 4 $/\$ $/\$
8	7	unieqd 4104	. . 3 $/\$ $/\$
9	1, 8	eqeq12d 2457	. 2 $/\$ $/\$
10		df-rdg 6869	. . 3 recs
11		df-recs 6835	. . 3 recs $/\$
12		vex 2978	. . . . . . . . . . . . 13
13	12	resex 5153	. . . . . . . . . . . 12
14		eqeq1 2449	. . . . . . . . . . . . . . 15
15		relres 5141	. . . . . . . . . . . . . . . 16
16		reldm0 5060	. . . . . . . . . . . . . . . 16
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15
18	14, 17	syl6bb 261	. . . . . . . . . . . . . 14
19		dmeq 5043	. . . . . . . . . . . . . . . 16
20		limeq 4734	. . . . . . . . . . . . . . . 16
21	19, 20	syl 16	. . . . . . . . . . . . . . 15
22		rneq 5068	. . . . . . . . . . . . . . . . 17
23		df-ima 4856	. . . . . . . . . . . . . . . . 17
24	22, 23	syl6eqr 2493	. . . . . . . . . . . . . . . 16
25	24	unieqd 4104	. . . . . . . . . . . . . . 15
26		id 22	. . . . . . . . . . . . . . . . 17
27	19	unieqd 4104	. . . . . . . . . . . . . . . . 17
28	26, 27	fveq12d 5700	. . . . . . . . . . . . . . . 16
29	28	fveq2d 5698	. . . . . . . . . . . . . . 15
30	21, 25, 29	ifbieq12d 3819	. . . . . . . . . . . . . 14
31	18, 30	ifbieq2d 3817	. . . . . . . . . . . . 13
32		eqid 2443	. . . . . . . . . . . . 13
33		vex 2978	. . . . . . . . . . . . . 14
34		imaexg 6518	. . . . . . . . . . . . . . . . 17
35	12, 34	ax-mp 5	. . . . . . . . . . . . . . . 16
36	35	uniex 6379	. . . . . . . . . . . . . . 15
37		fvex 5704	. . . . . . . . . . . . . . 15
38	36, 37	ifex 3861	. . . . . . . . . . . . . 14
39	33, 38	ifex 3861	. . . . . . . . . . . . 13
40	31, 32, 39	fvmpt 5777	. . . . . . . . . . . 12
41	13, 40	ax-mp 5	. . . . . . . . . . 11
42		dmres 5134	. . . . . . . . . . . . 13
43		onelss 4764	. . . . . . . . . . . . . . . . 17
44	43	imp 429	. . . . . . . . . . . . . . . 16 $/\$
45	44	3adant2 1007	. . . . . . . . . . . . . . 15 $/\$ $/\$
46		fndm 5513	. . . . . . . . . . . . . . . 16
47	46	3ad2ant2 1010	. . . . . . . . . . . . . . 15 $/\$ $/\$
48	45, 47	sseqtr4d 3396	. . . . . . . . . . . . . 14 $/\$ $/\$
49		df-ss 3345	. . . . . . . . . . . . . 14
50	48, 49	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$
51	42, 50	syl5eq 2487	. . . . . . . . . . . 12 $/\$ $/\$
52		eqeq1 2449	. . . . . . . . . . . . . 14
53		limeq 4734	. . . . . . . . . . . . . . 15
54		unieq 4102	. . . . . . . . . . . . . . . . 17
55	54	fveq2d 5698	. . . . . . . . . . . . . . . 16
56	55	fveq2d 5698	. . . . . . . . . . . . . . 15
57	53, 56	ifbieq2d 3817	. . . . . . . . . . . . . 14
58	52, 57	ifbieq2d 3817	. . . . . . . . . . . . 13
59		onelon 4747	. . . . . . . . . . . . . . . 16 $/\$
60		eloni 4732	. . . . . . . . . . . . . . . 16
61	59, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$
62	61	3adant2 1007	. . . . . . . . . . . . . 14 $/\$ $/\$
63		ordzsl 6459	. . . . . . . . . . . . . . 15 $\/$ $\/$
64		iftrue 3800	. . . . . . . . . . . . . . . . 17
65		iftrue 3800	. . . . . . . . . . . . . . . . 17
66	64, 65	eqtr4d 2478	. . . . . . . . . . . . . . . 16
67		vex 2978	. . . . . . . . . . . . . . . . . . . . . . 23
68	67	sucid 4801	. . . . . . . . . . . . . . . . . . . . . 22
69		fvres 5707	. . . . . . . . . . . . . . . . . . . . . 22
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
71		eloni 4732	. . . . . . . . . . . . . . . . . . . . . . 23
72		ordunisuc 6446	. . . . . . . . . . . . . . . . . . . . . . 23
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
74	73	fveq2d 5698	. . . . . . . . . . . . . . . . . . . . 21
75	73	fveq2d 5698	. . . . . . . . . . . . . . . . . . . . 21
76	70, 74, 75	3eqtr4a 2501	. . . . . . . . . . . . . . . . . . . 20
77	76	fveq2d 5698	. . . . . . . . . . . . . . . . . . 19
78		nsuceq0 4802	. . . . . . . . . . . . . . . . . . . . . 22
79		df-ne 2611	. . . . . . . . . . . . . . . . . . . . . 22
80	78, 79	mpbi 208	. . . . . . . . . . . . . . . . . . . . 21
81	80	iffalsei 3803	. . . . . . . . . . . . . . . . . . . 20
82		nlimsucg 6456	. . . . . . . . . . . . . . . . . . . . 21
83		iffalse 3802	. . . . . . . . . . . . . . . . . . . . 21
84	67, 82, 83	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
85	81, 84	eqtri 2463	. . . . . . . . . . . . . . . . . . 19
86	80	iffalsei 3803	. . . . . . . . . . . . . . . . . . . 20
87		iffalse 3802	. . . . . . . . . . . . . . . . . . . . 21
88	67, 82, 87	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
89	86, 88	eqtri 2463	. . . . . . . . . . . . . . . . . . 19
90	77, 85, 89	3eqtr4g 2500	. . . . . . . . . . . . . . . . . 18
91		eqeq1 2449	. . . . . . . . . . . . . . . . . . . 20
92		limeq 4734	. . . . . . . . . . . . . . . . . . . . 21
93		reseq2 5108	. . . . . . . . . . . . . . . . . . . . . . 23
94		unieq 4102	. . . . . . . . . . . . . . . . . . . . . . 23
95	93, 94	fveq12d 5700	. . . . . . . . . . . . . . . . . . . . . 22
96	95	fveq2d 5698	. . . . . . . . . . . . . . . . . . . . 21
97	92, 96	ifbieq2d 3817	. . . . . . . . . . . . . . . . . . . 20
98	91, 97	ifbieq2d 3817	. . . . . . . . . . . . . . . . . . 19
99	94	fveq2d 5698	. . . . . . . . . . . . . . . . . . . . . 22
100	99	fveq2d 5698	. . . . . . . . . . . . . . . . . . . . 21
101	92, 100	ifbieq2d 3817	. . . . . . . . . . . . . . . . . . . 20
102	91, 101	ifbieq2d 3817	. . . . . . . . . . . . . . . . . . 19
103	98, 102	eqeq12d 2457	. . . . . . . . . . . . . . . . . 18
104	90, 103	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17
105	104	rexlimiv 2838	. . . . . . . . . . . . . . . 16
106		iftrue 3800	. . . . . . . . . . . . . . . . . 18
107		df-lim 4727	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
108	107	simp2bi 1004	. . . . . . . . . . . . . . . . . . . 20
109	108	neneqd 2627	. . . . . . . . . . . . . . . . . . 19
110		iffalse 3802	. . . . . . . . . . . . . . . . . . 19
111	109, 110	syl 16	. . . . . . . . . . . . . . . . . 18
112		iftrue 3800	. . . . . . . . . . . . . . . . . 18
113	106, 111, 112	3eqtr4d 2485	. . . . . . . . . . . . . . . . 17
114		iffalse 3802	. . . . . . . . . . . . . . . . . 18
115	109, 114	syl 16	. . . . . . . . . . . . . . . . 17
116	113, 115	eqtr4d 2478	. . . . . . . . . . . . . . . 16
117	66, 105, 116	3jaoi 1281	. . . . . . . . . . . . . . 15 $\/$ $\/$
118	63, 117	sylbi 195	. . . . . . . . . . . . . 14
119	62, 118	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
120	58, 119	sylan9eqr 2497	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	51, 120	mpdan 668	. . . . . . . . . . 11 $/\$ $/\$
122	41, 121	syl5eq 2487	. . . . . . . . . 10 $/\$ $/\$
123	122	eqeq2d 2454	. . . . . . . . 9 $/\$ $/\$
124	123	3expa 1187	. . . . . . . 8 $/\$ $/\$
125	124	ralbidva 2734	. . . . . . 7 $/\$
126	125	pm5.32da 641	. . . . . 6 $/\$ $/\$
127	126	rexbiia 2751	. . . . 5 $/\$ $/\$
128	127	abbii 2558	. . . 4 $/\$ $/\$
129	128	unieqi 4103	. . 3 $/\$ $/\$
130	10, 11, 129	3eqtri 2467	. 2 $/\$
131	9, 130	vtoclg 3033	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 2429

wne 2609

wral 2718

wrex 2719

cvv 2975

cin 3330

wss 3331

c0 3640

cif 3794

cuni 4094

cmpt 4353

word 4721

con0 4722

wlim 4723

csuc 4724

cdm 4843

crn 4844

cres 4845

cima 4846

wrel 4848

wfn 5416

cfv 5421 recscrecs 6834

crdg 6868

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 2423 ax-sep 4416 ax-nul 4424 ax-pr 4534 ax-un 6375

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 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2571 df-ne 2611 df-ral 2723 df-rex 2724 df-rab 2727 df-v 2977 df-sbc 3190 df-dif 3334 df-un 3336 df-in 3338 df-ss 3345 df-pss 3347 df-nul 3641 df-if 3795 df-pw 3865 df-sn 3881 df-pr 3883 df-tp 3885 df-op 3887 df-uni 4095 df-br 4296 df-opab 4354 df-mpt 4355 df-tr 4389 df-eprel 4635 df-id 4639 df-po 4644 df-so 4645 df-fr 4682 df-we 4684 df-ord 4725 df-on 4726 df-lim 4727 df-suc 4728 df-xp 4849 df-rel 4850 df-cnv 4851 df-co 4852 df-dm 4853 df-rn 4854 df-res 4855 df-ima 4856 df-iota 5384 df-fun 5423 df-fn 5424 df-fv 5429 df-recs 6835 df-rdg 6869

This theorem is referenced by: dfrdg3 27613

W3C validator