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 29393

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 6996	. . 3
2		ifeq1 3861	. . . . . . . . 9
3	2	eqeq2d 2396	. . . . . . . 8
4	3	ralbidv 2821	. . . . . . 7
5	4	anbi2d 701	. . . . . 6 $/\$ $/\$
6	5	rexbidv 2893	. . . . 5 $/\$ $/\$
7	6	abbidv 2518	. . . 4 $/\$ $/\$
8	7	unieqd 4173	. . 3 $/\$ $/\$
9	1, 8	eqeq12d 2404	. 2 $/\$ $/\$
10		df-rdg 6994	. . 3 recs
11		df-recs 6960	. . 3 recs $/\$
12		vex 3037	. . . . . . . . . . . . 13
13	12	resex 5229	. . . . . . . . . . . 12
14		eqeq1 2386	. . . . . . . . . . . . . . 15
15		relres 5213	. . . . . . . . . . . . . . . 16
16		reldm0 5133	. . . . . . . . . . . . . . . 16
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15
18	14, 17	syl6bb 261	. . . . . . . . . . . . . 14
19		dmeq 5116	. . . . . . . . . . . . . . . 16
20		limeq 4804	. . . . . . . . . . . . . . . 16
21	19, 20	syl 16	. . . . . . . . . . . . . . 15
22		rneq 5141	. . . . . . . . . . . . . . . . 17
23		df-ima 4926	. . . . . . . . . . . . . . . . 17
24	22, 23	syl6eqr 2441	. . . . . . . . . . . . . . . 16
25	24	unieqd 4173	. . . . . . . . . . . . . . 15
26		id 22	. . . . . . . . . . . . . . . . 17
27	19	unieqd 4173	. . . . . . . . . . . . . . . . 17
28	26, 27	fveq12d 5780	. . . . . . . . . . . . . . . 16
29	28	fveq2d 5778	. . . . . . . . . . . . . . 15
30	21, 25, 29	ifbieq12d 3884	. . . . . . . . . . . . . 14
31	18, 30	ifbieq2d 3882	. . . . . . . . . . . . 13
32		eqid 2382	. . . . . . . . . . . . 13
33		vex 3037	. . . . . . . . . . . . . 14
34		imaexg 6636	. . . . . . . . . . . . . . . . 17
35	12, 34	ax-mp 5	. . . . . . . . . . . . . . . 16
36	35	uniex 6495	. . . . . . . . . . . . . . 15
37		fvex 5784	. . . . . . . . . . . . . . 15
38	36, 37	ifex 3925	. . . . . . . . . . . . . 14
39	33, 38	ifex 3925	. . . . . . . . . . . . 13
40	31, 32, 39	fvmpt 5857	. . . . . . . . . . . 12
41	13, 40	ax-mp 5	. . . . . . . . . . 11
42		dmres 5206	. . . . . . . . . . . . 13
43		onelss 4834	. . . . . . . . . . . . . . . . 17
44	43	imp 427	. . . . . . . . . . . . . . . 16 $/\$
45	44	3adant2 1013	. . . . . . . . . . . . . . 15 $/\$ $/\$
46		fndm 5588	. . . . . . . . . . . . . . . 16
47	46	3ad2ant2 1016	. . . . . . . . . . . . . . 15 $/\$ $/\$
48	45, 47	sseqtr4d 3454	. . . . . . . . . . . . . 14 $/\$ $/\$
49		df-ss 3403	. . . . . . . . . . . . . 14
50	48, 49	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$
51	42, 50	syl5eq 2435	. . . . . . . . . . . 12 $/\$ $/\$
52		eqeq1 2386	. . . . . . . . . . . . . 14
53		limeq 4804	. . . . . . . . . . . . . . 15
54		unieq 4171	. . . . . . . . . . . . . . . . 17
55	54	fveq2d 5778	. . . . . . . . . . . . . . . 16
56	55	fveq2d 5778	. . . . . . . . . . . . . . 15
57	53, 56	ifbieq2d 3882	. . . . . . . . . . . . . 14
58	52, 57	ifbieq2d 3882	. . . . . . . . . . . . 13
59		onelon 4817	. . . . . . . . . . . . . . . 16 $/\$
60		eloni 4802	. . . . . . . . . . . . . . . 16
61	59, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$
62	61	3adant2 1013	. . . . . . . . . . . . . 14 $/\$ $/\$
63		ordzsl 6579	. . . . . . . . . . . . . . 15 $\/$ $\/$
64		iftrue 3863	. . . . . . . . . . . . . . . . 17
65		iftrue 3863	. . . . . . . . . . . . . . . . 17
66	64, 65	eqtr4d 2426	. . . . . . . . . . . . . . . 16
67		vex 3037	. . . . . . . . . . . . . . . . . . . . . . 23
68	67	sucid 4871	. . . . . . . . . . . . . . . . . . . . . 22
69		fvres 5788	. . . . . . . . . . . . . . . . . . . . . 22
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
71		eloni 4802	. . . . . . . . . . . . . . . . . . . . . . 23
72		ordunisuc 6566	. . . . . . . . . . . . . . . . . . . . . . 23
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
74	73	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . 21
75	73	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . 21
76	70, 74, 75	3eqtr4a 2449	. . . . . . . . . . . . . . . . . . . 20
77	76	fveq2d 5778	. . . . . . . . . . . . . . . . . . 19
78		nsuceq0 4872	. . . . . . . . . . . . . . . . . . . . . 22
79	78	neii 2581	. . . . . . . . . . . . . . . . . . . . 21
80	79	iffalsei 3867	. . . . . . . . . . . . . . . . . . . 20
81		nlimsucg 6576	. . . . . . . . . . . . . . . . . . . . 21
82		iffalse 3866	. . . . . . . . . . . . . . . . . . . . 21
83	67, 81, 82	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
84	80, 83	eqtri 2411	. . . . . . . . . . . . . . . . . . 19
85	79	iffalsei 3867	. . . . . . . . . . . . . . . . . . . 20
86		iffalse 3866	. . . . . . . . . . . . . . . . . . . . 21
87	67, 81, 86	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
88	85, 87	eqtri 2411	. . . . . . . . . . . . . . . . . . 19
89	77, 84, 88	3eqtr4g 2448	. . . . . . . . . . . . . . . . . 18
90		eqeq1 2386	. . . . . . . . . . . . . . . . . . . 20
91		limeq 4804	. . . . . . . . . . . . . . . . . . . . 21
92		reseq2 5181	. . . . . . . . . . . . . . . . . . . . . . 23
93		unieq 4171	. . . . . . . . . . . . . . . . . . . . . . 23
94	92, 93	fveq12d 5780	. . . . . . . . . . . . . . . . . . . . . 22
95	94	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . 21
96	91, 95	ifbieq2d 3882	. . . . . . . . . . . . . . . . . . . 20
97	90, 96	ifbieq2d 3882	. . . . . . . . . . . . . . . . . . 19
98	93	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . . 22
99	98	fveq2d 5778	. . . . . . . . . . . . . . . . . . . . 21
100	91, 99	ifbieq2d 3882	. . . . . . . . . . . . . . . . . . . 20
101	90, 100	ifbieq2d 3882	. . . . . . . . . . . . . . . . . . 19
102	97, 101	eqeq12d 2404	. . . . . . . . . . . . . . . . . 18
103	89, 102	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17
104	103	rexlimiv 2868	. . . . . . . . . . . . . . . 16
105		iftrue 3863	. . . . . . . . . . . . . . . . . 18
106		df-lim 4797	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	simp2bi 1010	. . . . . . . . . . . . . . . . . . . 20
108	107	neneqd 2584	. . . . . . . . . . . . . . . . . . 19
109	108	iffalsed 3868	. . . . . . . . . . . . . . . . . 18
110		iftrue 3863	. . . . . . . . . . . . . . . . . 18
111	105, 109, 110	3eqtr4d 2433	. . . . . . . . . . . . . . . . 17
112	108	iffalsed 3868	. . . . . . . . . . . . . . . . 17
113	111, 112	eqtr4d 2426	. . . . . . . . . . . . . . . 16
114	66, 104, 113	3jaoi 1289	. . . . . . . . . . . . . . 15 $\/$ $\/$
115	63, 114	sylbi 195	. . . . . . . . . . . . . 14
116	62, 115	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
117	58, 116	sylan9eqr 2445	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	51, 117	mpdan 666	. . . . . . . . . . 11 $/\$ $/\$
119	41, 118	syl5eq 2435	. . . . . . . . . 10 $/\$ $/\$
120	119	eqeq2d 2396	. . . . . . . . 9 $/\$ $/\$
121	120	3expa 1194	. . . . . . . 8 $/\$ $/\$
122	121	ralbidva 2818	. . . . . . 7 $/\$
123	122	pm5.32da 639	. . . . . 6 $/\$ $/\$
124	123	rexbiia 2883	. . . . 5 $/\$ $/\$
125	124	abbii 2516	. . . 4 $/\$ $/\$
126	125	unieqi 4172	. . 3 $/\$ $/\$
127	10, 11, 126	3eqtri 2415	. 2 $/\$
128	9, 127	vtoclg 3092	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $\/$ w3o 970 $/\$ w3a 971

wceq 1399

wcel 1826

cab 2367

wne 2577

wral 2732

wrex 2733

cvv 3034

cin 3388

wss 3389

c0 3711

cif 3857

cuni 4163

cmpt 4425

word 4791

con0 4792

wlim 4793

csuc 4794

cdm 4913

crn 4914

cres 4915

cima 4916

wrel 4918

wfn 5491

cfv 5496 recscrecs 6959

crdg 6993

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-sep 4488 ax-nul 4496 ax-pr 4601 ax-un 6491

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-ral 2737 df-rex 2738 df-rab 2741 df-v 3036 df-sbc 3253 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-fv 5504 df-recs 6960 df-rdg 6994

This theorem is referenced by: dfrdg3 29394

W3C validator