dfrdg4 - Mathbox for Scott Fenton

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

Theorem dfrdg4 30766

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 30491	. 2 $/\$
2		an12 811	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
3		df-fn 5603	. . . . . . . . . 10 $/\$
4		ancom 456	. . . . . . . . . 10 $/\$ $/\$
5		eqcom 2468	. . . . . . . . . . 11
6	5	anbi1i 706	. . . . . . . . . 10 $/\$ $/\$
7	3, 4, 6	3bitri 279	. . . . . . . . 9 $/\$
8	7	anbi1i 706	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9		anass 659	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	2, 8, 9	3bitri 279	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
11	10	exbii 1728	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
12		vex 3059	. . . . . . . 8
13	12	dmex 6752	. . . . . . 7
14		eleq1 2527	. . . . . . . . 9
15		raleq 2998	. . . . . . . . 9
16	14, 15	anbi12d 722	. . . . . . . 8 $/\$ $/\$
17	16	anbi2d 715	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
18	13, 17	ceqsexv 3095	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
19	11, 18	bitri 257	. . . . 5 $/\$ $/\$ $/\$ $/\$
20		df-rex 2754	. . . . 5 $/\$ $/\$ $/\$
21		eldif 3425	. . . . . 6 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
22		elin 3628	. . . . . . . 8 Domain $/\$ Domain
23	12	elfuns 30730	. . . . . . . . 9
24	12	elima 5191	. . . . . . . . . 10 Domain Domain
25		df-rex 2754	. . . . . . . . . 10 Domain $/\$ Domain
26		ancom 456	. . . . . . . . . . . . 13 $/\$ Domain Domain $/\$
27		vex 3059	. . . . . . . . . . . . . . . 16
28	27, 12	brcnv 5035	. . . . . . . . . . . . . . 15 Domain Domain
29	12, 27	brdomain 30748	. . . . . . . . . . . . . . 15 Domain
30	28, 29	bitri 257	. . . . . . . . . . . . . 14 Domain
31	30	anbi1i 706	. . . . . . . . . . . . 13 Domain $/\$ $/\$
32	26, 31	bitri 257	. . . . . . . . . . . 12 $/\$ Domain $/\$
33	32	exbii 1728	. . . . . . . . . . 11 $/\$ Domain $/\$
34	13, 14	ceqsexv 3095	. . . . . . . . . . 11 $/\$
35	33, 34	bitri 257	. . . . . . . . . 10 $/\$ Domain
36	24, 25, 35	3bitri 279	. . . . . . . . 9 Domain
37	23, 36	anbi12i 708	. . . . . . . 8 $/\$ Domain $/\$
38	22, 37	bitri 257	. . . . . . 7 Domain $/\$
39	38	anbi1i 706	. . . . . 6 Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
40		brdif 4466	. . . . . . . . . . . . . . 15 Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Apply Img FullFun Apply pprod Succ
41		vex 3059	. . . . . . . . . . . . . . . . . 18
42	12, 41	brco 5023	. . . . . . . . . . . . . . . . 17 Domain Domain $/\$
43	29	anbi1i 706	. . . . . . . . . . . . . . . . . . 19 Domain $/\$ $/\$
44	43	exbii 1728	. . . . . . . . . . . . . . . . . 18 Domain $/\$ $/\$
45		breq1 4418	. . . . . . . . . . . . . . . . . . 19
46	13, 45	ceqsexv 3095	. . . . . . . . . . . . . . . . . 18 $/\$
47	44, 46	bitri 257	. . . . . . . . . . . . . . . . 17 Domain $/\$
48	13, 41	brcnv 5035	. . . . . . . . . . . . . . . . . 18
49	13	epelc 4765	. . . . . . . . . . . . . . . . . 18
50	48, 49	bitri 257	. . . . . . . . . . . . . . . . 17
51	42, 47, 50	3bitri 279	. . . . . . . . . . . . . . . 16 Domain
52	51	anbi1i 706	. . . . . . . . . . . . . . 15 Domain $/\$ Apply Img FullFun Apply pprod Succ $/\$ Apply Img FullFun Apply pprod Succ
53	40, 52	bitri 257	. . . . . . . . . . . . . 14 Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ Apply Img FullFun Apply pprod Succ
54		onelon 5466	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
55	54	3adant1 1032	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
56		brun 4464	. . . . . . . . . . . . . . . . . . . . . . . . 25 Img FullFun Apply pprod Succ $\/$ Img FullFun Apply pprod Succ
57		brxp 4883	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
58		opelxp 4882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
59	12, 58	mpbiran 934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		elsn 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62		elsn 3993	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
63	61, 62	anbi12i 708	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
64	57, 63	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
65		brun 4464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img FullFun Apply pprod Succ Img $\/$ FullFun Apply pprod Succ
66	27	brres 5129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img Img $/\$
67		opex 4677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
68	67, 27	brco 5023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img Img $/\$
69		vex 3059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
70	12, 41, 69	brimg 30752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Img
71	27	brbigcup 30713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	70, 71	anbi12i 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Img $/\$ $/\$
73	72	exbii 1728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img $/\$ $/\$
74		imaexg 6756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
75	12, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
76		unieq 4219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77	76	eqeq1d 2463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
78	75, 77	ceqsexv 3095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
79		eqcom 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
80	78, 79	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
81	68, 73, 80	3bitri 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Img
82		opelxp 4882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
83	12, 82	mpbiran 934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
84	41	ellimits 30725	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
85	83, 84	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
86	81, 85	anbi12ci 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img $/\$ $/\$
87	66, 86	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Img $/\$
88	27	brres 5129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod Succ FullFun Apply pprod $/\$ Succ
89	67, 27	brco 5023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 FullFun Apply pprod Apply pprod $/\$ FullFun
90		vex 3059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
91	67, 90	brco 5023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Apply pprod pprod $/\$ Apply
92	12, 41, 69	brpprod3a 30701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 pprod $/\$ $/\$
93		3anrot 996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
94	90	ideq 5005	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
95		equcom 1872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
96	94, 95	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
97		vex 3059	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
98	97	brbigcup 30713	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
99		eqcom 2468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
100	98, 99	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
101		biid 244	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
102	96, 100, 101	3anbi123i 1203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
103	93, 102	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$
104	103	2exbii 1729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
105	41	uniex 6613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
106		opeq1 4179	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
107	106	eqeq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
108		opeq2 4180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
109	108	eqeq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
110	12, 105, 107, 109	ceqsex2v 3098	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
111	92, 104, 110	3bitri 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 pprod
112	111	anbi1i 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 pprod $/\$ Apply $/\$ Apply
113	112	exbii 1728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 pprod $/\$ Apply $/\$ Apply
114		opex 4677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
115		breq1 4418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Apply Apply
116	114, 115	ceqsexv 3095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ Apply Apply
117	12, 105, 90	brapply 30753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Apply
118	116, 117	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ Apply
119	91, 113, 118	3bitri 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Apply pprod
120	90, 27	brfullfun 30763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 FullFun
121	119, 120	anbi12i 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Apply pprod $/\$ FullFun $/\$
122	121	exbii 1728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Apply pprod $/\$ FullFun $/\$
123		fvex 5897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
124		fveq2 5887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
125	124	eqeq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
126	123, 125	ceqsexv 3095	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
127	89, 122, 126	3bitri 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 FullFun Apply pprod
128		opelxp 4882	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ $/\$ Succ
129	12, 128	mpbiran 934	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
130	41	elrn 5093	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
131	69, 41	brsuccf 30756	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ
132	131	exbii 1728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ
133	129, 130, 132	3bitri 279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Succ
134	127, 133	anbi12ci 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod $/\$ Succ $/\$
135	88, 134	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 FullFun Apply pprod Succ $/\$
136	87, 135	orbi12i 528	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img $\/$ FullFun Apply pprod Succ $/\$ $\/$ $/\$
137	65, 136	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Img FullFun Apply pprod Succ $/\$ $\/$ $/\$
138	64, 137	orbi12i 528	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ Img FullFun Apply pprod Succ $/\$ $\/$ $/\$ $\/$ $/\$
139	56, 138	bitri 257	. . . . . . . . . . . . . . . . . . . . . . . 24 Img FullFun Apply pprod Succ $/\$ $\/$ $/\$ $\/$ $/\$
140		onzsl 6699	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$ $/\$
141		nlim0 5499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
142		limeq 5453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
143	141, 142	mtbiri 309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
144	143	intnanrd 933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
145		nsuceq0 5521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
146		neeq2 2698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
147	145, 146	mpbiri 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
148	147	necomd 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
149	148	neneqd 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
150	149	nexdv 1792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
151	150	intnanrd 933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
152		ioran 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
153	144, 151, 152	sylanbrc 675	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$
154		orel2 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
155	153, 154	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
156		iftrue 3898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
157		unisnif 30740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
158	156, 157	syl6eqr 2513	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
159	158	eqeq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
160	159	biimprd 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
161	160	adantld 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
162	155, 161	syld 45	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
163	159	biimpd 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
164	163	anc2li 564	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
165		orc 391	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
166	164, 165	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
167	162, 166	impbid 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$ $/\$ $\/$ $/\$
168		neeq1 2697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
169	145, 168	mpbiri 241	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
170	169	neneqd 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
171	170	intnanrd 933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
172	171	rexlimivw 2887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
173		orel1 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
174	172, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
175		nlimsucg 6695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
176	69, 175	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177		limeq 5453	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178	176, 177	mtbiri 309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179	178	rexlimivw 2887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180	179	intnanrd 933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
181		orel1 388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $/\$
182	180, 181	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $/\$
183	145	neii 2636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
184	183	iffalsei 3902	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
185		iffalse 3901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
186	69, 175, 185	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
187	184, 186	eqtri 2483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
188		eqeq1 2465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
189		unieq 4219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
190	189	fveq2d 5891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
191	190	fveq2d 5891	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
192	177, 191	ifbieq2d 3917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
193	188, 192	ifbieq2d 3917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
194	187, 193, 191	3eqtr4a 2521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
195	194	rexlimivw 2887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
196	195	eqeq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
197	196	biimprd 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
198	197	adantld 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
199	174, 182, 198	3syld 57	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
200		rexex 2855	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
201	196	biimpd 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
202		olc 390	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$
203	202	olcd 399	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
204	200, 201, 203	syl6an 552	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
205	199, 204	impbid 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$ $/\$ $\/$ $/\$
206	143	con2i 125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
207	206	intnanrd 933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
208	207, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
209	178	exlimiv 1786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
210	209	con2i 125	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
211	210	intnanrd 933	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
212		orel2 389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$ $/\$
213	211, 212	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$
214	206	iffalsed 3903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
215		iftrue 3898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
216	214, 215	eqtrd 2495	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
217	216	eqeq2d 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
218	217	biimprd 231	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
219	218	adantld 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
220	208, 213, 219	3syld 57	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$
221	220	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
222	217	biimpd 212	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
223	222	anc2li 564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
224		orc 391	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$
225	224	olcd 399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
226	223, 225	syl6 34	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$
227	226	adantl 472	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
228	221, 227	impbid 195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
229	167, 205, 228	3jaoi 1340	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
230	140, 229	sylbi 200	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$ $/\$ $\/$ $/\$
231	139, 230	syl5bb 265	. . . . . . . . . . . . . . . . . . . . . . 23 Img FullFun Apply pprod Succ
232	55, 231	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Img FullFun Apply pprod Succ
233	27, 67	brcnv 5035	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply Apply
234	12, 41, 27	brapply 30753	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply
235	233, 234	bitri 257	. . . . . . . . . . . . . . . . . . . . . . 23 Apply
236	235	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Apply
237	232, 236	anbi12d 722	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
238		ancom 456	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
239	237, 238	syl6bb 269	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
240	239	exbidv 1778	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
241		df-br 4416	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
242	67	elfix 30718	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
243	67, 67	brco 5023	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Img FullFun Apply pprod Succ $/\$ Apply
244	241, 242, 243	3bitri 279	. . . . . . . . . . . . . . . . . . 19 Apply Img FullFun Apply pprod Succ Img FullFun Apply pprod Succ $/\$ Apply
245		fvex 5897	. . . . . . . . . . . . . . . . . . . 20
246	245	eqvinc 3177	. . . . . . . . . . . . . . . . . . 19 $/\$
247	240, 244, 246	3bitr4g 296	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
248	247	notbid 300	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
249	248	3expia 1217	. . . . . . . . . . . . . . . 16 $/\$ Apply Img FullFun Apply pprod Succ
250	249	pm5.32d 649	. . . . . . . . . . . . . . 15 $/\$ $/\$ Apply Img FullFun Apply pprod Succ $/\$
251		annim 431	. . . . . . . . . . . . . . 15 $/\$
252	250, 251	syl6bb 269	. . . . . . . . . . . . . 14 $/\$ $/\$ Apply Img FullFun Apply pprod Succ
253	53, 252	syl5bb 265	. . . . . . . . . . . . 13 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
254	253	exbidv 1778	. . . . . . . . . . . 12 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
255		exnal 1709	. . . . . . . . . . . 12
256	254, 255	syl6rbb 270	. . . . . . . . . . 11 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
257	12	eldm 5050	. . . . . . . . . . 11 Domain $\$ Apply Img FullFun Apply pprod Succ Domain $\$ Apply Img FullFun Apply pprod Succ
258	256, 257	syl6bbr 271	. . . . . . . . . 10 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
259	258	con1bid 336	. . . . . . . . 9 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
260		df-ral 2753	. . . . . . . . 9
261	259, 260	syl6bbr 271	. . . . . . . 8 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
262	261	pm5.32i 647	. . . . . . 7 $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
263		anass 659	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
264	262, 263	bitri 257	. . . . . 6 $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
265	21, 39, 264	3bitri 279	. . . . 5 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
266	19, 20, 265	3bitr4ri 286	. . . 4 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
267	266	abbi2i 2576	. . 3 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
268	267	unieqi 4220	. 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 189 $\/$ wo 374 $/\$ wa 375 $\/$ w3o 990 $/\$ w3a 991

wal 1452

wceq 1454

wex 1673

wcel 1897

cab 2447

wne 2632

wral 2748

wrex 2749

cvv 3056 $\$ cdif 3412

cun 3413

cin 3414

c0 3742

cif 3892

csn 3979

cop 3985

cuni 4211 class class class wbr 4415

cep 4761

cid 4762

cxp 4850

ccnv 4851

cdm 4852

crn 4853

cres 4854

cima 4855

ccom 4856

con0 5441

wlim 5442

csuc 5443

wfun 5594

wfn 5595

cfv 5600

crdg 7152 pprodcpprod 30645

cbigcup 30648

cfix 30649

climits 30650

cfuns 30651 Imgcimg 30656 Domaincdomain 30657 Applycapply 30659 Succcsuccf 30662 FullFuncfullfn 30664

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-8 1899 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-rep 4528 ax-sep 4538 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6609

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-reu 2755 df-rab 2757 df-v 3058 df-sbc 3279 df-csb 3375 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-pss 3431 df-symdif 3674 df-nul 3743 df-if 3893 df-pw 3964 df-sn 3980 df-pr 3982 df-tp 3984 df-op 3986 df-uni 4212 df-iun 4293 df-br 4416 df-opab 4475 df-mpt 4476 df-tr 4511 df-eprel 4763 df-id 4767 df-po 4773 df-so 4774 df-fr 4811 df-we 4813 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-pred 5398 df-ord 5444 df-on 5445 df-lim 5446 df-suc 5447 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-f1 5605 df-fo 5606 df-f1o 5607 df-fv 5608 df-om 6719 df-1st 6819 df-2nd 6820 df-wrecs 7053 df-recs 7115 df-rdg 7153 df-txp 30668 df-pprod 30669 df-bigcup 30672 df-fix 30673 df-limits 30674 df-funs 30675 df-singleton 30676 df-singles 30677 df-image 30678 df-cart 30679 df-img 30680 df-domain 30681 df-cup 30683 df-succf 30686 df-apply 30687 df-funpart 30688 df-fullfun 30689

This theorem is referenced by: (None)

W3C validator