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 29828

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 29469	. 2 $/\$
2		an12 795	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
3		df-fn 5573	. . . . . . . . . 10 $/\$
4		ancom 448	. . . . . . . . . 10 $/\$ $/\$
5		eqcom 2463	. . . . . . . . . . 11
6	5	anbi1i 693	. . . . . . . . . 10 $/\$ $/\$
7	3, 4, 6	3bitri 271	. . . . . . . . 9 $/\$
8	7	anbi1i 693	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9		anass 647	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	2, 8, 9	3bitri 271	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
11	10	exbii 1672	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
12		vex 3109	. . . . . . . 8
13	12	dmex 6706	. . . . . . 7
14		eleq1 2526	. . . . . . . . 9
15		raleq 3051	. . . . . . . . 9
16	14, 15	anbi12d 708	. . . . . . . 8 $/\$ $/\$
17	16	anbi2d 701	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
18	13, 17	ceqsexv 3143	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
19	11, 18	bitri 249	. . . . 5 $/\$ $/\$ $/\$ $/\$
20		df-rex 2810	. . . . 5 $/\$ $/\$ $/\$
21		eldif 3471	. . . . . 6 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
22		elin 3673	. . . . . . . 8 Domain $/\$ Domain
23	12	elfuns 29793	. . . . . . . . 9
24	12	elima 5330	. . . . . . . . . 10 Domain Domain
25		df-rex 2810	. . . . . . . . . 10 Domain $/\$ Domain
26		ancom 448	. . . . . . . . . . . . 13 $/\$ Domain Domain $/\$
27		vex 3109	. . . . . . . . . . . . . . . 16
28	27, 12	brcnv 5174	. . . . . . . . . . . . . . 15 Domain Domain
29	12, 27	brdomain 29811	. . . . . . . . . . . . . . 15 Domain
30	28, 29	bitri 249	. . . . . . . . . . . . . 14 Domain
31	30	anbi1i 693	. . . . . . . . . . . . 13 Domain $/\$ $/\$
32	26, 31	bitri 249	. . . . . . . . . . . 12 $/\$ Domain $/\$
33	32	exbii 1672	. . . . . . . . . . 11 $/\$ Domain $/\$
34	13, 14	ceqsexv 3143	. . . . . . . . . . 11 $/\$
35	33, 34	bitri 249	. . . . . . . . . 10 $/\$ Domain
36	24, 25, 35	3bitri 271	. . . . . . . . 9 Domain
37	23, 36	anbi12i 695	. . . . . . . 8 $/\$ Domain $/\$
38	22, 37	bitri 249	. . . . . . 7 Domain $/\$
39	38	anbi1i 693	. . . . . 6 Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
40		brdif 4489	. . . . . . . . . . . . . . 15 Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Apply Img FullFun Apply pprod Succ
41		vex 3109	. . . . . . . . . . . . . . . . . 18
42	12, 41	brco 5162	. . . . . . . . . . . . . . . . 17 Domain Domain $/\$
43	29	anbi1i 693	. . . . . . . . . . . . . . . . . . 19 Domain $/\$ $/\$
44	43	exbii 1672	. . . . . . . . . . . . . . . . . 18 Domain $/\$ $/\$
45		breq1 4442	. . . . . . . . . . . . . . . . . . 19
46	13, 45	ceqsexv 3143	. . . . . . . . . . . . . . . . . 18 $/\$
47	44, 46	bitri 249	. . . . . . . . . . . . . . . . 17 Domain $/\$
48	13, 41	brcnv 5174	. . . . . . . . . . . . . . . . . 18
49	13	epelc 4782	. . . . . . . . . . . . . . . . . 18
50	48, 49	bitri 249	. . . . . . . . . . . . . . . . 17
51	42, 47, 50	3bitri 271	. . . . . . . . . . . . . . . 16 Domain
52	51	anbi1i 693	. . . . . . . . . . . . . . 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 4892	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
55	54	3adant1 1012	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
56		brun 4487	. . . . . . . . . . . . . . . . . . . . . . . . 25 Img FullFun Apply pprod Succ $\/$ Img FullFun Apply pprod Succ
57		brxp 5019	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
58		opelxp 5018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
59	12, 58	mpbiran 916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		elsn 4030	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62		elsn 4030	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
63	61, 62	anbi12i 695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
64	57, 63	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
65		brun 4487	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img FullFun Apply pprod Succ Img $\/$ FullFun Apply pprod Succ
66	27	brres 5268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img Img $/\$
67		opex 4701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
68	67, 27	brco 5162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img Img $/\$
69		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
70	12, 41, 69	brimg 29815	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Img
71	27	brbigcup 29776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	70, 71	anbi12i 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Img $/\$ $/\$
73	72	exbii 1672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img $/\$ $/\$
74		imaexg 6710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
75	12, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
76		unieq 4243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77	76	eqeq1d 2456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
78	75, 77	ceqsexv 3143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
79		eqcom 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
80	78, 79	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
81	68, 73, 80	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Img
82		opelxp 5018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
83	12, 82	mpbiran 916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
84	41	ellimits 29788	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
85	83, 84	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
86	81, 85	anbi12ci 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img $/\$ $/\$
87	66, 86	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Img $/\$
88	27	brres 5268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod Succ FullFun Apply pprod $/\$ Succ
89	67, 27	brco 5162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 FullFun Apply pprod Apply pprod $/\$ FullFun
90		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
91	67, 90	brco 5162	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Apply pprod pprod $/\$ Apply
92	12, 41, 69	brpprod3a 29764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 pprod $/\$ $/\$
93		3anrot 976	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
94	90	ideq 5144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
95		equcom 1799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
96	94, 95	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
97		vex 3109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
98	97	brbigcup 29776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
99		eqcom 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
100	98, 99	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
101		biid 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
102	96, 100, 101	3anbi123i 1183	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
103	93, 102	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$
104	103	2exbii 1673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
105	41	uniex 6569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
106		opeq1 4203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
107	106	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
108		opeq2 4204	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
109	108	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
110	12, 105, 107, 109	ceqsex2v 3145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
111	92, 104, 110	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 pprod
112	111	anbi1i 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 pprod $/\$ Apply $/\$ Apply
113	112	exbii 1672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 pprod $/\$ Apply $/\$ Apply
114		opex 4701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
115		breq1 4442	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Apply Apply
116	114, 115	ceqsexv 3143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ Apply Apply
117	12, 105, 90	brapply 29816	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Apply
118	116, 117	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ Apply
119	91, 113, 118	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Apply pprod
120	90, 27	brfullfun 29826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 FullFun
121	119, 120	anbi12i 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Apply pprod $/\$ FullFun $/\$
122	121	exbii 1672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Apply pprod $/\$ FullFun $/\$
123		fvex 5858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
124		fveq2 5848	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
125	124	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
126	123, 125	ceqsexv 3143	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
127	89, 122, 126	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 FullFun Apply pprod
128		opelxp 5018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ $/\$ Succ
129	12, 128	mpbiran 916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
130	41	elrn 5232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
131	69, 41	brsuccf 29819	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ
132	131	exbii 1672	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ
133	129, 130, 132	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Succ
134	127, 133	anbi12ci 696	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod $/\$ Succ $/\$
135	88, 134	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 FullFun Apply pprod Succ $/\$
136	87, 135	orbi12i 519	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img $\/$ FullFun Apply pprod Succ $/\$ $\/$ $/\$
137	65, 136	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Img FullFun Apply pprod Succ $/\$ $\/$ $/\$
138	64, 137	orbi12i 519	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ Img FullFun Apply pprod Succ $/\$ $\/$ $/\$ $\/$ $/\$
139	56, 138	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . 24 Img FullFun Apply pprod Succ $/\$ $\/$ $/\$ $\/$ $/\$
140		onzsl 6654	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$ $/\$
141		nlim0 4925	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
142		limeq 4879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
143	141, 142	mtbiri 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
144	143	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
145		nsuceq0 4947	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
146		neeq2 2737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
147	145, 146	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
148	147	necomd 2725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
149	148	neneqd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
150	149	nexdv 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
151	150	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
152		ioran 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
153	144, 151, 152	sylanbrc 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$
154		orel2 381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
155	153, 154	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
156		iftrue 3935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
157		unisnif 29803	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
158	156, 157	syl6eqr 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
159	158	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
160	159	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
161	160	adantld 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
162	155, 161	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
163	159	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
164	163	anc2li 555	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
165		orc 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
166	164, 165	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
167	162, 166	impbid 191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$ $/\$ $\/$ $/\$
168		neeq1 2735	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
169	145, 168	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
170	169	neneqd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
171	170	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
172	171	rexlimivw 2943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
173		orel1 380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
174	172, 173	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
175		nlimsucg 6650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
176	69, 175	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177		limeq 4879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178	176, 177	mtbiri 301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179	178	rexlimivw 2943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180	179	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
181		orel1 380	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $/\$
182	180, 181	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $/\$
183	145	neii 2653	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	183	iffalsei 3939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185		iffalse 3938	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
186	69, 175, 185	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
187	184, 186	eqtri 2483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
188		eqeq1 2458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
189		unieq 4243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
190	189	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191	190	fveq2d 5852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192	177, 191	ifbieq2d 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193	188, 192	ifbieq2d 3954	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
194	187, 193, 191	3eqtr4a 2521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
195	194	rexlimivw 2943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
196	195	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
197	196	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
198	197	adantld 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
199	174, 182, 198	3syld 55	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
200		rexex 2911	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
201	196	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
202		olc 382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$
203	202	olcd 391	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
204	200, 201, 203	syl6an 543	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
205	199, 204	impbid 191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$ $/\$ $\/$ $/\$
206	143	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
207	206	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
208	207, 173	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
209	178	exlimiv 1727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
210	209	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
211	210	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
212		orel2 381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$ $/\$
213	211, 212	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$
214	206	iffalsed 3940	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
215		iftrue 3935	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
216	214, 215	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
217	216	eqeq2d 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
218	217	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
219	218	adantld 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
220	208, 213, 219	3syld 55	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$
221	220	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
222	217	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
223	222	anc2li 555	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
224		orc 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$
225	224	olcd 391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
226	223, 225	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$
227	226	adantl 464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
228	221, 227	impbid 191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
229	167, 205, 228	3jaoi 1289	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
230	140, 229	sylbi 195	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$ $/\$ $\/$ $/\$
231	139, 230	syl5bb 257	. . . . . . . . . . . . . . . . . . . . . . 23 Img FullFun Apply pprod Succ
232	55, 231	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Img FullFun Apply pprod Succ
233	27, 67	brcnv 5174	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply Apply
234	12, 41, 27	brapply 29816	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply
235	233, 234	bitri 249	. . . . . . . . . . . . . . . . . . . . . . 23 Apply
236	235	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Apply
237	232, 236	anbi12d 708	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
238		ancom 448	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
239	237, 238	syl6bb 261	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
240	239	exbidv 1719	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
241		df-br 4440	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
242	67	elfix 29781	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
243	67, 67	brco 5162	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Img FullFun Apply pprod Succ $/\$ Apply
244	241, 242, 243	3bitri 271	. . . . . . . . . . . . . . . . . . 19 Apply Img FullFun Apply pprod Succ Img FullFun Apply pprod Succ $/\$ Apply
245		fvex 5858	. . . . . . . . . . . . . . . . . . . 20
246	245	eqvinc 3223	. . . . . . . . . . . . . . . . . . 19 $/\$
247	240, 244, 246	3bitr4g 288	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
248	247	notbid 292	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
249	248	3expia 1196	. . . . . . . . . . . . . . . 16 $/\$ Apply Img FullFun Apply pprod Succ
250	249	pm5.32d 637	. . . . . . . . . . . . . . 15 $/\$ $/\$ Apply Img FullFun Apply pprod Succ $/\$
251		annim 423	. . . . . . . . . . . . . . 15 $/\$
252	250, 251	syl6bb 261	. . . . . . . . . . . . . 14 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
253	53, 252	syl5bb 257	. . . . . . . . . . . . 13 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
254	253	exbidv 1719	. . . . . . . . . . . 12 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
255		exnal 1653	. . . . . . . . . . . 12
256	254, 255	syl6rbb 262	. . . . . . . . . . 11 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
257	12	eldm 5189	. . . . . . . . . . 11 Domain $\$ Apply Img FullFun Apply pprod Succ Domain $\$ Apply Img FullFun Apply pprod Succ
258	256, 257	syl6bbr 263	. . . . . . . . . 10 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
259	258	con1bid 328	. . . . . . . . 9 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
260		df-ral 2809	. . . . . . . . 9
261	259, 260	syl6bbr 263	. . . . . . . 8 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
262	261	pm5.32i 635	. . . . . . 7 $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
263		anass 647	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
264	262, 263	bitri 249	. . . . . 6 $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
265	21, 39, 264	3bitri 271	. . . . 5 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
266	19, 20, 265	3bitr4ri 278	. . . 4 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
267	266	abbi2i 2587	. . 3 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
268	267	unieqi 4244	. 2 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
269	1, 268	eqtr4i 2486	1 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367 $\/$ w3o 970 $/\$ w3a 971

wal 1396

wceq 1398

wex 1617

wcel 1823

cab 2439

wne 2649

wral 2804

wrex 2805

cvv 3106 $\$ cdif 3458

cun 3459

cin 3460

c0 3783

cif 3929

csn 4016

cop 4022

cuni 4235 class class class wbr 4439

cep 4778

cid 4779

con0 4867

wlim 4868

csuc 4869

cxp 4986

ccnv 4987

cdm 4988

crn 4989

cres 4990

cima 4991

ccom 4992

wfun 5564

wfn 5565

cfv 5570

crdg 7067 pprodcpprod 29708

cbigcup 29711

cfix 29712

climits 29713

cfuns 29714 Imgcimg 29719 Domaincdomain 29720 Applycapply 29722 Succcsuccf 29725 FullFuncfullfn 29727

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-rep 4550 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-ral 2809 df-rex 2810 df-reu 2811 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-symdif 3715 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-om 6674 df-1st 6773 df-2nd 6774 df-recs 7034 df-rdg 7068 df-txp 29731 df-pprod 29732 df-bigcup 29735 df-fix 29736 df-limits 29737 df-funs 29738 df-singleton 29739 df-singles 29740 df-image 29741 df-cart 29742 df-img 29743 df-domain 29744 df-cup 29746 df-succf 29749 df-apply 29750 df-funpart 29751 df-fullfun 29752

This theorem is referenced by: (None)

W3C validator