axdc3lem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > axdc3lem2		Structured version Visualization version Unicode version

Theorem axdc3lem2 9273

Description: Lemma for axdc3 9276. We have constructed a "candidate set"

, which consists of all finite sequences

that satisfy our property of interest, namely

on its domain, but with the added constraint that

. These sets are possible "initial segments" of the infinite sequence satisfying these constraints, but we can leverage the standard ax-dc 9268 (with no initial condition) to select a sequence of ever-lengthening finite sequences, namely

(for some integer

). We let our "choice" function select a sequence whose domain is one more than the last one, and agrees with the previous one on its domain. Thus, the application of vanilla ax-dc 9268 yields a sequence of sequences whose domains increase without bound, and whose union is a function which has all the properties we want. In this lemma, we show that given the sequence

, we can construct the sequence

that we are after. (Contributed by Mario Carneiro, 30-Jan-2013.)

**Hypotheses**
Ref	Expression
axdc3lem2.1
axdc3lem2.2	$/\$ $/\$
axdc3lem2.3	$/\$

**Assertion**
Ref	Expression
axdc3lem2	$/\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

Proof of Theorem axdc3lem2 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. . . . . . . . . . . . 13
2		fveq2 6191	. . . . . . . . . . . . . 14
3	2	dmeqd 5326	. . . . . . . . . . . . 13
4	1, 3	eleq12d 2695	. . . . . . . . . . . 12
5		eleq2 2690	. . . . . . . . . . . . 13
6	2	sseq2d 3633	. . . . . . . . . . . . 13
7	5, 6	imbi12d 334	. . . . . . . . . . . 12
8	4, 7	anbi12d 747	. . . . . . . . . . 11 $/\$ $/\$
9		id 22	. . . . . . . . . . . . 13
10		fveq2 6191	. . . . . . . . . . . . . 14
11	10	dmeqd 5326	. . . . . . . . . . . . 13
12	9, 11	eleq12d 2695	. . . . . . . . . . . 12
13		elequ2 2004	. . . . . . . . . . . . 13
14	10	sseq2d 3633	. . . . . . . . . . . . 13
15	13, 14	imbi12d 334	. . . . . . . . . . . 12
16	12, 15	anbi12d 747	. . . . . . . . . . 11 $/\$ $/\$
17		id 22	. . . . . . . . . . . . 13
18		fveq2 6191	. . . . . . . . . . . . . 14
19	18	dmeqd 5326	. . . . . . . . . . . . 13
20	17, 19	eleq12d 2695	. . . . . . . . . . . 12
21		eleq2 2690	. . . . . . . . . . . . 13
22	18	sseq2d 3633	. . . . . . . . . . . . 13
23	21, 22	imbi12d 334	. . . . . . . . . . . 12
24	20, 23	anbi12d 747	. . . . . . . . . . 11 $/\$ $/\$
25		peano1 7085	. . . . . . . . . . . . . . 15
26		ffvelrn 6357	. . . . . . . . . . . . . . 15 $/\$
27	25, 26	mpan2 707	. . . . . . . . . . . . . 14
28		axdc3lem2.2	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
29		fdm 6051	. . . . . . . . . . . . . . . . . . . . . . 23
30		nnord 7073	. . . . . . . . . . . . . . . . . . . . . . . . 25
31		0elsuc 7035	. . . . . . . . . . . . . . . . . . . . . . . . 25
32	30, 31	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24
33		peano2 7086	. . . . . . . . . . . . . . . . . . . . . . . 24
34		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . 26
35		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . 26
36	34, 35	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
37	36	biimprcd 240	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
38	32, 33, 37	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
39	29, 38	syl5com 31	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
40	39	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
41	40	impcom 446	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
42	41	rexlimiva 3028	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
43	42	ss2abi 3674	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
44	28, 43	eqsstri 3635	. . . . . . . . . . . . . . . . 17 $/\$
45	44	sseli 3599	. . . . . . . . . . . . . . . 16 $/\$
46		fvex 6201	. . . . . . . . . . . . . . . . 17
47		dmeq 5324	. . . . . . . . . . . . . . . . . . 19
48	47	eleq2d 2687	. . . . . . . . . . . . . . . . . 18
49	47	eleq1d 2686	. . . . . . . . . . . . . . . . . 18
50	48, 49	anbi12d 747	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
51	46, 50	elab 3350	. . . . . . . . . . . . . . . 16 $/\$ $/\$
52	45, 51	sylib 208	. . . . . . . . . . . . . . 15 $/\$
53	52	simpld 475	. . . . . . . . . . . . . 14
54	27, 53	syl 17	. . . . . . . . . . . . 13
55		noel 3919	. . . . . . . . . . . . . 14
56	55	pm2.21i 116	. . . . . . . . . . . . 13
57	54, 56	jctir 561	. . . . . . . . . . . 12 $/\$
58	57	adantr 481	. . . . . . . . . . 11 $/\$ $/\$
59		ffvelrn 6357	. . . . . . . . . . . . . . 15 $/\$
60	59	ancoms 469	. . . . . . . . . . . . . 14 $/\$
61	60	adantrr 753	. . . . . . . . . . . . 13 $/\$ $/\$
62		suceq 5790	. . . . . . . . . . . . . . . . 17
63	62	fveq2d 6195	. . . . . . . . . . . . . . . 16
64		fveq2 6191	. . . . . . . . . . . . . . . . 17
65	64	fveq2d 6195	. . . . . . . . . . . . . . . 16
66	63, 65	eleq12d 2695	. . . . . . . . . . . . . . 15
67	66	rspcva 3307	. . . . . . . . . . . . . 14 $/\$
68	67	adantrl 752	. . . . . . . . . . . . 13 $/\$ $/\$
69	44	sseli 3599	. . . . . . . . . . . . . . . . . . . 20 $/\$
70		fvex 6201	. . . . . . . . . . . . . . . . . . . . 21
71		dmeq 5324	. . . . . . . . . . . . . . . . . . . . . . 23
72	71	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . 22
73	71	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . 22
74	72, 73	anbi12d 747	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
75	70, 74	elab 3350	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
76	69, 75	sylib 208	. . . . . . . . . . . . . . . . . . 19 $/\$
77	76	simprd 479	. . . . . . . . . . . . . . . . . 18
78		nnord 7073	. . . . . . . . . . . . . . . . . 18
79		ordsucelsuc 7022	. . . . . . . . . . . . . . . . . 18
80	77, 78, 79	3syl 18	. . . . . . . . . . . . . . . . 17
81	80	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
82		dmeq 5324	. . . . . . . . . . . . . . . . . . . . . . . . . 26
83		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . . . . 26
84	82, 83	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
85	84	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . 24
86	82	reseq2d 5396	. . . . . . . . . . . . . . . . . . . . . . . . 25
87		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25
88	86, 87	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . 24
89	85, 88	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
90	89	rabbidv 3189	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
91		axdc3lem2.3	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
92		axdc3lem2.1	. . . . . . . . . . . . . . . . . . . . . . . 24
93	92, 28	axdc3lem 9272	. . . . . . . . . . . . . . . . . . . . . . 23
94	93	rabex 4813	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
95	90, 91, 94	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . 21 $/\$
96	95	eleq2d 2687	. . . . . . . . . . . . . . . . . . . 20 $/\$
97		dmeq 5324	. . . . . . . . . . . . . . . . . . . . . . 23
98	97	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . 22
99		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . 23
100	99	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . 22
101	98, 100	anbi12d 747	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
102	101	elrab 3363	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
103	96, 102	syl6bb 276	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
104	103	simplbda 654	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
105	104	simpld 475	. . . . . . . . . . . . . . . . 17 $/\$
106	105	eleq2d 2687	. . . . . . . . . . . . . . . 16 $/\$
107	81, 106	bitr4d 271	. . . . . . . . . . . . . . 15 $/\$
108	107	biimpd 219	. . . . . . . . . . . . . 14 $/\$
109	104	simprd 479	. . . . . . . . . . . . . . 15 $/\$
110		resss 5422	. . . . . . . . . . . . . . . 16
111		sseq1 3626	. . . . . . . . . . . . . . . 16
112	110, 111	mpbii 223	. . . . . . . . . . . . . . 15
113		elsuci 5791	. . . . . . . . . . . . . . . . 17 $\/$
114		pm2.27 42	. . . . . . . . . . . . . . . . . . 19
115		sstr2 3610	. . . . . . . . . . . . . . . . . . 19
116	114, 115	syl6 35	. . . . . . . . . . . . . . . . . 18
117		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21
118	117	sseq1d 3632	. . . . . . . . . . . . . . . . . . . 20
119	118	biimprd 238	. . . . . . . . . . . . . . . . . . 19
120	119	a1d 25	. . . . . . . . . . . . . . . . . 18
121	116, 120	jaoi 394	. . . . . . . . . . . . . . . . 17 $\/$
122	113, 121	syl 17	. . . . . . . . . . . . . . . 16
123	122	com13 88	. . . . . . . . . . . . . . 15
124	109, 112, 123	3syl 18	. . . . . . . . . . . . . 14 $/\$
125	108, 124	anim12d 586	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
126	61, 68, 125	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
127	126	ex 450	. . . . . . . . . . 11 $/\$ $/\$ $/\$
128	8, 16, 24, 58, 127	finds2 7094	. . . . . . . . . 10 $/\$ $/\$
129	128	imp 445	. . . . . . . . 9 $/\$ $/\$ $/\$
130	129	simprd 479	. . . . . . . 8 $/\$ $/\$
131	130	expcom 451	. . . . . . 7 $/\$
132	131	ralrimdv 2968	. . . . . 6 $/\$
133	132	ralrimiv 2965	. . . . 5 $/\$
134		frn 6053	. . . . . . . . . . . 12
135		ffun 6048	. . . . . . . . . . . . . . . 16
136	135	3ad2ant1 1082	. . . . . . . . . . . . . . 15 $/\$ $/\$
137	136	rexlimivw 3029	. . . . . . . . . . . . . 14 $/\$ $/\$
138	137	ss2abi 3674	. . . . . . . . . . . . 13 $/\$ $/\$
139	28, 138	eqsstri 3635	. . . . . . . . . . . 12
140	134, 139	syl6ss 3615	. . . . . . . . . . 11
141	140	sseld 3602	. . . . . . . . . 10
142		vex 3203	. . . . . . . . . . 11
143		funeq 5908	. . . . . . . . . . 11
144	142, 143	elab 3350	. . . . . . . . . 10
145	141, 144	syl6ib 241	. . . . . . . . 9
146	145	adantr 481	. . . . . . . 8 $/\$
147		ffn 6045	. . . . . . . . 9
148		fvelrnb 6243	. . . . . . . . . . . . 13
149		fvelrnb 6243	. . . . . . . . . . . . . . 15
150		nnord 7073	. . . . . . . . . . . . . . . . . . . . . . 23
151		nnord 7073	. . . . . . . . . . . . . . . . . . . . . . 23
152	150, 151	anim12i 590	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
153		ordtri3or 5755	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\/$ $\/$
154		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
155	154	sseq2d 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
156	155	raleqbi1dv 3146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
157	156	rspcv 3305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
158		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
159	158	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
160	159	rspccv 3306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
161	157, 160	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
162	161	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
163	162	3imp 1256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
164	163	orcd 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\/$
165	164	3exp 1264	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\/$
166	165	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
167		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
168		eqimss 3657	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
169	168	orcd 407	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\/$
170	167, 169	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
171	170	2a1d 26	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
172		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
173	172	sseq2d 3633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
174	173	raleqbi1dv 3146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
175	174	rspcv 3305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
176		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
177	176	sseq1d 3632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
178	177	rspccv 3306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
179	175, 178	syl6 35	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
180	179	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
181	180	3imp 1256	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$
182	181	olcd 408	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $\/$
183	182	3exp 1264	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\/$
184	183	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
185	166, 171, 184	3jaoi 1391	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $\/$ $/\$ $\/$
186	153, 185	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$
187	152, 186	mpcom 38	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\/$
188		sseq12 3628	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
189		sseq12 3628	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
190	189	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
191	188, 190	orbi12d 746	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\/$ $\/$
192	191	biimpcd 239	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $/\$ $\/$
193	187, 192	syl6 35	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$
194	193	com23 86	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$
195	194	exp4b 632	. . . . . . . . . . . . . . . . . 18 $\/$
196	195	com23 86	. . . . . . . . . . . . . . . . 17 $\/$
197	196	rexlimiv 3027	. . . . . . . . . . . . . . . 16 $\/$
198	197	rexlimdv 3030	. . . . . . . . . . . . . . 15 $\/$
199	149, 198	syl6bi 243	. . . . . . . . . . . . . 14 $\/$
200	199	com23 86	. . . . . . . . . . . . 13 $\/$
201	148, 200	sylbid 230	. . . . . . . . . . . 12 $\/$
202	201	com24 95	. . . . . . . . . . 11 $\/$
203	202	imp 445	. . . . . . . . . 10 $/\$ $\/$
204	203	ralrimdv 2968	. . . . . . . . 9 $/\$ $\/$
205	147, 204	sylan 488	. . . . . . . 8 $/\$ $\/$
206	146, 205	jcad 555	. . . . . . 7 $/\$ $/\$ $\/$
207	206	ralrimiv 2965	. . . . . 6 $/\$ $/\$ $\/$
208		fununi 5964	. . . . . 6 $/\$ $\/$
209	207, 208	syl 17	. . . . 5 $/\$
210	133, 209	syldan 487	. . . 4 $/\$
211		vex 3203	. . . . . . . . 9
212	211	eldm2 5322	. . . . . . . 8
213		eluni2 4440	. . . . . . . . . 10
214	211, 142	opeldm 5328	. . . . . . . . . . . . . . 15
215	214	a1i 11	. . . . . . . . . . . . . 14
216	134, 44	syl6ss 3615	. . . . . . . . . . . . . . 15 $/\$
217		ssel 3597	. . . . . . . . . . . . . . . 16 $/\$ $/\$
218		vex 3203	. . . . . . . . . . . . . . . . . 18
219		dmeq 5324	. . . . . . . . . . . . . . . . . . . 20
220	219	eleq2d 2687	. . . . . . . . . . . . . . . . . . 19
221	219	eleq1d 2686	. . . . . . . . . . . . . . . . . . 19
222	220, 221	anbi12d 747	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
223	218, 222	elab 3350	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
224	223	simprbi 480	. . . . . . . . . . . . . . . 16 $/\$
225	217, 224	syl6 35	. . . . . . . . . . . . . . 15 $/\$
226	216, 225	syl 17	. . . . . . . . . . . . . 14
227	215, 226	anim12d 586	. . . . . . . . . . . . 13 $/\$ $/\$
228		elnn 7075	. . . . . . . . . . . . 13 $/\$
229	227, 228	syl6 35	. . . . . . . . . . . 12 $/\$
230	229	expcomd 454	. . . . . . . . . . 11
231	230	rexlimdv 3030	. . . . . . . . . 10
232	213, 231	syl5bi 232	. . . . . . . . 9
233	232	exlimdv 1861	. . . . . . . 8
234	212, 233	syl5bi 232	. . . . . . 7
235	234	adantr 481	. . . . . 6 $/\$
236		id 22	. . . . . . . . . . 11
237		fnfvelrn 6356	. . . . . . . . . . 11 $/\$
238	147, 236, 237	syl2anr 495	. . . . . . . . . 10 $/\$
239	238	adantrr 753	. . . . . . . . 9 $/\$ $/\$
240	129	simpld 475	. . . . . . . . 9 $/\$ $/\$
241		dmeq 5324	. . . . . . . . . 10
242	241	eliuni 4526	. . . . . . . . 9 $/\$
243	239, 240, 242	syl2anc 693	. . . . . . . 8 $/\$ $/\$
244		dmuni 5334	. . . . . . . 8
245	243, 244	syl6eleqr 2712	. . . . . . 7 $/\$ $/\$
246	245	expcom 451	. . . . . 6 $/\$
247	235, 246	impbid 202	. . . . 5 $/\$
248	247	eqrdv 2620	. . . 4 $/\$
249		rnuni 5544	. . . . . 6
250		frn 6053	. . . . . . . . . . . . . 14
251	250	3ad2ant1 1082	. . . . . . . . . . . . 13 $/\$ $/\$
252	251	rexlimivw 3029	. . . . . . . . . . . 12 $/\$ $/\$
253	252	ss2abi 3674	. . . . . . . . . . 11 $/\$ $/\$
254	28, 253	eqsstri 3635	. . . . . . . . . 10
255	134, 254	syl6ss 3615	. . . . . . . . 9
256		ssel 3597	. . . . . . . . . 10
257		abid 2610	. . . . . . . . . 10
258	256, 257	syl6ib 241	. . . . . . . . 9
259	255, 258	syl 17	. . . . . . . 8
260	259	ralrimiv 2965	. . . . . . 7
261		iunss 4561	. . . . . . 7
262	260, 261	sylibr 224	. . . . . 6
263	249, 262	syl5eqss 3649	. . . . 5
264	263	adantr 481	. . . 4 $/\$
265		df-fn 5891	. . . . 5 $/\$
266		df-f 5892	. . . . . 6 $/\$
267	266	biimpri 218	. . . . 5 $/\$
268	265, 267	sylanbr 490	. . . 4 $/\$ $/\$
269	210, 248, 264, 268	syl21anc 1325	. . 3 $/\$
270		fnfvelrn 6356	. . . . . . . 8 $/\$
271	147, 25, 270	sylancl 694	. . . . . . 7
272	271	adantr 481	. . . . . 6 $/\$
273		elssuni 4467	. . . . . 6
274	272, 273	syl 17	. . . . 5 $/\$
275	54	adantr 481	. . . . 5 $/\$
276		funssfv 6209	. . . . 5 $/\$ $/\$
277	210, 274, 275, 276	syl3anc 1326	. . . 4 $/\$
278		simp2 1062	. . . . . . . . . . 11 $/\$ $/\$
279	278	rexlimivw 3029	. . . . . . . . . 10 $/\$ $/\$
280	279	ss2abi 3674	. . . . . . . . 9 $/\$ $/\$
281	28, 280	eqsstri 3635	. . . . . . . 8
282	134, 281	syl6ss 3615	. . . . . . 7
283		ssel 3597	. . . . . . . 8
284		fveq1 6190	. . . . . . . . . 10
285	284	eqeq1d 2624	. . . . . . . . 9
286	46, 285	elab 3350	. . . . . . . 8
287	283, 286	syl6ib 241	. . . . . . 7
288	282, 287	syl 17	. . . . . 6
289	288	adantr 481	. . . . 5 $/\$
290	272, 289	mpd 15	. . . 4 $/\$
291	277, 290	eqtrd 2656	. . 3 $/\$
292		nfv 1843	. . . . 5
293		nfra1 2941	. . . . 5
294	292, 293	nfan 1828	. . . 4 $/\$
295	134	ad2antrr 762	. . . . . . 7 $/\$ $/\$
296		peano2 7086	. . . . . . . . 9
297		fnfvelrn 6356	. . . . . . . . 9 $/\$
298	147, 296, 297	syl2an 494	. . . . . . . 8 $/\$
299	298	adantlr 751	. . . . . . 7 $/\$ $/\$
300	240	expcom 451	. . . . . . . . 9 $/\$
301	300	ralrimiv 2965	. . . . . . . 8 $/\$
302		id 22	. . . . . . . . . . 11
303		fveq2 6191	. . . . . . . . . . . 12
304	303	dmeqd 5326	. . . . . . . . . . 11
305	302, 304	eleq12d 2695	. . . . . . . . . 10
306	305	rspcv 3305	. . . . . . . . 9
307	296, 306	syl 17	. . . . . . . 8
308	301, 307	mpan9 486	. . . . . . 7 $/\$ $/\$
309		eleq2 2690	. . . . . . . . . . . . . . . . . . . . 21
310	309	biimpa 501	. . . . . . . . . . . . . . . . . . . 20 $/\$
311	29, 310	sylan 488	. . . . . . . . . . . . . . . . . . 19 $/\$
312		ordsucelsuc 7022	. . . . . . . . . . . . . . . . . . . . . . 23
313	30, 312	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
314	313	biimprd 238	. . . . . . . . . . . . . . . . . . . . 21
315		rsp 2929	. . . . . . . . . . . . . . . . . . . . 21
316	314, 315	syl9r 78	. . . . . . . . . . . . . . . . . . . 20
317	316	com13 88	. . . . . . . . . . . . . . . . . . 19
318	311, 317	syl 17	. . . . . . . . . . . . . . . . . 18 $/\$
319	318	ex 450	. . . . . . . . . . . . . . . . 17
320	319	com24 95	. . . . . . . . . . . . . . . 16
321	320	imp 445	. . . . . . . . . . . . . . 15 $/\$
322	321	3adant2 1080	. . . . . . . . . . . . . 14 $/\$ $/\$
323	322	impcom 446	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
324	323	rexlimiva 3028	. . . . . . . . . . . 12 $/\$ $/\$
325	324	ss2abi 3674	. . . . . . . . . . 11 $/\$ $/\$
326	28, 325	eqsstri 3635	. . . . . . . . . 10
327		sstr 3611	. . . . . . . . . 10 $/\$
328	326, 327	mpan2 707	. . . . . . . . 9
329	328	sseld 3602	. . . . . . . 8
330		fvex 6201	. . . . . . . . 9
331		dmeq 5324	. . . . . . . . . . 11
332	331	eleq2d 2687	. . . . . . . . . 10
333		fveq1 6190	. . . . . . . . . . 11
334		fveq1 6190	. . . . . . . . . . . 12
335	334	fveq2d 6195	. . . . . . . . . . 11
336	333, 335	eleq12d 2695	. . . . . . . . . 10
337	332, 336	imbi12d 334	. . . . . . . . 9
338	330, 337	elab 3350	. . . . . . . 8
339	329, 338	syl6ib 241	. . . . . . 7
340	295, 299, 308, 339	syl3c 66	. . . . . 6 $/\$ $/\$
341	210	adantr 481	. . . . . . . 8 $/\$ $/\$
342		elssuni 4467	. . . . . . . . . 10
343	298, 342	syl 17	. . . . . . . . 9 $/\$
344	343	adantlr 751	. . . . . . . 8 $/\$ $/\$
345		funssfv 6209	. . . . . . . 8 $/\$ $/\$
346	341, 344, 308, 345	syl3anc 1326	. . . . . . 7 $/\$ $/\$
347	216	sseld 3602	. . . . . . . . . . . . . . 15 $/\$
348	331	eleq2d 2687	. . . . . . . . . . . . . . . . 17
349	331	eleq1d 2686	. . . . . . . . . . . . . . . . 17
350	348, 349	anbi12d 747	. . . . . . . . . . . . . . . 16 $/\$ $/\$
351	330, 350	elab 3350	. . . . . . . . . . . . . . 15 $/\$ $/\$
352	347, 351	syl6ib 241	. . . . . . . . . . . . . 14 $/\$
353	352	adantr 481	. . . . . . . . . . . . 13 $/\$ $/\$
354	298, 353	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$
355	354	simprd 479	. . . . . . . . . . 11 $/\$
356		nnord 7073	. . . . . . . . . . 11
357		ordtr 5737	. . . . . . . . . . 11
358		trsuc 5810	. . . . . . . . . . . 12 $/\$
359	358	ex 450	. . . . . . . . . . 11
360	355, 356, 357, 359	4syl 19	. . . . . . . . . 10 $/\$
361	360	adantlr 751	. . . . . . . . 9 $/\$ $/\$
362	308, 361	mpd 15	. . . . . . . 8 $/\$ $/\$
363		funssfv 6209	. . . . . . . 8 $/\$ $/\$
364	341, 344, 362, 363	syl3anc 1326	. . . . . . 7 $/\$ $/\$
365		simpl 473	. . . . . . . 8 $/\$
366		simpr 477	. . . . . . . . 9 $/\$
367	366	fveq2d 6195	. . . . . . . 8 $/\$
368	365, 367	eleq12d 2695	. . . . . . 7 $/\$
369	346, 364, 368	syl2anc 693	. . . . . 6 $/\$ $/\$
370	340, 369	mpbird 247	. . . . 5 $/\$ $/\$
371	370	ex 450	. . . 4 $/\$
372	294, 371	ralrimi 2957	. . 3 $/\$
373		vex 3203	. . . . . 6
374	373	rnex 7100	. . . . 5
375	374	uniex 6953	. . . 4
376		feq1 6026	. . . . 5
377		fveq1 6190	. . . . . 6
378	377	eqeq1d 2624	. . . . 5
379		fveq1 6190	. . . . . . 7
380		fveq1 6190	. . . . . . . 8
381	380	fveq2d 6195	. . . . . . 7
382	379, 381	eleq12d 2695	. . . . . 6
383	382	ralbidv 2986	. . . . 5
384	376, 378, 383	3anbi123d 1399	. . . 4 $/\$ $/\$ $/\$ $/\$
385	375, 384	spcev 3300	. . 3 $/\$ $/\$ $/\$ $/\$
386	269, 291, 372, 385	syl3anc 1326	. 2 $/\$ $/\$ $/\$
387	386	exlimiv 1858	1 $/\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $\/$ w3o 1036 $/\$ w3a 1037

wceq 1483

wex 1704

wcel 1990

cab 2608

wral 2912

wrex 2913

crab 2916

cvv 3200

wss 3574

c0 3915

cop 4183

cuni 4436

ciun 4520

cmpt 4729

wtr 4752

cdm 5114

crn 5115

cres 5116

word 5722

csuc 5725

wfun 5882

wfn 5883

wf 5884

cfv 5888

com 7065

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-dc 9268

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-fv 5896 df-om 7066 df-1o 7560

This theorem is referenced by: axdc3lem4 9275

W3C validator