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 28791

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 7068	. . 3
2		ifeq1 3936	. . . . . . . . 9
3	2	eqeq2d 2474	. . . . . . . 8
4	3	ralbidv 2896	. . . . . . 7
5	4	anbi2d 703	. . . . . 6 $/\$ $/\$
6	5	rexbidv 2966	. . . . 5 $/\$ $/\$
7	6	abbidv 2596	. . . 4 $/\$ $/\$
8	7	unieqd 4248	. . 3 $/\$ $/\$
9	1, 8	eqeq12d 2482	. 2 $/\$ $/\$
10		df-rdg 7066	. . 3 recs
11		df-recs 7032	. . 3 recs $/\$
12		vex 3109	. . . . . . . . . . . . 13
13	12	resex 5308	. . . . . . . . . . . 12
14		eqeq1 2464	. . . . . . . . . . . . . . 15
15		relres 5292	. . . . . . . . . . . . . . . 16
16		reldm0 5211	. . . . . . . . . . . . . . . 16
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15
18	14, 17	syl6bb 261	. . . . . . . . . . . . . 14
19		dmeq 5194	. . . . . . . . . . . . . . . 16
20		limeq 4883	. . . . . . . . . . . . . . . 16
21	19, 20	syl 16	. . . . . . . . . . . . . . 15
22		rneq 5219	. . . . . . . . . . . . . . . . 17
23		df-ima 5005	. . . . . . . . . . . . . . . . 17
24	22, 23	syl6eqr 2519	. . . . . . . . . . . . . . . 16
25	24	unieqd 4248	. . . . . . . . . . . . . . 15
26		id 22	. . . . . . . . . . . . . . . . 17
27	19	unieqd 4248	. . . . . . . . . . . . . . . . 17
28	26, 27	fveq12d 5863	. . . . . . . . . . . . . . . 16
29	28	fveq2d 5861	. . . . . . . . . . . . . . 15
30	21, 25, 29	ifbieq12d 3959	. . . . . . . . . . . . . 14
31	18, 30	ifbieq2d 3957	. . . . . . . . . . . . 13
32		eqid 2460	. . . . . . . . . . . . 13
33		vex 3109	. . . . . . . . . . . . . 14
34		imaexg 6711	. . . . . . . . . . . . . . . . 17
35	12, 34	ax-mp 5	. . . . . . . . . . . . . . . 16
36	35	uniex 6571	. . . . . . . . . . . . . . 15
37		fvex 5867	. . . . . . . . . . . . . . 15
38	36, 37	ifex 4001	. . . . . . . . . . . . . 14
39	33, 38	ifex 4001	. . . . . . . . . . . . 13
40	31, 32, 39	fvmpt 5941	. . . . . . . . . . . 12
41	13, 40	ax-mp 5	. . . . . . . . . . 11
42		dmres 5285	. . . . . . . . . . . . 13
43		onelss 4913	. . . . . . . . . . . . . . . . 17
44	43	imp 429	. . . . . . . . . . . . . . . 16 $/\$
45	44	3adant2 1010	. . . . . . . . . . . . . . 15 $/\$ $/\$
46		fndm 5671	. . . . . . . . . . . . . . . 16
47	46	3ad2ant2 1013	. . . . . . . . . . . . . . 15 $/\$ $/\$
48	45, 47	sseqtr4d 3534	. . . . . . . . . . . . . 14 $/\$ $/\$
49		df-ss 3483	. . . . . . . . . . . . . 14
50	48, 49	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$
51	42, 50	syl5eq 2513	. . . . . . . . . . . 12 $/\$ $/\$
52		eqeq1 2464	. . . . . . . . . . . . . 14
53		limeq 4883	. . . . . . . . . . . . . . 15
54		unieq 4246	. . . . . . . . . . . . . . . . 17
55	54	fveq2d 5861	. . . . . . . . . . . . . . . 16
56	55	fveq2d 5861	. . . . . . . . . . . . . . 15
57	53, 56	ifbieq2d 3957	. . . . . . . . . . . . . 14
58	52, 57	ifbieq2d 3957	. . . . . . . . . . . . 13
59		onelon 4896	. . . . . . . . . . . . . . . 16 $/\$
60		eloni 4881	. . . . . . . . . . . . . . . 16
61	59, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$
62	61	3adant2 1010	. . . . . . . . . . . . . 14 $/\$ $/\$
63		ordzsl 6651	. . . . . . . . . . . . . . 15 $\/$ $\/$
64		iftrue 3938	. . . . . . . . . . . . . . . . 17
65		iftrue 3938	. . . . . . . . . . . . . . . . 17
66	64, 65	eqtr4d 2504	. . . . . . . . . . . . . . . 16
67		vex 3109	. . . . . . . . . . . . . . . . . . . . . . 23
68	67	sucid 4950	. . . . . . . . . . . . . . . . . . . . . 22
69		fvres 5871	. . . . . . . . . . . . . . . . . . . . . 22
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
71		eloni 4881	. . . . . . . . . . . . . . . . . . . . . . 23
72		ordunisuc 6638	. . . . . . . . . . . . . . . . . . . . . . 23
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
74	73	fveq2d 5861	. . . . . . . . . . . . . . . . . . . . 21
75	73	fveq2d 5861	. . . . . . . . . . . . . . . . . . . . 21
76	70, 74, 75	3eqtr4a 2527	. . . . . . . . . . . . . . . . . . . 20
77	76	fveq2d 5861	. . . . . . . . . . . . . . . . . . 19
78		nsuceq0 4951	. . . . . . . . . . . . . . . . . . . . . 22
79		df-ne 2657	. . . . . . . . . . . . . . . . . . . . . 22
80	78, 79	mpbi 208	. . . . . . . . . . . . . . . . . . . . 21
81	80	iffalsei 3942	. . . . . . . . . . . . . . . . . . . 20
82		nlimsucg 6648	. . . . . . . . . . . . . . . . . . . . 21
83		iffalse 3941	. . . . . . . . . . . . . . . . . . . . 21
84	67, 82, 83	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
85	81, 84	eqtri 2489	. . . . . . . . . . . . . . . . . . 19
86	80	iffalsei 3942	. . . . . . . . . . . . . . . . . . . 20
87		iffalse 3941	. . . . . . . . . . . . . . . . . . . . 21
88	67, 82, 87	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
89	86, 88	eqtri 2489	. . . . . . . . . . . . . . . . . . 19
90	77, 85, 89	3eqtr4g 2526	. . . . . . . . . . . . . . . . . 18
91		eqeq1 2464	. . . . . . . . . . . . . . . . . . . 20
92		limeq 4883	. . . . . . . . . . . . . . . . . . . . 21
93		reseq2 5259	. . . . . . . . . . . . . . . . . . . . . . 23
94		unieq 4246	. . . . . . . . . . . . . . . . . . . . . . 23
95	93, 94	fveq12d 5863	. . . . . . . . . . . . . . . . . . . . . 22
96	95	fveq2d 5861	. . . . . . . . . . . . . . . . . . . . 21
97	92, 96	ifbieq2d 3957	. . . . . . . . . . . . . . . . . . . 20
98	91, 97	ifbieq2d 3957	. . . . . . . . . . . . . . . . . . 19
99	94	fveq2d 5861	. . . . . . . . . . . . . . . . . . . . . 22
100	99	fveq2d 5861	. . . . . . . . . . . . . . . . . . . . 21
101	92, 100	ifbieq2d 3957	. . . . . . . . . . . . . . . . . . . 20
102	91, 101	ifbieq2d 3957	. . . . . . . . . . . . . . . . . . 19
103	98, 102	eqeq12d 2482	. . . . . . . . . . . . . . . . . 18
104	90, 103	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17
105	104	rexlimiv 2942	. . . . . . . . . . . . . . . 16
106		iftrue 3938	. . . . . . . . . . . . . . . . . 18
107		df-lim 4876	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
108	107	simp2bi 1007	. . . . . . . . . . . . . . . . . . . 20
109	108	neneqd 2662	. . . . . . . . . . . . . . . . . . 19
110		iffalse 3941	. . . . . . . . . . . . . . . . . . 19
111	109, 110	syl 16	. . . . . . . . . . . . . . . . . 18
112		iftrue 3938	. . . . . . . . . . . . . . . . . 18
113	106, 111, 112	3eqtr4d 2511	. . . . . . . . . . . . . . . . 17
114		iffalse 3941	. . . . . . . . . . . . . . . . . 18
115	109, 114	syl 16	. . . . . . . . . . . . . . . . 17
116	113, 115	eqtr4d 2504	. . . . . . . . . . . . . . . 16
117	66, 105, 116	3jaoi 1286	. . . . . . . . . . . . . . 15 $\/$ $\/$
118	63, 117	sylbi 195	. . . . . . . . . . . . . 14
119	62, 118	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
120	58, 119	sylan9eqr 2523	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
121	51, 120	mpdan 668	. . . . . . . . . . 11 $/\$ $/\$
122	41, 121	syl5eq 2513	. . . . . . . . . 10 $/\$ $/\$
123	122	eqeq2d 2474	. . . . . . . . 9 $/\$ $/\$
124	123	3expa 1191	. . . . . . . 8 $/\$ $/\$
125	124	ralbidva 2893	. . . . . . 7 $/\$
126	125	pm5.32da 641	. . . . . 6 $/\$ $/\$
127	126	rexbiia 2957	. . . . 5 $/\$ $/\$
128	127	abbii 2594	. . . 4 $/\$ $/\$
129	128	unieqi 4247	. . 3 $/\$ $/\$
130	10, 11, 129	3eqtri 2493	. 2 $/\$
131	9, 130	vtoclg 3164	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $\/$ w3o 967 $/\$ w3a 968

wceq 1374

wcel 1762

cab 2445

wne 2655

wral 2807

wrex 2808

cvv 3106

cin 3468

wss 3469

c0 3778

cif 3932

cuni 4238

cmpt 4498

word 4870

con0 4871

wlim 4872

csuc 4873

cdm 4992

crn 4993

cres 4994

cima 4995

wrel 4997

wfn 5574

cfv 5579 recscrecs 7031

crdg 7065

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-8 1764 ax-9 1766 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1961 ax-ext 2438 ax-sep 4561 ax-nul 4569 ax-pr 4679 ax-un 6567

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 969 df-3an 970 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-eu 2272 df-mo 2273 df-clab 2446 df-cleq 2452 df-clel 2455 df-nfc 2610 df-ne 2657 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3108 df-sbc 3325 df-dif 3472 df-un 3474 df-in 3476 df-ss 3483 df-pss 3485 df-nul 3779 df-if 3933 df-pw 4005 df-sn 4021 df-pr 4023 df-tp 4025 df-op 4027 df-uni 4239 df-br 4441 df-opab 4499 df-mpt 4500 df-tr 4534 df-eprel 4784 df-id 4788 df-po 4793 df-so 4794 df-fr 4831 df-we 4833 df-ord 4874 df-on 4875 df-lim 4876 df-suc 4877 df-xp 4998 df-rel 4999 df-cnv 5000 df-co 5001 df-dm 5002 df-rn 5003 df-res 5004 df-ima 5005 df-iota 5542 df-fun 5581 df-fn 5582 df-fv 5587 df-recs 7032 df-rdg 7066

This theorem is referenced by: dfrdg3 28792

W3C validator