dfrdg4 - Mathbox for Scott Fenton

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

Theorem dfrdg4 28003

Description: A quantifier-free definition of the recursive definition generator. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)

**Assertion**
Ref	Expression
dfrdg4	Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ

Proof of Theorem dfrdg4 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfrdg3 27632	. 2 $/\$
2		an12 795	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
3		df-fn 5442	. . . . . . . . . 10 $/\$
4		ancom 450	. . . . . . . . . 10 $/\$ $/\$
5		eqcom 2445	. . . . . . . . . . 11
6	5	anbi1i 695	. . . . . . . . . 10 $/\$ $/\$
7	3, 4, 6	3bitri 271	. . . . . . . . 9 $/\$
8	7	anbi1i 695	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9		anass 649	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	2, 8, 9	3bitri 271	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
11	10	exbii 1634	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
12		vex 2996	. . . . . . . 8
13	12	dmex 6532	. . . . . . 7
14		eleq1 2503	. . . . . . . . 9
15		raleq 2938	. . . . . . . . 9
16	14, 15	anbi12d 710	. . . . . . . 8 $/\$ $/\$
17	16	anbi2d 703	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
18	13, 17	ceqsexv 3030	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
19	11, 18	bitri 249	. . . . 5 $/\$ $/\$ $/\$ $/\$
20		df-rex 2742	. . . . 5 $/\$ $/\$ $/\$
21		eldif 3359	. . . . . 6 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
22		elin 3560	. . . . . . . 8 Domain $/\$ Domain
23	12	elfuns 27968	. . . . . . . . 9
24	12	elima 5195	. . . . . . . . . 10 Domain Domain
25		df-rex 2742	. . . . . . . . . 10 Domain $/\$ Domain
26		ancom 450	. . . . . . . . . . . . 13 $/\$ Domain Domain $/\$
27		vex 2996	. . . . . . . . . . . . . . . 16
28	27, 12	brcnv 5043	. . . . . . . . . . . . . . 15 Domain Domain
29	12, 27	brdomain 27986	. . . . . . . . . . . . . . 15 Domain
30	28, 29	bitri 249	. . . . . . . . . . . . . 14 Domain
31	30	anbi1i 695	. . . . . . . . . . . . 13 Domain $/\$ $/\$
32	26, 31	bitri 249	. . . . . . . . . . . 12 $/\$ Domain $/\$
33	32	exbii 1634	. . . . . . . . . . 11 $/\$ Domain $/\$
34	13, 14	ceqsexv 3030	. . . . . . . . . . 11 $/\$
35	33, 34	bitri 249	. . . . . . . . . 10 $/\$ Domain
36	24, 25, 35	3bitri 271	. . . . . . . . 9 Domain
37	23, 36	anbi12i 697	. . . . . . . 8 $/\$ Domain $/\$
38	22, 37	bitri 249	. . . . . . 7 Domain $/\$
39	38	anbi1i 695	. . . . . 6 Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
40		brdif 4363	. . . . . . . . . . . . . . 15 Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Apply Img FullFun Apply pprod Succ
41		vex 2996	. . . . . . . . . . . . . . . . . 18
42	12, 41	brco 5031	. . . . . . . . . . . . . . . . 17 Domain Domain $/\$
43	29	anbi1i 695	. . . . . . . . . . . . . . . . . . 19 Domain $/\$ $/\$
44	43	exbii 1634	. . . . . . . . . . . . . . . . . 18 Domain $/\$ $/\$
45		breq1 4316	. . . . . . . . . . . . . . . . . . 19
46	13, 45	ceqsexv 3030	. . . . . . . . . . . . . . . . . 18 $/\$
47	44, 46	bitri 249	. . . . . . . . . . . . . . . . 17 Domain $/\$
48	13, 41	brcnv 5043	. . . . . . . . . . . . . . . . . 18
49	13	epelc 4655	. . . . . . . . . . . . . . . . . 18
50	48, 49	bitri 249	. . . . . . . . . . . . . . . . 17
51	42, 47, 50	3bitri 271	. . . . . . . . . . . . . . . 16 Domain
52	51	anbi1i 695	. . . . . . . . . . . . . . 15 Domain $/\$ Apply Img FullFun Apply pprod Succ $/\$ Apply Img FullFun Apply pprod Succ
53	40, 52	bitri 249	. . . . . . . . . . . . . 14 Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ Apply Img FullFun Apply pprod Succ
54		onelon 4765	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
55	54	3adant1 1006	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
56		brun 4361	. . . . . . . . . . . . . . . . . . . . . . . . 25 Img FullFun Apply pprod Succ $\/$ Img FullFun Apply pprod Succ
57		brxp 4891	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
58		opelxp 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
59	12, 58	mpbiran 909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		elsn 3912	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62		elsn 3912	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
63	61, 62	anbi12i 697	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
64	57, 63	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
65		brun 4361	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img FullFun Apply pprod Succ Img $\/$ FullFun Apply pprod Succ
66	27	brres 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img Img $/\$
67		opex 4577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
68	67, 27	brco 5031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img Img $/\$
69		vex 2996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
70	12, 41, 69	brimg 27990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Img
71	27	brbigcup 27951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	70, 71	anbi12i 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Img $/\$ $/\$
73	72	exbii 1634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img $/\$ $/\$
74		imaexg 6536	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
75	12, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
76		unieq 4120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77	76	eqeq1d 2451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
78	75, 77	ceqsexv 3030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
79		eqcom 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
80	78, 79	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
81	68, 73, 80	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Img
82		opelxp 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
83	12, 82	mpbiran 909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
84	41	ellimits 27963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
85	83, 84	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
86	81, 85	anbi12ci 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img $/\$ $/\$
87	66, 86	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Img $/\$
88	27	brres 5138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod Succ FullFun Apply pprod $/\$ Succ
89	67, 27	brco 5031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 FullFun Apply pprod Apply pprod $/\$ FullFun
90		vex 2996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
91	67, 90	brco 5031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Apply pprod pprod $/\$ Apply
92	12, 41, 69	brpprod3a 27939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 pprod $/\$ $/\$
93		3anrot 970	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
94	90	ideq 5013	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
95		equcom 1732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
96	94, 95	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
97		vex 2996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
98	97	brbigcup 27951	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
99		eqcom 2445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
100	98, 99	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
101		biid 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
102	96, 100, 101	3anbi123i 1176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
103	93, 102	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$
104	103	2exbii 1635	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
105	41	uniex 6397	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
106		opeq1 4080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
107	106	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
108		opeq2 4081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
109	108	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
110	12, 105, 107, 109	ceqsex2v 3032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
111	92, 104, 110	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 pprod
112	111	anbi1i 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 pprod $/\$ Apply $/\$ Apply
113	112	exbii 1634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 pprod $/\$ Apply $/\$ Apply
114		opex 4577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
115		breq1 4316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Apply Apply
116	114, 115	ceqsexv 3030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ Apply Apply
117	12, 105, 90	brapply 27991	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Apply
118	116, 117	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ Apply
119	91, 113, 118	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Apply pprod
120	90, 27	brfullfun 28001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 FullFun
121	119, 120	anbi12i 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Apply pprod $/\$ FullFun $/\$
122	121	exbii 1634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Apply pprod $/\$ FullFun $/\$
123		fvex 5722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
124		fveq2 5712	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
125	124	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
126	123, 125	ceqsexv 3030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
127	89, 122, 126	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 FullFun Apply pprod
128		opelxp 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ $/\$ Succ
129	12, 128	mpbiran 909	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
130	41	elrn 5101	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
131	69, 41	brsuccf 27994	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ
132	131	exbii 1634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ
133	129, 130, 132	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Succ
134	127, 133	anbi12ci 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod $/\$ Succ $/\$
135	88, 134	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 FullFun Apply pprod Succ $/\$
136	87, 135	orbi12i 521	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img $\/$ FullFun Apply pprod Succ $/\$ $\/$ $/\$
137	65, 136	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Img FullFun Apply pprod Succ $/\$ $\/$ $/\$
138	64, 137	orbi12i 521	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ Img FullFun Apply pprod Succ $/\$ $\/$ $/\$ $\/$ $/\$
139	56, 138	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . 24 Img FullFun Apply pprod Succ $/\$ $\/$ $/\$ $\/$ $/\$
140		onzsl 6478	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$ $/\$
141		nlim0 4798	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
142		limeq 4752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
143	141, 142	mtbiri 303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
144	143	intnanrd 908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
145		nsuceq0 4820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
146		neeq2 2646	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
147	145, 146	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
148	147	necomd 2640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
149	148	neneqd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
150	149	nexdv 1818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
151	150	intnanrd 908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
152		ioran 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
153	144, 151, 152	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$
154		orel2 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
155	153, 154	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
156		iftrue 3818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
157		unisnif 27978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
158	156, 157	syl6eqr 2493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
159	158	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
160	159	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
161	160	adantld 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
162	155, 161	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
163	159	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
164	163	anc2li 557	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
165		orc 385	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
166	164, 165	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
167	162, 166	impbid 191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$ $/\$ $\/$ $/\$
168		neeq1 2644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
169	145, 168	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
170	169	neneqd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
171	170	intnanrd 908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
172	171	rexlimivw 2858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
173		orel1 382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
174	172, 173	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
175		nlimsucg 6474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
176	69, 175	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177		limeq 4752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178	176, 177	mtbiri 303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179	178	rexlimivw 2858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180	179	intnanrd 908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
181		orel1 382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $/\$
182	180, 181	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $/\$
183		df-ne 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
184	145, 183	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
185	184	iffalsei 3821	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
186		iffalse 3820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
187	69, 175, 186	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
188	185, 187	eqtri 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
189		eqeq1 2449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
190		unieq 4120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
191	190	fveq2d 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
192	191	fveq2d 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
193	177, 192	ifbieq2d 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
194	189, 193	ifbieq2d 3835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
195	188, 194, 192	3eqtr4a 2501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
196	195	rexlimivw 2858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
197	196	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
198	197	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
199	198	adantld 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
200	174, 182, 199	3syld 55	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
201		rexex 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
202	197	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
203		olc 384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$
204	203	olcd 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
205	201, 202, 204	syl6an 545	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
206	200, 205	impbid 191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$ $/\$ $\/$ $/\$
207	143	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
208	207	intnanrd 908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
209	208, 173	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
210	178	exlimiv 1688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	210	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212	211	intnanrd 908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
213		orel2 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$ $/\$
214	212, 213	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$
215		iffalse 3820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
216	207, 215	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
217		iftrue 3818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
218	216, 217	eqtrd 2475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
219	218	eqeq2d 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
220	219	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
221	220	adantld 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
222	209, 214, 221	3syld 55	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$
223	222	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
224	219	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
225	224	anc2li 557	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
226		orc 385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$
227	226	olcd 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
228	225, 227	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$
229	228	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
230	223, 229	impbid 191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
231	167, 206, 230	3jaoi 1281	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
232	140, 231	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$ $/\$ $\/$ $/\$
233	139, 232	syl5bb 257	. . . . . . . . . . . . . . . . . . . . . . 23 Img FullFun Apply pprod Succ
234	55, 233	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Img FullFun Apply pprod Succ
235	27, 67	brcnv 5043	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply Apply
236	12, 41, 27	brapply 27991	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply
237	235, 236	bitri 249	. . . . . . . . . . . . . . . . . . . . . . 23 Apply
238	237	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Apply
239	234, 238	anbi12d 710	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
240		ancom 450	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
241	239, 240	syl6bb 261	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
242	241	exbidv 1680	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
243		df-br 4314	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
244	67	elfix 27956	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
245	67, 67	brco 5031	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Img FullFun Apply pprod Succ $/\$ Apply
246	243, 244, 245	3bitri 271	. . . . . . . . . . . . . . . . . . 19 Apply Img FullFun Apply pprod Succ Img FullFun Apply pprod Succ $/\$ Apply
247		fvex 5722	. . . . . . . . . . . . . . . . . . . 20
248	247	eqvinc 3107	. . . . . . . . . . . . . . . . . . 19 $/\$
249	242, 246, 248	3bitr4g 288	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
250	249	notbid 294	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
251	250	3expia 1189	. . . . . . . . . . . . . . . 16 $/\$ Apply Img FullFun Apply pprod Succ
252	251	pm5.32d 639	. . . . . . . . . . . . . . 15 $/\$ $/\$ Apply Img FullFun Apply pprod Succ $/\$
253		annim 425	. . . . . . . . . . . . . . 15 $/\$
254	252, 253	syl6bb 261	. . . . . . . . . . . . . 14 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
255	53, 254	syl5bb 257	. . . . . . . . . . . . 13 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
256	255	exbidv 1680	. . . . . . . . . . . 12 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
257		exnal 1618	. . . . . . . . . . . 12
258	256, 257	syl6rbb 262	. . . . . . . . . . 11 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
259	12	eldm 5058	. . . . . . . . . . 11 Domain $\$ Apply Img FullFun Apply pprod Succ Domain $\$ Apply Img FullFun Apply pprod Succ
260	258, 259	syl6bbr 263	. . . . . . . . . 10 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
261	260	con1bid 330	. . . . . . . . 9 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
262		df-ral 2741	. . . . . . . . 9
263	261, 262	syl6bbr 263	. . . . . . . 8 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
264	263	pm5.32i 637	. . . . . . 7 $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
265		anass 649	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
266	264, 265	bitri 249	. . . . . 6 $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
267	21, 39, 266	3bitri 271	. . . . 5 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
268	19, 20, 267	3bitr4ri 278	. . . 4 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
269	268	abbi2i 2560	. . 3 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
270	269	unieqi 4121	. 2 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
271	1, 270	eqtr4i 2466	1 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369 $\/$ w3o 964 $/\$ w3a 965

wal 1367

wceq 1369

wex 1586

wcel 1756

cab 2429

wne 2620

wral 2736

wrex 2737

cvv 2993 $\$ cdif 3346

cun 3347

cin 3348

c0 3658

cif 3812

csn 3898

cop 3904

cuni 4112 class class class wbr 4313

cep 4651

cid 4652

con0 4740

wlim 4741

csuc 4742

cxp 4859

ccnv 4860

cdm 4861

crn 4862

cres 4863

cima 4864

ccom 4865

wfun 5433

wfn 5434

cfv 5439

crdg 6886 pprodcpprod 27883

cbigcup 27886

cfix 27887

climits 27888

cfuns 27889 Imgcimg 27894 Domaincdomain 27895 Applycapply 27897 Succcsuccf 27900 FullFuncfullfn 27902

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4424 ax-sep 4434 ax-nul 4442 ax-pow 4491 ax-pr 4552 ax-un 6393

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-ral 2741 df-rex 2742 df-reu 2743 df-rab 2745 df-v 2995 df-sbc 3208 df-csb 3310 df-dif 3352 df-un 3354 df-in 3356 df-ss 3363 df-pss 3365 df-nul 3659 df-if 3813 df-pw 3883 df-sn 3899 df-pr 3901 df-tp 3903 df-op 3905 df-uni 4113 df-iun 4194 df-br 4314 df-opab 4372 df-mpt 4373 df-tr 4407 df-eprel 4653 df-id 4657 df-po 4662 df-so 4663 df-fr 4700 df-we 4702 df-ord 4743 df-on 4744 df-lim 4745 df-suc 4746 df-xp 4867 df-rel 4868 df-cnv 4869 df-co 4870 df-dm 4871 df-rn 4872 df-res 4873 df-ima 4874 df-iota 5402 df-fun 5441 df-fn 5442 df-f 5443 df-f1 5444 df-fo 5445 df-f1o 5446 df-fv 5447 df-om 6498 df-1st 6598 df-2nd 6599 df-recs 6853 df-rdg 6887 df-symdif 27871 df-txp 27906 df-pprod 27907 df-bigcup 27910 df-fix 27911 df-limits 27912 df-funs 27913 df-singleton 27914 df-singles 27915 df-image 27916 df-cart 27917 df-img 27918 df-domain 27919 df-cup 27921 df-succf 27924 df-apply 27925 df-funpart 27926 df-fullfun 27927

This theorem is referenced by: (None)

W3C validator