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 29203

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 7080	. . 3
2		ifeq1 3930	. . . . . . . . 9
3	2	eqeq2d 2457	. . . . . . . 8
4	3	ralbidv 2882	. . . . . . 7
5	4	anbi2d 703	. . . . . 6 $/\$ $/\$
6	5	rexbidv 2954	. . . . 5 $/\$ $/\$
7	6	abbidv 2579	. . . 4 $/\$ $/\$
8	7	unieqd 4244	. . 3 $/\$ $/\$
9	1, 8	eqeq12d 2465	. 2 $/\$ $/\$
10		df-rdg 7078	. . 3 recs
11		df-recs 7044	. . 3 recs $/\$
12		vex 3098	. . . . . . . . . . . . 13
13	12	resex 5307	. . . . . . . . . . . 12
14		eqeq1 2447	. . . . . . . . . . . . . . 15
15		relres 5291	. . . . . . . . . . . . . . . 16
16		reldm0 5210	. . . . . . . . . . . . . . . 16
17	15, 16	ax-mp 5	. . . . . . . . . . . . . . 15
18	14, 17	syl6bb 261	. . . . . . . . . . . . . 14
19		dmeq 5193	. . . . . . . . . . . . . . . 16
20		limeq 4880	. . . . . . . . . . . . . . . 16
21	19, 20	syl 16	. . . . . . . . . . . . . . 15
22		rneq 5218	. . . . . . . . . . . . . . . . 17
23		df-ima 5002	. . . . . . . . . . . . . . . . 17
24	22, 23	syl6eqr 2502	. . . . . . . . . . . . . . . 16
25	24	unieqd 4244	. . . . . . . . . . . . . . 15
26		id 22	. . . . . . . . . . . . . . . . 17
27	19	unieqd 4244	. . . . . . . . . . . . . . . . 17
28	26, 27	fveq12d 5862	. . . . . . . . . . . . . . . 16
29	28	fveq2d 5860	. . . . . . . . . . . . . . 15
30	21, 25, 29	ifbieq12d 3953	. . . . . . . . . . . . . 14
31	18, 30	ifbieq2d 3951	. . . . . . . . . . . . 13
32		eqid 2443	. . . . . . . . . . . . 13
33		vex 3098	. . . . . . . . . . . . . 14
34		imaexg 6722	. . . . . . . . . . . . . . . . 17
35	12, 34	ax-mp 5	. . . . . . . . . . . . . . . 16
36	35	uniex 6581	. . . . . . . . . . . . . . 15
37		fvex 5866	. . . . . . . . . . . . . . 15
38	36, 37	ifex 3995	. . . . . . . . . . . . . 14
39	33, 38	ifex 3995	. . . . . . . . . . . . 13
40	31, 32, 39	fvmpt 5941	. . . . . . . . . . . 12
41	13, 40	ax-mp 5	. . . . . . . . . . 11
42		dmres 5284	. . . . . . . . . . . . 13
43		onelss 4910	. . . . . . . . . . . . . . . . 17
44	43	imp 429	. . . . . . . . . . . . . . . 16 $/\$
45	44	3adant2 1016	. . . . . . . . . . . . . . 15 $/\$ $/\$
46		fndm 5670	. . . . . . . . . . . . . . . 16
47	46	3ad2ant2 1019	. . . . . . . . . . . . . . 15 $/\$ $/\$
48	45, 47	sseqtr4d 3526	. . . . . . . . . . . . . 14 $/\$ $/\$
49		df-ss 3475	. . . . . . . . . . . . . 14
50	48, 49	sylib 196	. . . . . . . . . . . . 13 $/\$ $/\$
51	42, 50	syl5eq 2496	. . . . . . . . . . . 12 $/\$ $/\$
52		eqeq1 2447	. . . . . . . . . . . . . 14
53		limeq 4880	. . . . . . . . . . . . . . 15
54		unieq 4242	. . . . . . . . . . . . . . . . 17
55	54	fveq2d 5860	. . . . . . . . . . . . . . . 16
56	55	fveq2d 5860	. . . . . . . . . . . . . . 15
57	53, 56	ifbieq2d 3951	. . . . . . . . . . . . . 14
58	52, 57	ifbieq2d 3951	. . . . . . . . . . . . 13
59		onelon 4893	. . . . . . . . . . . . . . . 16 $/\$
60		eloni 4878	. . . . . . . . . . . . . . . 16
61	59, 60	syl 16	. . . . . . . . . . . . . . 15 $/\$
62	61	3adant2 1016	. . . . . . . . . . . . . 14 $/\$ $/\$
63		ordzsl 6665	. . . . . . . . . . . . . . 15 $\/$ $\/$
64		iftrue 3932	. . . . . . . . . . . . . . . . 17
65		iftrue 3932	. . . . . . . . . . . . . . . . 17
66	64, 65	eqtr4d 2487	. . . . . . . . . . . . . . . 16
67		vex 3098	. . . . . . . . . . . . . . . . . . . . . . 23
68	67	sucid 4947	. . . . . . . . . . . . . . . . . . . . . 22
69		fvres 5870	. . . . . . . . . . . . . . . . . . . . . 22
70	68, 69	ax-mp 5	. . . . . . . . . . . . . . . . . . . . 21
71		eloni 4878	. . . . . . . . . . . . . . . . . . . . . . 23
72		ordunisuc 6652	. . . . . . . . . . . . . . . . . . . . . . 23
73	71, 72	syl 16	. . . . . . . . . . . . . . . . . . . . . 22
74	73	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . 21
75	73	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . 21
76	70, 74, 75	3eqtr4a 2510	. . . . . . . . . . . . . . . . . . . 20
77	76	fveq2d 5860	. . . . . . . . . . . . . . . . . . 19
78		nsuceq0 4948	. . . . . . . . . . . . . . . . . . . . . 22
79	78	neii 2642	. . . . . . . . . . . . . . . . . . . . 21
80	79	iffalsei 3936	. . . . . . . . . . . . . . . . . . . 20
81		nlimsucg 6662	. . . . . . . . . . . . . . . . . . . . 21
82		iffalse 3935	. . . . . . . . . . . . . . . . . . . . 21
83	67, 81, 82	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
84	80, 83	eqtri 2472	. . . . . . . . . . . . . . . . . . 19
85	79	iffalsei 3936	. . . . . . . . . . . . . . . . . . . 20
86		iffalse 3935	. . . . . . . . . . . . . . . . . . . . 21
87	67, 81, 86	mp2b 10	. . . . . . . . . . . . . . . . . . . 20
88	85, 87	eqtri 2472	. . . . . . . . . . . . . . . . . . 19
89	77, 84, 88	3eqtr4g 2509	. . . . . . . . . . . . . . . . . 18
90		eqeq1 2447	. . . . . . . . . . . . . . . . . . . 20
91		limeq 4880	. . . . . . . . . . . . . . . . . . . . 21
92		reseq2 5258	. . . . . . . . . . . . . . . . . . . . . . 23
93		unieq 4242	. . . . . . . . . . . . . . . . . . . . . . 23
94	92, 93	fveq12d 5862	. . . . . . . . . . . . . . . . . . . . . 22
95	94	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . 21
96	91, 95	ifbieq2d 3951	. . . . . . . . . . . . . . . . . . . 20
97	90, 96	ifbieq2d 3951	. . . . . . . . . . . . . . . . . . 19
98	93	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . . 22
99	98	fveq2d 5860	. . . . . . . . . . . . . . . . . . . . 21
100	91, 99	ifbieq2d 3951	. . . . . . . . . . . . . . . . . . . 20
101	90, 100	ifbieq2d 3951	. . . . . . . . . . . . . . . . . . 19
102	97, 101	eqeq12d 2465	. . . . . . . . . . . . . . . . . 18
103	89, 102	syl5ibrcom 222	. . . . . . . . . . . . . . . . 17
104	103	rexlimiv 2929	. . . . . . . . . . . . . . . 16
105		iftrue 3932	. . . . . . . . . . . . . . . . . 18
106		df-lim 4873	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
107	106	simp2bi 1013	. . . . . . . . . . . . . . . . . . . 20
108	107	neneqd 2645	. . . . . . . . . . . . . . . . . . 19
109	108	iffalsed 3937	. . . . . . . . . . . . . . . . . 18
110		iftrue 3932	. . . . . . . . . . . . . . . . . 18
111	105, 109, 110	3eqtr4d 2494	. . . . . . . . . . . . . . . . 17
112	108	iffalsed 3937	. . . . . . . . . . . . . . . . 17
113	111, 112	eqtr4d 2487	. . . . . . . . . . . . . . . 16
114	66, 104, 113	3jaoi 1292	. . . . . . . . . . . . . . 15 $\/$ $\/$
115	63, 114	sylbi 195	. . . . . . . . . . . . . 14
116	62, 115	syl 16	. . . . . . . . . . . . 13 $/\$ $/\$
117	58, 116	sylan9eqr 2506	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
118	51, 117	mpdan 668	. . . . . . . . . . 11 $/\$ $/\$
119	41, 118	syl5eq 2496	. . . . . . . . . 10 $/\$ $/\$
120	119	eqeq2d 2457	. . . . . . . . 9 $/\$ $/\$
121	120	3expa 1197	. . . . . . . 8 $/\$ $/\$
122	121	ralbidva 2879	. . . . . . 7 $/\$
123	122	pm5.32da 641	. . . . . 6 $/\$ $/\$
124	123	rexbiia 2944	. . . . 5 $/\$ $/\$
125	124	abbii 2577	. . . 4 $/\$ $/\$
126	125	unieqi 4243	. . 3 $/\$ $/\$
127	10, 11, 126	3eqtri 2476	. 2 $/\$
128	9, 127	vtoclg 3153	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $\/$ w3o 973 $/\$ w3a 974

wceq 1383

wcel 1804

cab 2428

wne 2638

wral 2793

wrex 2794

cvv 3095

cin 3460

wss 3461

c0 3770

cif 3926

cuni 4234

cmpt 4495

word 4867

con0 4868

wlim 4869

csuc 4870

cdm 4989

crn 4990

cres 4991

cima 4992

wrel 4994

wfn 5573

cfv 5578 recscrecs 7043

crdg 7077

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-sep 4558 ax-nul 4566 ax-pr 4676 ax-un 6577

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-ral 2798 df-rex 2799 df-rab 2802 df-v 3097 df-sbc 3314 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-fv 5586 df-recs 7044 df-rdg 7078

This theorem is referenced by: dfrdg3 29204

W3C validator