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 30449

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 7141	. . 3
2		ifeq1 3915	. . . . . . . . 9
3	2	eqeq2d 2436	. . . . . . . 8
4	3	ralbidv 2861	. . . . . . 7
5	4	anbi2d 708	. . . . . 6 $/\$ $/\$
6	5	rexbidv 2936	. . . . 5 $/\$ $/\$
7	6	abbidv 2553	. . . 4 $/\$ $/\$
8	7	unieqd 4229	. . 3 $/\$ $/\$
9	1, 8	eqeq12d 2444	. 2 $/\$ $/\$
10		df-rdg 7139	. . 3 recs
11		dfrecs3 7102	. . 3 recs $/\$
12		vex 3083	. . . . . . . . . . . . 13
13	12	resex 5167	. . . . . . . . . . . 12
14		eqeq1 2426	. . . . . . . . . . . . . . 15
15		relres 5151	. . . . . . . . . . . . . . . 16
16		reldm0 5071	. . . . . . . . . . . . . . . 16
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15
18	14, 17	syl6bb 264	. . . . . . . . . . . . . 14
19		dmeq 5054	. . . . . . . . . . . . . . . 16
20		limeq 5454	. . . . . . . . . . . . . . . 16
21	19, 20	syl 17	. . . . . . . . . . . . . . 15
22		rneq 5079	. . . . . . . . . . . . . . . . 17
23		df-ima 4866	. . . . . . . . . . . . . . . . 17
24	22, 23	syl6eqr 2481	. . . . . . . . . . . . . . . 16
25	24	unieqd 4229	. . . . . . . . . . . . . . 15
26		id 22	. . . . . . . . . . . . . . . . 17
27	19	unieqd 4229	. . . . . . . . . . . . . . . . 17
28	26, 27	fveq12d 5887	. . . . . . . . . . . . . . . 16
29	28	fveq2d 5885	. . . . . . . . . . . . . . 15
30	21, 25, 29	ifbieq12d 3938	. . . . . . . . . . . . . 14
31	18, 30	ifbieq2d 3936	. . . . . . . . . . . . 13
32		eqid 2422	. . . . . . . . . . . . 13
33		vex 3083	. . . . . . . . . . . . . 14
34		imaexg 6744	. . . . . . . . . . . . . . . . 17
35	12, 34	ax-mp 5	. . . . . . . . . . . . . . . 16
36	35	uniex 6601	. . . . . . . . . . . . . . 15
37		fvex 5891	. . . . . . . . . . . . . . 15
38	36, 37	ifex 3979	. . . . . . . . . . . . . 14
39	33, 38	ifex 3979	. . . . . . . . . . . . 13
40	31, 32, 39	fvmpt 5964	. . . . . . . . . . . 12
41	13, 40	ax-mp 5	. . . . . . . . . . 11
42		dmres 5144	. . . . . . . . . . . . 13
43		onelss 5484	. . . . . . . . . . . . . . . . 17
44	43	imp 430	. . . . . . . . . . . . . . . 16 $/\$
45	44	3adant2 1024	. . . . . . . . . . . . . . 15 $/\$ $/\$
46		fndm 5693	. . . . . . . . . . . . . . . 16
47	46	3ad2ant2 1027	. . . . . . . . . . . . . . 15 $/\$ $/\$
48	45, 47	sseqtr4d 3501	. . . . . . . . . . . . . 14 $/\$ $/\$
49		df-ss 3450	. . . . . . . . . . . . . 14
50	48, 49	sylib 199	. . . . . . . . . . . . 13 $/\$ $/\$
51	42, 50	syl5eq 2475	. . . . . . . . . . . 12 $/\$ $/\$
52		eqeq1 2426	. . . . . . . . . . . . . 14
53		limeq 5454	. . . . . . . . . . . . . . 15
54		unieq 4227	. . . . . . . . . . . . . . . . 17
55	54	fveq2d 5885	. . . . . . . . . . . . . . . 16
56	55	fveq2d 5885	. . . . . . . . . . . . . . 15
57	53, 56	ifbieq2d 3936	. . . . . . . . . . . . . 14
58	52, 57	ifbieq2d 3936	. . . . . . . . . . . . 13
59		onelon 5467	. . . . . . . . . . . . . . . 16 $/\$
60		eloni 5452	. . . . . . . . . . . . . . . 16
61	59, 60	syl 17	. . . . . . . . . . . . . . 15 $/\$
62	61	3adant2 1024	. . . . . . . . . . . . . 14 $/\$ $/\$
63		ordzsl 6686	. . . . . . . . . . . . . . 15 $\/$ $\/$
64		iftrue 3917	. . . . . . . . . . . . . . . . 17
65		iftrue 3917	. . . . . . . . . . . . . . . . 17
66	64, 65	eqtr4d 2466	. . . . . . . . . . . . . . . 16
67		vex 3083	. . . . . . . . . . . . . . . . . . . . . . 23
68	67	sucid 5521	. . . . . . . . . . . . . . . . . . . . . 22
69		fvres 5895	. . . . . . . . . . . . . . . . . . . . . 22
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
71		eloni 5452	. . . . . . . . . . . . . . . . . . . . . . 23
72		ordunisuc 6673	. . . . . . . . . . . . . . . . . . . . . . 23
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
74	73	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . 21
75	73	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . 21
76	70, 74, 75	3eqtr4a 2489	. . . . . . . . . . . . . . . . . . . 20
77	76	fveq2d 5885	. . . . . . . . . . . . . . . . . . 19
78		nsuceq0 5522	. . . . . . . . . . . . . . . . . . . . . 22
79	78	neii 2618	. . . . . . . . . . . . . . . . . . . . 21
80	79	iffalsei 3921	. . . . . . . . . . . . . . . . . . . 20
81		nlimsucg 6683	. . . . . . . . . . . . . . . . . . . . 21
82		iffalse 3920	. . . . . . . . . . . . . . . . . . . . 21
83	67, 81, 82	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
84	80, 83	eqtri 2451	. . . . . . . . . . . . . . . . . . 19
85	79	iffalsei 3921	. . . . . . . . . . . . . . . . . . . 20
86		iffalse 3920	. . . . . . . . . . . . . . . . . . . . 21
87	67, 81, 86	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
88	85, 87	eqtri 2451	. . . . . . . . . . . . . . . . . . 19
89	77, 84, 88	3eqtr4g 2488	. . . . . . . . . . . . . . . . . 18
90		eqeq1 2426	. . . . . . . . . . . . . . . . . . . 20
91		limeq 5454	. . . . . . . . . . . . . . . . . . . . 21
92		reseq2 5119	. . . . . . . . . . . . . . . . . . . . . . 23
93		unieq 4227	. . . . . . . . . . . . . . . . . . . . . . 23
94	92, 93	fveq12d 5887	. . . . . . . . . . . . . . . . . . . . . 22
95	94	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . 21
96	91, 95	ifbieq2d 3936	. . . . . . . . . . . . . . . . . . . 20
97	90, 96	ifbieq2d 3936	. . . . . . . . . . . . . . . . . . 19
98	93	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . 22
99	98	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . 21
100	91, 99	ifbieq2d 3936	. . . . . . . . . . . . . . . . . . . 20
101	90, 100	ifbieq2d 3936	. . . . . . . . . . . . . . . . . . 19
102	97, 101	eqeq12d 2444	. . . . . . . . . . . . . . . . . 18
103	89, 102	syl5ibrcom 225	. . . . . . . . . . . . . . . . 17
104	103	rexlimiv 2908	. . . . . . . . . . . . . . . 16
105		iftrue 3917	. . . . . . . . . . . . . . . . . 18
106		df-lim 5447	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	simp2bi 1021	. . . . . . . . . . . . . . . . . . . 20
108	107	neneqd 2621	. . . . . . . . . . . . . . . . . . 19
109	108	iffalsed 3922	. . . . . . . . . . . . . . . . . 18
110		iftrue 3917	. . . . . . . . . . . . . . . . . 18
111	105, 109, 110	3eqtr4d 2473	. . . . . . . . . . . . . . . . 17
112	108	iffalsed 3922	. . . . . . . . . . . . . . . . 17
113	111, 112	eqtr4d 2466	. . . . . . . . . . . . . . . 16
114	66, 104, 113	3jaoi 1327	. . . . . . . . . . . . . . 15 $\/$ $\/$
115	63, 114	sylbi 198	. . . . . . . . . . . . . 14
116	62, 115	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
117	58, 116	sylan9eqr 2485	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	51, 117	mpdan 672	. . . . . . . . . . 11 $/\$ $/\$
119	41, 118	syl5eq 2475	. . . . . . . . . 10 $/\$ $/\$
120	119	eqeq2d 2436	. . . . . . . . 9 $/\$ $/\$
121	120	3expa 1205	. . . . . . . 8 $/\$ $/\$
122	121	ralbidva 2858	. . . . . . 7 $/\$
123	122	pm5.32da 645	. . . . . 6 $/\$ $/\$
124	123	rexbiia 2923	. . . . 5 $/\$ $/\$
125	124	abbii 2551	. . . 4 $/\$ $/\$
126	125	unieqi 4228	. . 3 $/\$ $/\$
127	10, 11, 126	3eqtri 2455	. 2 $/\$
128	9, 127	vtoclg 3139	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $\/$ w3o 981 $/\$ w3a 982

wceq 1437

wcel 1872

cab 2407

wne 2614

wral 2771

wrex 2772

cvv 3080

cin 3435

wss 3436

c0 3761

cif 3911

cuni 4219

cmpt 4482

cdm 4853

crn 4854

cres 4855

cima 4856

wrel 4858

word 5441

con0 5442

wlim 5443

csuc 5444

wfn 5596

cfv 5601 recscrecs 7100

crdg 7138

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-sep 4546 ax-nul 4555 ax-pr 4660 ax-un 6597

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-ral 2776 df-rex 2777 df-rab 2780 df-v 3082 df-sbc 3300 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-pss 3452 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-tp 4003 df-op 4005 df-uni 4220 df-br 4424 df-opab 4483 df-mpt 4484 df-tr 4519 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-fv 5609 df-wrecs 7039 df-recs 7101 df-rdg 7139

This theorem is referenced by: dfrdg3 30450

W3C validator