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 29453

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 29082	. 2 $/\$
2		an12 795	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
3		df-fn 5591	. . . . . . . . . 10 $/\$
4		ancom 450	. . . . . . . . . 10 $/\$ $/\$
5		eqcom 2476	. . . . . . . . . . 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 1644	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
12		vex 3116	. . . . . . . 8
13	12	dmex 6718	. . . . . . 7
14		eleq1 2539	. . . . . . . . 9
15		raleq 3058	. . . . . . . . 9
16	14, 15	anbi12d 710	. . . . . . . 8 $/\$ $/\$
17	16	anbi2d 703	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
18	13, 17	ceqsexv 3150	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
19	11, 18	bitri 249	. . . . 5 $/\$ $/\$ $/\$ $/\$
20		df-rex 2820	. . . . 5 $/\$ $/\$ $/\$
21		eldif 3486	. . . . . 6 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
22		elin 3687	. . . . . . . 8 Domain $/\$ Domain
23	12	elfuns 29418	. . . . . . . . 9
24	12	elima 5342	. . . . . . . . . 10 Domain Domain
25		df-rex 2820	. . . . . . . . . 10 Domain $/\$ Domain
26		ancom 450	. . . . . . . . . . . . 13 $/\$ Domain Domain $/\$
27		vex 3116	. . . . . . . . . . . . . . . 16
28	27, 12	brcnv 5185	. . . . . . . . . . . . . . 15 Domain Domain
29	12, 27	brdomain 29436	. . . . . . . . . . . . . . 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 1644	. . . . . . . . . . 11 $/\$ Domain $/\$
34	13, 14	ceqsexv 3150	. . . . . . . . . . 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 4497	. . . . . . . . . . . . . . 15 Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Apply Img FullFun Apply pprod Succ
41		vex 3116	. . . . . . . . . . . . . . . . . 18
42	12, 41	brco 5173	. . . . . . . . . . . . . . . . 17 Domain Domain $/\$
43	29	anbi1i 695	. . . . . . . . . . . . . . . . . . 19 Domain $/\$ $/\$
44	43	exbii 1644	. . . . . . . . . . . . . . . . . 18 Domain $/\$ $/\$
45		breq1 4450	. . . . . . . . . . . . . . . . . . 19
46	13, 45	ceqsexv 3150	. . . . . . . . . . . . . . . . . 18 $/\$
47	44, 46	bitri 249	. . . . . . . . . . . . . . . . 17 Domain $/\$
48	13, 41	brcnv 5185	. . . . . . . . . . . . . . . . . 18
49	13	epelc 4793	. . . . . . . . . . . . . . . . . 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 4903	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
55	54	3adant1 1014	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
56		brun 4495	. . . . . . . . . . . . . . . . . . . . . . . . 25 Img FullFun Apply pprod Succ $\/$ Img FullFun Apply pprod Succ
57		brxp 5030	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
58		opelxp 5029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
59	12, 58	mpbiran 916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		elsn 4041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62		elsn 4041	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
63	61, 62	anbi12i 697	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
64	57, 63	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
65		brun 4495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img FullFun Apply pprod Succ Img $\/$ FullFun Apply pprod Succ
66	27	brres 5280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img Img $/\$
67		opex 4711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
68	67, 27	brco 5173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img Img $/\$
69		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
70	12, 41, 69	brimg 29440	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Img
71	27	brbigcup 29401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	70, 71	anbi12i 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Img $/\$ $/\$
73	72	exbii 1644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img $/\$ $/\$
74		imaexg 6722	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
75	12, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
76		unieq 4253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77	76	eqeq1d 2469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
78	75, 77	ceqsexv 3150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
79		eqcom 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
80	78, 79	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
81	68, 73, 80	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Img
82		opelxp 5029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
83	12, 82	mpbiran 916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
84	41	ellimits 29413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
85	83, 84	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
86	81, 85	anbi12ci 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img $/\$ $/\$
87	66, 86	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Img $/\$
88	27	brres 5280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod Succ FullFun Apply pprod $/\$ Succ
89	67, 27	brco 5173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 FullFun Apply pprod Apply pprod $/\$ FullFun
90		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
91	67, 90	brco 5173	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Apply pprod pprod $/\$ Apply
92	12, 41, 69	brpprod3a 29389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 pprod $/\$ $/\$
93		3anrot 978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
94	90	ideq 5155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
95		equcom 1743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
96	94, 95	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
97		vex 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
98	97	brbigcup 29401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
99		eqcom 2476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
100	98, 99	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
101		biid 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
102	96, 100, 101	3anbi123i 1185	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
103	93, 102	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$
104	103	2exbii 1645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
105	41	uniex 6581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
106		opeq1 4213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
107	106	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
108		opeq2 4214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
109	108	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
110	12, 105, 107, 109	ceqsex2v 3152	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
111	92, 104, 110	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 pprod
112	111	anbi1i 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 pprod $/\$ Apply $/\$ Apply
113	112	exbii 1644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 pprod $/\$ Apply $/\$ Apply
114		opex 4711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
115		breq1 4450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Apply Apply
116	114, 115	ceqsexv 3150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ Apply Apply
117	12, 105, 90	brapply 29441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Apply
118	116, 117	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ Apply
119	91, 113, 118	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Apply pprod
120	90, 27	brfullfun 29451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 FullFun
121	119, 120	anbi12i 697	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Apply pprod $/\$ FullFun $/\$
122	121	exbii 1644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Apply pprod $/\$ FullFun $/\$
123		fvex 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
124		fveq2 5866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
125	124	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
126	123, 125	ceqsexv 3150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
127	89, 122, 126	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 FullFun Apply pprod
128		opelxp 5029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ $/\$ Succ
129	12, 128	mpbiran 916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
130	41	elrn 5243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
131	69, 41	brsuccf 29444	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ
132	131	exbii 1644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6666	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$ $/\$
141		nlim0 4936	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
142		limeq 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
143	141, 142	mtbiri 303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
144	143	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
145		nsuceq0 4958	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
146		neeq2 2750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
147	145, 146	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
148	147	necomd 2738	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
149	148	neneqd 2669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
150	149	nexdv 1832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
151	150	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
152		ioran 490	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
153	144, 151, 152	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$
154		orel2 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
155	153, 154	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
156		iftrue 3945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
157		unisnif 29428	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
158	156, 157	syl6eqr 2526	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
159	158	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
169	145, 168	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
170	169	neneqd 2669	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
171	170	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
172	171	rexlimivw 2952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
173		orel1 382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
174	172, 173	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
175		nlimsucg 6662	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
176	69, 175	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177		limeq 4890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178	176, 177	mtbiri 303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179	178	rexlimivw 2952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180	179	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
181		orel1 382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $/\$
182	180, 181	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $/\$
183		df-ne 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
184	145, 183	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
185	184	iffalsei 3949	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
186		iffalse 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
187	69, 175, 186	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
188	185, 187	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
189		eqeq1 2471	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
190		unieq 4253	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
191	190	fveq2d 5870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
192	191	fveq2d 5870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
193	177, 192	ifbieq2d 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
194	189, 193	ifbieq2d 3964	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
195	188, 194, 192	3eqtr4a 2534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
196	195	rexlimivw 2952	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
197	196	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
198	197	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
199	198	adantld 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
200	174, 182, 199	3syld 55	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
201		rexex 2921	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
209	208, 173	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
210	178	exlimiv 1698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	210	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212	211	intnanrd 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
213		orel2 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$ $/\$
214	212, 213	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$
215		iffalse 3948	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
216	207, 215	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
217		iftrue 3945	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
218	216, 217	eqtrd 2508	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
219	218	eqeq2d 2481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1291	. . . . . . . . . . . . . . . . . . . . . . . . 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 5185	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply Apply
236	12, 41, 27	brapply 29441	. . . . . . . . . . . . . . . . . . . . . . . 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 1690	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
243		df-br 4448	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
244	67	elfix 29406	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
245	67, 67	brco 5173	. . . . . . . . . . . . . . . . . . . 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 5876	. . . . . . . . . . . . . . . . . . . 20
248	247	eqvinc 3230	. . . . . . . . . . . . . . . . . . 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 1198	. . . . . . . . . . . . . . . 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 1690	. . . . . . . . . . . 12 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
257		exnal 1628	. . . . . . . . . . . 12
258	256, 257	syl6rbb 262	. . . . . . . . . . 11 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
259	12	eldm 5200	. . . . . . . . . . 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 2819	. . . . . . . . 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 2600	. . 3 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
270	269	unieqi 4254	. 2 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
271	1, 270	eqtr4i 2499	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 972 $/\$ w3a 973

wal 1377

wceq 1379

wex 1596

wcel 1767

cab 2452

wne 2662

wral 2814

wrex 2815

cvv 3113 $\$ cdif 3473

cun 3474

cin 3475

c0 3785

cif 3939

csn 4027

cop 4033

cuni 4245 class class class wbr 4447

cep 4789

cid 4790

con0 4878

wlim 4879

csuc 4880

cxp 4997

ccnv 4998

cdm 4999

crn 5000

cres 5001

cima 5002

ccom 5003

wfun 5582

wfn 5583

cfv 5588

crdg 7076 pprodcpprod 29333

cbigcup 29336

cfix 29337

climits 29338

cfuns 29339 Imgcimg 29344 Domaincdomain 29345 Applycapply 29347 Succcsuccf 29350 FullFuncfullfn 29352

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6577

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-reu 2821 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5551 df-fun 5590 df-fn 5591 df-f 5592 df-f1 5593 df-fo 5594 df-f1o 5595 df-fv 5596 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7043 df-rdg 7077 df-symdif 29321 df-txp 29356 df-pprod 29357 df-bigcup 29360 df-fix 29361 df-limits 29362 df-funs 29363 df-singleton 29364 df-singles 29365 df-image 29366 df-cart 29367 df-img 29368 df-domain 29369 df-cup 29371 df-succf 29374 df-apply 29375 df-funpart 29376 df-fullfun 29377

This theorem is referenced by: (None)

W3C validator