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 27910

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 27539	. 2 $/\$
2		an12 790	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
3		df-fn 5418	. . . . . . . . . 10 $/\$
4		ancom 448	. . . . . . . . . 10 $/\$ $/\$
5		eqcom 2443	. . . . . . . . . . 11
6	5	anbi1i 690	. . . . . . . . . 10 $/\$ $/\$
7	3, 4, 6	3bitri 271	. . . . . . . . 9 $/\$
8	7	anbi1i 690	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
9		anass 644	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10	2, 8, 9	3bitri 271	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
11	10	exbii 1639	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
12		vex 2973	. . . . . . . 8
13	12	dmex 6510	. . . . . . 7
14		eleq1 2501	. . . . . . . . 9
15		raleq 2915	. . . . . . . . 9
16	14, 15	anbi12d 705	. . . . . . . 8 $/\$ $/\$
17	16	anbi2d 698	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
18	13, 17	ceqsexv 3006	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
19	11, 18	bitri 249	. . . . 5 $/\$ $/\$ $/\$ $/\$
20		df-rex 2719	. . . . 5 $/\$ $/\$ $/\$
21		eldif 3335	. . . . . 6 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
22		elin 3536	. . . . . . . 8 Domain $/\$ Domain
23	12	elfuns 27875	. . . . . . . . 9
24	12	elima 5171	. . . . . . . . . 10 Domain Domain
25		df-rex 2719	. . . . . . . . . 10 Domain $/\$ Domain
26		ancom 448	. . . . . . . . . . . . 13 $/\$ Domain Domain $/\$
27		vex 2973	. . . . . . . . . . . . . . . 16
28	27, 12	brcnv 5018	. . . . . . . . . . . . . . 15 Domain Domain
29	12, 27	brdomain 27893	. . . . . . . . . . . . . . 15 Domain
30	28, 29	bitri 249	. . . . . . . . . . . . . 14 Domain
31	30	anbi1i 690	. . . . . . . . . . . . 13 Domain $/\$ $/\$
32	26, 31	bitri 249	. . . . . . . . . . . 12 $/\$ Domain $/\$
33	32	exbii 1639	. . . . . . . . . . 11 $/\$ Domain $/\$
34	13, 14	ceqsexv 3006	. . . . . . . . . . 11 $/\$
35	33, 34	bitri 249	. . . . . . . . . 10 $/\$ Domain
36	24, 25, 35	3bitri 271	. . . . . . . . 9 Domain
37	23, 36	anbi12i 692	. . . . . . . 8 $/\$ Domain $/\$
38	22, 37	bitri 249	. . . . . . 7 Domain $/\$
39	38	anbi1i 690	. . . . . 6 Domain $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
40		brdif 4339	. . . . . . . . . . . . . . 15 Domain $\$ Apply Img FullFun Apply pprod Succ Domain $/\$ Apply Img FullFun Apply pprod Succ
41		vex 2973	. . . . . . . . . . . . . . . . . 18
42	12, 41	brco 5006	. . . . . . . . . . . . . . . . 17 Domain Domain $/\$
43	29	anbi1i 690	. . . . . . . . . . . . . . . . . . 19 Domain $/\$ $/\$
44	43	exbii 1639	. . . . . . . . . . . . . . . . . 18 Domain $/\$ $/\$
45		breq1 4292	. . . . . . . . . . . . . . . . . . 19
46	13, 45	ceqsexv 3006	. . . . . . . . . . . . . . . . . 18 $/\$
47	44, 46	bitri 249	. . . . . . . . . . . . . . . . 17 Domain $/\$
48	13, 41	brcnv 5018	. . . . . . . . . . . . . . . . . 18
49	13	epelc 4630	. . . . . . . . . . . . . . . . . 18
50	48, 49	bitri 249	. . . . . . . . . . . . . . . . 17
51	42, 47, 50	3bitri 271	. . . . . . . . . . . . . . . 16 Domain
52	51	anbi1i 690	. . . . . . . . . . . . . . 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 4740	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
55	54	3adant1 1001	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
56		brun 4337	. . . . . . . . . . . . . . . . . . . . . . . . 25 Img FullFun Apply pprod Succ $\/$ Img FullFun Apply pprod Succ
57		brxp 4866	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
58		opelxp 4865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
59	12, 58	mpbiran 904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
60		elsn 3888	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
61	59, 60	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
62		elsn 3888	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
63	61, 62	anbi12i 692	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
64	57, 63	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
65		brun 4337	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img FullFun Apply pprod Succ Img $\/$ FullFun Apply pprod Succ
66	27	brres 5113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img Img $/\$
67		opex 4553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
68	67, 27	brco 5006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img Img $/\$
69		vex 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
70	12, 41, 69	brimg 27897	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Img
71	27	brbigcup 27858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
72	70, 71	anbi12i 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Img $/\$ $/\$
73	72	exbii 1639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Img $/\$ $/\$
74		imaexg 6514	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
75	12, 74	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
76		unieq 4096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
77	76	eqeq1d 2449	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
78	75, 77	ceqsexv 3006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
79		eqcom 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
80	78, 79	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
81	68, 73, 80	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Img
82		opelxp 4865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
83	12, 82	mpbiran 904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
84	41	ellimits 27870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
85	83, 84	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
86	81, 85	anbi12ci 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 Img $/\$ $/\$
87	66, 86	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Img $/\$
88	27	brres 5113	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod Succ FullFun Apply pprod $/\$ Succ
89	67, 27	brco 5006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 FullFun Apply pprod Apply pprod $/\$ FullFun
90		vex 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
91	67, 90	brco 5006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 Apply pprod pprod $/\$ Apply
92	12, 41, 69	brpprod3a 27846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 pprod $/\$ $/\$
93		3anrot 965	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
94	90	ideq 4988	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
95		equcom 1737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
96	94, 95	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
97		vex 2973	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
98	97	brbigcup 27858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
99		eqcom 2443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
100	98, 99	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
101		biid 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
102	96, 100, 101	3anbi123i 1171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$
103	93, 102	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$
104	103	2exbii 1640	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$
105	41	uniex 6375	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
106		opeq1 4056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
107	106	eqeq2d 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
108		opeq2 4057	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39
109	108	eqeq2d 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
110	12, 105, 107, 109	ceqsex2v 3008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
111	92, 104, 110	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 pprod
112	111	anbi1i 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 pprod $/\$ Apply $/\$ Apply
113	112	exbii 1639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 pprod $/\$ Apply $/\$ Apply
114		opex 4553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
115		breq1 4292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 Apply Apply
116	114, 115	ceqsexv 3006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ Apply Apply
117	12, 105, 90	brapply 27898	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 Apply
118	116, 117	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ Apply
119	91, 113, 118	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Apply pprod
120	90, 27	brfullfun 27908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 FullFun
121	119, 120	anbi12i 692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Apply pprod $/\$ FullFun $/\$
122	121	exbii 1639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Apply pprod $/\$ FullFun $/\$
123		fvex 5698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
124		fveq2 5688	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
125	124	eqeq2d 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
126	123, 125	ceqsexv 3006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
127	89, 122, 126	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 FullFun Apply pprod
128		opelxp 4865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ $/\$ Succ
129	12, 128	mpbiran 904	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
130	41	elrn 5076	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ Succ
131	69, 41	brsuccf 27901	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 Succ
132	131	exbii 1639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 Succ
133	129, 130, 132	3bitri 271	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 Succ
134	127, 133	anbi12ci 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 FullFun Apply pprod $/\$ Succ $/\$
135	88, 134	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 FullFun Apply pprod Succ $/\$
136	87, 135	orbi12i 518	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 Img $\/$ FullFun Apply pprod Succ $/\$ $\/$ $/\$
137	65, 136	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Img FullFun Apply pprod Succ $/\$ $\/$ $/\$
138	64, 137	orbi12i 518	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ Img FullFun Apply pprod Succ $/\$ $\/$ $/\$ $\/$ $/\$
139	56, 138	bitri 249	. . . . . . . . . . . . . . . . . . . . . . . 24 Img FullFun Apply pprod Succ $/\$ $\/$ $/\$ $\/$ $/\$
140		onzsl 6456	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$ $\/$ $/\$
141		nlim0 4773	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
142		limeq 4727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
143	141, 142	mtbiri 303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
144	143	intnanrd 903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
145		nsuceq0 4795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
146		neeq2 2615	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
147	145, 146	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
148	147	necomd 2693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
149	148	neneqd 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
150	149	nexdv 1939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
151	150	intnanrd 903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
152		ioran 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $\/$ $/\$ $/\$ $/\$ $/\$
153	144, 151, 152	sylanbrc 659	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$
154		orel2 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
155	153, 154	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$
156		iftrue 3794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
157		unisnif 27885	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
158	156, 157	syl6eqr 2491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
159	158	eqeq2d 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
160	159	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
161	160	adantld 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
162	155, 161	syld 44	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
163	159	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
164	163	anc2li 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
165		orc 385	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
166	164, 165	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
167	162, 166	impbid 191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$ $/\$ $\/$ $/\$
168		neeq1 2614	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
169	145, 168	mpbiri 233	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
170	169	neneqd 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
171	170	intnanrd 903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
172	171	rexlimivw 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
173		orel1 382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
174	172, 173	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
175		nlimsucg 6452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
176	69, 175	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177		limeq 4727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
178	176, 177	mtbiri 303	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
179	178	rexlimivw 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
180	179	intnanrd 903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
181		orel1 382	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $/\$
182	180, 181	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $/\$
183		df-ne 2606	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
184	145, 183	mpbi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
185	184	iffalsei 3797	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
186		iffalse 3796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
187	69, 175, 186	mp2b 10	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
188	185, 187	eqtri 2461	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
189		eqeq1 2447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
190		unieq 4096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
191	190	fveq2d 5692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
192	191	fveq2d 5692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
193	177, 192	ifbieq2d 3811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
194	189, 193	ifbieq2d 3811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
195	188, 194, 192	3eqtr4a 2499	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
196	195	rexlimivw 2835	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
197	196	eqeq2d 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
198	197	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
199	198	adantld 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
200	174, 182, 199	3syld 55	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
201		rexex 2773	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
202	197	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
203		olc 384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$
204	203	olcd 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
205	201, 202, 204	syl6an 542	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $\/$ $/\$ $\/$ $/\$
206	200, 205	impbid 191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$ $/\$ $\/$ $/\$
207	143	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
208	207	intnanrd 903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
209	208, 173	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
210	178	exlimiv 1693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
211	210	con2i 120	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
212	211	intnanrd 903	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
213		orel2 383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$ $/\$
214	212, 213	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $\/$ $/\$ $/\$
215		iffalse 3796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
216	207, 215	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
217		iftrue 3794	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
218	216, 217	eqtrd 2473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
219	218	eqeq2d 2452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
220	219	biimprd 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
221	220	adantld 464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
222	209, 214, 221	3syld 55	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$
223	222	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
224	219	biimpd 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
225	224	anc2li 554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
226		orc 385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $\/$ $/\$
227	226	olcd 393	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
228	225, 227	syl6 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $\/$ $/\$ $\/$ $/\$
229	228	adantl 463	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
230	223, 229	impbid 191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
231	167, 206, 230	3jaoi 1276	. . . . . . . . . . . . . . . . . . . . . . . . 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 5018	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply Apply
236	12, 41, 27	brapply 27898	. . . . . . . . . . . . . . . . . . . . . . . 24 Apply
237	235, 236	bitri 249	. . . . . . . . . . . . . . . . . . . . . . 23 Apply
238	237	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ Apply
239	234, 238	anbi12d 705	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
240		ancom 448	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
241	239, 240	syl6bb 261	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
242	241	exbidv 1685	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ Img FullFun Apply pprod Succ $/\$ Apply $/\$
243		df-br 4290	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
244	67	elfix 27863	. . . . . . . . . . . . . . . . . . . 20 Apply Img FullFun Apply pprod Succ Apply Img FullFun Apply pprod Succ
245	67, 67	brco 5006	. . . . . . . . . . . . . . . . . . . 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 5698	. . . . . . . . . . . . . . . . . . . 20
248	247	eqvinc 3083	. . . . . . . . . . . . . . . . . . 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 1184	. . . . . . . . . . . . . . . 16 $/\$ Apply Img FullFun Apply pprod Succ
252	251	pm5.32d 634	. . . . . . . . . . . . . . 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 1685	. . . . . . . . . . . 12 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
257		exnal 1623	. . . . . . . . . . . 12
258	256, 257	syl6rbb 262	. . . . . . . . . . 11 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
259	12	eldm 5033	. . . . . . . . . . 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 2718	. . . . . . . . 9
263	261, 262	syl6bbr 263	. . . . . . . 8 $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ
264	263	pm5.32i 632	. . . . . . 7 $/\$ $/\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$ $/\$
265		anass 644	. . . . . . 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 2552	. . 3 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
270	269	unieqi 4097	. 2 Domain $\$ Domain $\$ Apply Img FullFun Apply pprod Succ $/\$
271	1, 270	eqtr4i 2464	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 959 $/\$ w3a 960

wal 1362

wceq 1364

wex 1591

wcel 1761

cab 2427

wne 2604

wral 2713

wrex 2714

cvv 2970 $\$ cdif 3322

cun 3323

cin 3324

c0 3634

cif 3788

csn 3874

cop 3880

cuni 4088 class class class wbr 4289

cep 4626

cid 4627

con0 4715

wlim 4716

csuc 4717

cxp 4834

ccnv 4835

cdm 4836

crn 4837

cres 4838

cima 4839

ccom 4840

wfun 5409

wfn 5410

cfv 5415

crdg 6861 pprodcpprod 27790

cbigcup 27793

cfix 27794

climits 27795

cfuns 27796 Imgcimg 27801 Domaincdomain 27802 Applycapply 27804 Succcsuccf 27807 FullFuncfullfn 27809

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-ral 2718 df-rex 2719 df-reu 2720 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-symdif 27778 df-txp 27813 df-pprod 27814 df-bigcup 27817 df-fix 27818 df-limits 27819 df-funs 27820 df-singleton 27821 df-singles 27822 df-image 27823 df-cart 27824 df-img 27825 df-domain 27826 df-cup 27828 df-succf 27831 df-apply 27832 df-funpart 27833 df-fullfun 27834

This theorem is referenced by: (None)

W3C validator