dfrdg2 - Mathbox for Scott Fenton

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

Theorem dfrdg2 30513

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 7148	. . 3
2		ifeq1 3876	. . . . . . . . 9
3	2	eqeq2d 2481	. . . . . . . 8
4	3	ralbidv 2829	. . . . . . 7
5	4	anbi2d 718	. . . . . 6 $/\$ $/\$
6	5	rexbidv 2892	. . . . 5 $/\$ $/\$
7	6	abbidv 2589	. . . 4 $/\$ $/\$
8	7	unieqd 4200	. . 3 $/\$ $/\$
9	1, 8	eqeq12d 2486	. 2 $/\$ $/\$
10		df-rdg 7146	. . 3 recs
11		dfrecs3 7109	. . 3 recs $/\$
12		vex 3034	. . . . . . . . . . . . 13
13	12	resex 5154	. . . . . . . . . . . 12
14		eqeq1 2475	. . . . . . . . . . . . . . 15
15		relres 5138	. . . . . . . . . . . . . . . 16
16		reldm0 5058	. . . . . . . . . . . . . . . 16
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15
18	14, 17	syl6bb 269	. . . . . . . . . . . . . 14
19		dmeq 5040	. . . . . . . . . . . . . . . 16
20		limeq 5442	. . . . . . . . . . . . . . . 16
21	19, 20	syl 17	. . . . . . . . . . . . . . 15
22		rneq 5066	. . . . . . . . . . . . . . . . 17
23		df-ima 4852	. . . . . . . . . . . . . . . . 17
24	22, 23	syl6eqr 2523	. . . . . . . . . . . . . . . 16
25	24	unieqd 4200	. . . . . . . . . . . . . . 15
26		id 22	. . . . . . . . . . . . . . . . 17
27	19	unieqd 4200	. . . . . . . . . . . . . . . . 17
28	26, 27	fveq12d 5885	. . . . . . . . . . . . . . . 16
29	28	fveq2d 5883	. . . . . . . . . . . . . . 15
30	21, 25, 29	ifbieq12d 3899	. . . . . . . . . . . . . 14
31	18, 30	ifbieq2d 3897	. . . . . . . . . . . . 13
32		eqid 2471	. . . . . . . . . . . . 13
33		vex 3034	. . . . . . . . . . . . . 14
34		imaexg 6749	. . . . . . . . . . . . . . . . 17
35	12, 34	ax-mp 5	. . . . . . . . . . . . . . . 16
36	35	uniex 6606	. . . . . . . . . . . . . . 15
37		fvex 5889	. . . . . . . . . . . . . . 15
38	36, 37	ifex 3940	. . . . . . . . . . . . . 14
39	33, 38	ifex 3940	. . . . . . . . . . . . 13
40	31, 32, 39	fvmpt 5963	. . . . . . . . . . . 12
41	13, 40	ax-mp 5	. . . . . . . . . . 11
42		dmres 5131	. . . . . . . . . . . . 13
43		onelss 5472	. . . . . . . . . . . . . . . . 17
44	43	imp 436	. . . . . . . . . . . . . . . 16 $/\$
45	44	3adant2 1049	. . . . . . . . . . . . . . 15 $/\$ $/\$
46		fndm 5685	. . . . . . . . . . . . . . . 16
47	46	3ad2ant2 1052	. . . . . . . . . . . . . . 15 $/\$ $/\$
48	45, 47	sseqtr4d 3455	. . . . . . . . . . . . . 14 $/\$ $/\$
49		df-ss 3404	. . . . . . . . . . . . . 14
50	48, 49	sylib 201	. . . . . . . . . . . . 13 $/\$ $/\$
51	42, 50	syl5eq 2517	. . . . . . . . . . . 12 $/\$ $/\$
52		eqeq1 2475	. . . . . . . . . . . . . 14
53		limeq 5442	. . . . . . . . . . . . . . 15
54		unieq 4198	. . . . . . . . . . . . . . . . 17
55	54	fveq2d 5883	. . . . . . . . . . . . . . . 16
56	55	fveq2d 5883	. . . . . . . . . . . . . . 15
57	53, 56	ifbieq2d 3897	. . . . . . . . . . . . . 14
58	52, 57	ifbieq2d 3897	. . . . . . . . . . . . 13
59		onelon 5455	. . . . . . . . . . . . . . . 16 $/\$
60		eloni 5440	. . . . . . . . . . . . . . . 16
61	59, 60	syl 17	. . . . . . . . . . . . . . 15 $/\$
62	61	3adant2 1049	. . . . . . . . . . . . . 14 $/\$ $/\$
63		ordzsl 6691	. . . . . . . . . . . . . . 15 $\/$ $\/$
64		iftrue 3878	. . . . . . . . . . . . . . . . 17
65		iftrue 3878	. . . . . . . . . . . . . . . . 17
66	64, 65	eqtr4d 2508	. . . . . . . . . . . . . . . 16
67		vex 3034	. . . . . . . . . . . . . . . . . . . . . . 23
68	67	sucid 5509	. . . . . . . . . . . . . . . . . . . . . 22
69		fvres 5893	. . . . . . . . . . . . . . . . . . . . . 22
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
71		eloni 5440	. . . . . . . . . . . . . . . . . . . . . . 23
72		ordunisuc 6678	. . . . . . . . . . . . . . . . . . . . . . 23
73	71, 72	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
74	73	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
75	73	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
76	70, 74, 75	3eqtr4a 2531	. . . . . . . . . . . . . . . . . . . 20
77	76	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19
78		nsuceq0 5510	. . . . . . . . . . . . . . . . . . . . . 22
79	78	neii 2645	. . . . . . . . . . . . . . . . . . . . 21
80	79	iffalsei 3882	. . . . . . . . . . . . . . . . . . . 20
81		nlimsucg 6688	. . . . . . . . . . . . . . . . . . . . 21
82		iffalse 3881	. . . . . . . . . . . . . . . . . . . . 21
83	67, 81, 82	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
84	80, 83	eqtri 2493	. . . . . . . . . . . . . . . . . . 19
85	79	iffalsei 3882	. . . . . . . . . . . . . . . . . . . 20
86		iffalse 3881	. . . . . . . . . . . . . . . . . . . . 21
87	67, 81, 86	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
88	85, 87	eqtri 2493	. . . . . . . . . . . . . . . . . . 19
89	77, 84, 88	3eqtr4g 2530	. . . . . . . . . . . . . . . . . 18
90		eqeq1 2475	. . . . . . . . . . . . . . . . . . . 20
91		limeq 5442	. . . . . . . . . . . . . . . . . . . . 21
92		reseq2 5106	. . . . . . . . . . . . . . . . . . . . . . 23
93		unieq 4198	. . . . . . . . . . . . . . . . . . . . . . 23
94	92, 93	fveq12d 5885	. . . . . . . . . . . . . . . . . . . . . 22
95	94	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
96	91, 95	ifbieq2d 3897	. . . . . . . . . . . . . . . . . . . 20
97	90, 96	ifbieq2d 3897	. . . . . . . . . . . . . . . . . . 19
98	93	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22
99	98	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . 21
100	91, 99	ifbieq2d 3897	. . . . . . . . . . . . . . . . . . . 20
101	90, 100	ifbieq2d 3897	. . . . . . . . . . . . . . . . . . 19
102	97, 101	eqeq12d 2486	. . . . . . . . . . . . . . . . . 18
103	89, 102	syl5ibrcom 230	. . . . . . . . . . . . . . . . 17
104	103	rexlimiv 2867	. . . . . . . . . . . . . . . 16
105		iftrue 3878	. . . . . . . . . . . . . . . . . 18
106		df-lim 5435	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	simp2bi 1046	. . . . . . . . . . . . . . . . . . . 20
108	107	neneqd 2648	. . . . . . . . . . . . . . . . . . 19
109	108	iffalsed 3883	. . . . . . . . . . . . . . . . . 18
110		iftrue 3878	. . . . . . . . . . . . . . . . . 18
111	105, 109, 110	3eqtr4d 2515	. . . . . . . . . . . . . . . . 17
112	108	iffalsed 3883	. . . . . . . . . . . . . . . . 17
113	111, 112	eqtr4d 2508	. . . . . . . . . . . . . . . 16
114	66, 104, 113	3jaoi 1357	. . . . . . . . . . . . . . 15 $\/$ $\/$
115	63, 114	sylbi 200	. . . . . . . . . . . . . 14
116	62, 115	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$
117	58, 116	sylan9eqr 2527	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	51, 117	mpdan 681	. . . . . . . . . . 11 $/\$ $/\$
119	41, 118	syl5eq 2517	. . . . . . . . . 10 $/\$ $/\$
120	119	eqeq2d 2481	. . . . . . . . 9 $/\$ $/\$
121	120	3expa 1231	. . . . . . . 8 $/\$ $/\$
122	121	ralbidva 2828	. . . . . . 7 $/\$
123	122	pm5.32da 653	. . . . . 6 $/\$ $/\$
124	123	rexbiia 2880	. . . . 5 $/\$ $/\$
125	124	abbii 2587	. . . 4 $/\$ $/\$
126	125	unieqi 4199	. . 3 $/\$ $/\$
127	10, 11, 126	3eqtri 2497	. 2 $/\$
128	9, 127	vtoclg 3093	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $\/$ w3o 1006 $/\$ w3a 1007

wceq 1452

wcel 1904

cab 2457

wne 2641

wral 2756

wrex 2757

cvv 3031

cin 3389

wss 3390

c0 3722

cif 3872

cuni 4190

cmpt 4454

cdm 4839

crn 4840

cres 4841

cima 4842

wrel 4844

word 5429

con0 5430

wlim 5431

csuc 5432

wfn 5584

cfv 5589 recscrecs 7107

crdg 7145

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pr 4639 ax-un 6602

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-sbc 3256 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-pss 3406 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-tp 3964 df-op 3966 df-uni 4191 df-br 4396 df-opab 4455 df-mpt 4456 df-tr 4491 df-eprel 4750 df-id 4754 df-po 4760 df-so 4761 df-fr 4798 df-we 4800 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-pred 5387 df-ord 5433 df-on 5434 df-lim 5435 df-suc 5436 df-iota 5553 df-fun 5591 df-fn 5592 df-fv 5597 df-wrecs 7046 df-recs 7108 df-rdg 7146

This theorem is referenced by: dfrdg3 30514

W3C validator