axdc3lem4 - Metamath Proof Explorer

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

Theorem axdc3lem4 9275

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

is nonempty, and that

always maps to a nonempty subset of

, so that we can apply axdc2 9271. See axdc3lem2 9273 for the rest of the proof. (Contributed by Mario Carneiro, 27-Jan-2013.)

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

**Assertion**
Ref	Expression
axdc3lem4	$/\$ $\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

Proof of Theorem axdc3lem4 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		peano1 7085	. . . . . 6
2		eqid 2622	. . . . . . . . . 10
3		fsng 6404	. . . . . . . . . . 11 $/\$
4	1, 3	mpan 706	. . . . . . . . . 10
5	2, 4	mpbiri 248	. . . . . . . . 9
6		snssi 4339	. . . . . . . . 9
7	5, 6	fssd 6057	. . . . . . . 8
8		suc0 5799	. . . . . . . . 9
9	8	feq2i 6037	. . . . . . . 8
10	7, 9	sylibr 224	. . . . . . 7
11		fvsng 6447	. . . . . . . 8 $/\$
12	1, 11	mpan 706	. . . . . . 7
13		ral0 4076	. . . . . . . 8
14	13	a1i 11	. . . . . . 7
15	10, 12, 14	3jca 1242	. . . . . 6 $/\$ $/\$
16		suceq 5790	. . . . . . . . 9
17	16	feq2d 6031	. . . . . . . 8
18		raleq 3138	. . . . . . . 8
19	17, 18	3anbi13d 1401	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
20	19	rspcev 3309	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
21	1, 15, 20	sylancr 695	. . . . 5 $/\$ $/\$
22		axdc3lem4.1	. . . . . 6
23		axdc3lem4.2	. . . . . 6 $/\$ $/\$
24		snex 4908	. . . . . 6
25	22, 23, 24	axdc3lem3 9274	. . . . 5 $/\$ $/\$
26	21, 25	sylibr 224	. . . 4
27		ne0i 3921	. . . 4
28	26, 27	syl 17	. . 3
29		ssrab2 3687	. . . . . . 7 $/\$
30	22, 23	axdc3lem 9272	. . . . . . . 8
31	30	elpw2 4828	. . . . . . 7 $/\$ $/\$
32	29, 31	mpbir 221	. . . . . 6 $/\$
33	32	a1i 11	. . . . 5 $\$ $/\$ $/\$
34		vex 3203	. . . . . . . . . 10
35	22, 23, 34	axdc3lem3 9274	. . . . . . . . 9 $/\$ $/\$
36		simp2 1062	. . . . . . . . . . . . . . . 16 $/\$ $/\$
37		vex 3203	. . . . . . . . . . . . . . . . . . . . . 22
38	37	sucid 5804	. . . . . . . . . . . . . . . . . . . . 21
39		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . 21 $/\$
40	38, 39	mpan2 707	. . . . . . . . . . . . . . . . . . . 20
41		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $\$
42	40, 41	sylan2 491	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\$
43		eldifn 3733	. . . . . . . . . . . . . . . . . . . 20 $\$
44		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . 23
45	44	elsn 4192	. . . . . . . . . . . . . . . . . . . . . 22
46	45	necon3bbii 2841	. . . . . . . . . . . . . . . . . . . . 21
47		n0 3931	. . . . . . . . . . . . . . . . . . . . 21
48	46, 47	bitri 264	. . . . . . . . . . . . . . . . . . . 20
49	43, 48	sylib 208	. . . . . . . . . . . . . . . . . . 19 $\$
50	42, 49	syl 17	. . . . . . . . . . . . . . . . . 18 $\$ $/\$
51		simp32 1098	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
52		eldifi 3732	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $\$
53		elelpwi 4171	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
54	53	expcom 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
55	42, 52, 54	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\$ $/\$
56		peano2 7086	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
57	56	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
58	57	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
59		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
60	34	dmex 7099	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
61		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
62		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
63		fsng 6404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
64	62, 63	mpbiri 248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
65	60, 61, 64	mp2an 708	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
66		simpr 477	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$
67	66	snssd 4340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
68		fss 6056	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
69	65, 67, 68	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
70		fdm 6051	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
71	56	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$
72		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
73	72	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$
74	71, 73	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$
75		nnord 7073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
76		ordirr 5741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
77	74, 75, 76	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
78		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
79	78	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
80	77, 79	mtbid 314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
81		disjsn 4246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
82	80, 81	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
83	70, 82	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
84	83	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
85		fun2 6067	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
86	59, 69, 84, 85	syl21anc 1325	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
87		sneq 4187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
88	87	uneq2d 3767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
89		df-suc 5729	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
90	88, 89	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
91	70, 90	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
92	91	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
93	92	feq2d 6031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
94	86, 93	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
95	94	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
96	95	adantrd 484	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
97	96	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
98	97	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
99	98	3adant1 1079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$
100	99	3imp 1256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
101		ffun 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
102	101	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
103	60, 61	funsn 5939	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
104	102, 103	jctir 561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
105	61	dmsnop 5609	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
106	105	ineq2i 3811	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
107		disjsn 4246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
108	77, 107	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$
109	106, 108	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
110	70, 109	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
111		funun 5932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
112	104, 110, 111	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
113		ssun1 3776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
115		nnord 7073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
116		0elsuc 7035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
117	115, 116	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
118	117	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
119	70	eleq2d 2687	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
120	119	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$
121	118, 120	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$
122		funssfv 6209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
123	112, 114, 121, 122	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
124	123	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
125	124	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
126	125	3adant1 1079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
127	126	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
128	127	adantrl 752	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
129	128	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
130		nfra1 2941	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
131		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
132		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
133	130, 131, 132	nf3an 1831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
134		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
135		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
136	133, 134, 135	nf3an 1831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$
137		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
138		elsuci 5791	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $\/$
139		rsp 2929	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
140	139	impcom 446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$
141	140	ad2ant2lr 784	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$ $/\$
142	141	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 $/\$ $/\$ $/\$ $/\$
143	112	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$ $/\$
144	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$ $/\$
145		ordsucelsuc 7022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
146	115, 145	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
147	146	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$
148		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
149	148	biimparc 504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$
150	147, 70, 149	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$ $/\$
151		funssfv 6209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$ $/\$
152	143, 144, 150, 151	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$ $/\$
153	152	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$ $/\$ $/\$
154	112	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
155	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
156		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
157	156	biimparc 504	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 $/\$
158	70, 157	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 $/\$
159	158	3adant1 1079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
160		funssfv 6209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
161	154, 155, 159, 160	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$ $/\$
162	161	3adant1r 1319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$ $/\$ $/\$
163	162	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$ $/\$ $/\$
164	153, 163	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$ $/\$
165	164	3adant2l 1320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 $/\$ $/\$ $/\$ $/\$
166	142, 165	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$ $/\$ $/\$ $/\$
167	166	a1d 25	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$ $/\$ $/\$
168	167	3expib 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$
169	168	expcom 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
170	112	3adant1 1079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
171		ssun2 3777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
173		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
174	173	eqeq2d 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
175	174	biimpar 502	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 $/\$
176	60	snid 4208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
177	176, 105	eleqtrri 2700	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
178	175, 177	syl6eqelr 2710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 $/\$
179	70, 178	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 $/\$
180	179	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
181		funssfv 6209	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
182	170, 172, 180, 181	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$ $/\$
183	175	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 $/\$ $/\$
184	60, 61	fvsn 6446	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
185		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
186	184, 185	syl5reqr 2671	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
187	183, 186	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
188	70, 187	syl3an3 1361	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$ $/\$
189	182, 188	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$ $/\$
190	189	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$ $/\$
191	190	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$ $/\$
192	161	3adant1l 1318	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$ $/\$ $/\$
193		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
194	193	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$
195	194	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$ $/\$ $/\$
196	192, 195	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$ $/\$ $/\$
197	196	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$ $/\$
198	191, 197	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 $/\$ $/\$ $/\$
199	198	3adant2l 1320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$ $/\$ $/\$ $/\$
200	199	biimprd 238	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$ $/\$ $/\$
201	200	3expib 1268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$
202	201	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
203	169, 202	jaoi 394	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $\/$ $/\$ $/\$
204	138, 203	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
205	204	com3r 87	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$
206	137, 205	mpd 15	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
207	206	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
208	207	expcom 451	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
209	208	3impd 1281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
210	209	impd 447	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$
211	210	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$
212	211	3adant3 1081	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$
213	136, 212	ralrimi 2957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
214		suceq 5790	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
215	214	feq2d 6031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
216		raleq 3138	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
217	215, 216	3anbi13d 1401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$
218	217	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
219	58, 100, 129, 213, 218	syl13anc 1328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
220		snex 4908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
221	34, 220	unex 6956	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
222	22, 23, 221	axdc3lem3 9274	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
223	219, 222	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
224	223	3coml 1272	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
225	224	3exp 1264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$
226	225	expd 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
227	55, 226	sylcom 30	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\$ $/\$ $/\$ $/\$
228	227	3impd 1281	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$ $/\$ $/\$ $/\$ $/\$
229	228	ex 450	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$ $/\$ $/\$ $/\$
230	229	com23 86	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$ $/\$ $/\$ $/\$
231	51, 230	mpdi 45	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $/\$ $/\$ $/\$
232	231	imp 445	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$ $/\$ $/\$ $/\$ $/\$
233		resundir 5411	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
234		frel 6050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
235		resdm 5441	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
236	234, 235	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
237	236	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
238	70, 74	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
239	75, 76	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
240		incom 3805	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
241	240	eqeq1i 2627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
242	60, 61	fnsn 5946	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
243		fnresdisj 6001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
244	242, 243	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
245	241, 244, 107	3bitr3ri 291	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
246	239, 245	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
247	238, 246	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
248	237, 247	uneq12d 3768	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
249		un0 3967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
250	248, 249	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
251	233, 250	syl5eq 2668	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
252	251	ancoms 469	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
253	252	3adant1 1079	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
254	253	3ad2ant3 1084	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
255	254	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $/\$ $/\$ $/\$ $/\$ $/\$
256	105	uneq2i 3764	. . . . . . . . . . . . . . . . . . . . . . . 24
257		dmun 5331	. . . . . . . . . . . . . . . . . . . . . . . 24
258		df-suc 5729	. . . . . . . . . . . . . . . . . . . . . . . 24
259	256, 257, 258	3eqtr4i 2654	. . . . . . . . . . . . . . . . . . . . . . 23
260	255, 259	jctil 560	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
261		dmeq 5324	. . . . . . . . . . . . . . . . . . . . . . . . 25
262	261	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . 24
263		reseq1 5390	. . . . . . . . . . . . . . . . . . . . . . . . 25
264	263	eqeq1d 2624	. . . . . . . . . . . . . . . . . . . . . . . 24
265	262, 264	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
266	265	rspcev 3309	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
267	232, 260, 266	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 $\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
268	267	3exp2 1285	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$ $/\$ $/\$
269	268	exlimdv 1861	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $/\$ $/\$
270	269	adantr 481	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $/\$ $/\$
271	50, 270	mpd 15	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $/\$ $/\$
272	271	com3r 87	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $/\$
273	36, 272	mpan2d 710	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$
274	273	com3r 87	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $/\$
275	274	3expd 1284	. . . . . . . . . . . . 13 $\$ $/\$
276	275	com3r 87	. . . . . . . . . . . 12 $\$ $/\$
277	276	3imp 1256	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$
278	277	com12 32	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$
279	278	rexlimiv 3027	. . . . . . . . 9 $/\$ $/\$ $\$ $/\$
280	35, 279	sylbi 207	. . . . . . . 8 $\$ $/\$
281	280	impcom 446	. . . . . . 7 $\$ $/\$ $/\$
282		rabn0 3958	. . . . . . 7 $/\$ $/\$
283	281, 282	sylibr 224	. . . . . 6 $\$ $/\$ $/\$
284	30	rabex 4813	. . . . . . . 8 $/\$
285	284	elsn 4192	. . . . . . 7 $/\$ $/\$
286	285	necon3bbii 2841	. . . . . 6 $/\$ $/\$
287	283, 286	sylibr 224	. . . . 5 $\$ $/\$ $/\$
288	33, 287	eldifd 3585	. . . 4 $\$ $/\$ $/\$ $\$
289		axdc3lem4.3	. . . 4 $/\$
290	288, 289	fmptd 6385	. . 3 $\$ $\$
291	30	axdc2 9271	. . 3 $/\$ $\$ $/\$
292	28, 290, 291	syl2an 494	. 2 $/\$ $\$ $/\$
293	22, 23, 289	axdc3lem2 9273	. 2 $/\$ $/\$ $/\$
294	292, 293	syl 17	1 $/\$ $\$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wex 1704

wcel 1990

cab 2608

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200 $\$ cdif 3571

cun 3572

cin 3573

wss 3574

c0 3915

cpw 4158

csn 4177

cop 4183

cmpt 4729

cdm 5114

cres 5116

wrel 5119

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-reu 2919 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-ima 5127 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-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-om 7066 df-1o 7560

This theorem is referenced by: axdc3 9276

W3C validator