cantnflem1 - Metamath Proof Explorer

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

Theorem cantnflem1 8586

Description: Lemma for cantnf 8590. This part of the proof is showing uniqueness of the Cantor normal form. We already know that the relation

is a strict order, but we haven't shown it is a well-order yet. But being a strict order is enough to show that two distinct

are

-related as

, and WLOG assuming that

, we show that CNF respects this order and maps these two to different ordinals. (Contributed by Mario Carneiro, 28-May-2015.) (Revised by AV, 2-Jul-2019.)

**Hypotheses**
Ref	Expression
cantnfs.s	CNF
cantnfs.a
cantnfs.b
oemapval.t	$/\$
oemapval.f
oemapval.g
oemapvali.r
oemapvali.x
cantnflem1.o	OrdIso supp
cantnflem1.h	seq_𝜔

**Assertion**
Ref	Expression
cantnflem1	CNF CNF

Distinct variable groups:

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

Proof of Theorem cantnflem1 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ovex 6678	. . . . . 6 supp
2		cantnflem1.o	. . . . . . 7 OrdIso supp
3	2	oion 8441	. . . . . 6 supp
4	1, 3	mp1i 13	. . . . 5
5		uniexg 6955	. . . . 5
6		sucidg 5803	. . . . 5
7	4, 5, 6	3syl 18	. . . 4
8		cantnfs.s	. . . . . . . . . 10 CNF
9		cantnfs.a	. . . . . . . . . 10
10		cantnfs.b	. . . . . . . . . 10
11		oemapval.t	. . . . . . . . . 10 $/\$
12		oemapval.f	. . . . . . . . . 10
13		oemapval.g	. . . . . . . . . 10
14		oemapvali.r	. . . . . . . . . 10
15		oemapvali.x	. . . . . . . . . 10
16	8, 9, 10, 11, 12, 13, 14, 15	cantnflem1a 8582	. . . . . . . . 9 supp
17		n0i 3920	. . . . . . . . 9 supp supp
18	16, 17	syl 17	. . . . . . . 8 supp
19		ovexd 6680	. . . . . . . . . 10 supp
20	8, 9, 10, 2, 13	cantnfcl 8564	. . . . . . . . . . 11 supp $/\$
21	20	simpld 475	. . . . . . . . . 10 supp
22	2	oien 8443	. . . . . . . . . 10 supp $/\$ supp supp
23	19, 21, 22	syl2anc 693	. . . . . . . . 9 supp
24		breq1 4656	. . . . . . . . . 10 supp supp
25		ensymb 8004	. . . . . . . . . . 11 supp supp
26		en0 8019	. . . . . . . . . . 11 supp supp
27	25, 26	bitri 264	. . . . . . . . . 10 supp supp
28	24, 27	syl6bb 276	. . . . . . . . 9 supp supp
29	23, 28	syl5ibcom 235	. . . . . . . 8 supp
30	18, 29	mtod 189	. . . . . . 7
31	20	simprd 479	. . . . . . . 8
32		nnlim 7078	. . . . . . . 8
33	31, 32	syl 17	. . . . . . 7
34		ioran 511	. . . . . . 7 $\/$ $/\$
35	30, 33, 34	sylanbrc 698	. . . . . 6 $\/$
36	2	oicl 8434	. . . . . . 7
37		unizlim 5844	. . . . . . 7 $\/$
38	36, 37	mp1i 13	. . . . . 6 $\/$
39	35, 38	mtbird 315	. . . . 5
40		orduniorsuc 7030	. . . . . . 7 $\/$
41	36, 40	mp1i 13	. . . . . 6 $\/$
42	41	ord 392	. . . . 5
43	39, 42	mpd 15	. . . 4
44	7, 43	eleqtrrd 2704	. . 3
45	2	oiiso 8442	. . . . . . . 8 supp $/\$ supp supp
46	19, 21, 45	syl2anc 693	. . . . . . 7 supp
47		isof1o 6573	. . . . . . 7 supp supp
48	46, 47	syl 17	. . . . . 6 supp
49		f1ocnv 6149	. . . . . 6 supp supp
50		f1of 6137	. . . . . 6 supp supp
51	48, 49, 50	3syl 18	. . . . 5 supp
52	51, 16	ffvelrnd 6360	. . . 4
53		elssuni 4467	. . . 4
54	52, 53	syl 17	. . 3
55	43, 31	eqeltrrd 2702	. . . . 5
56		peano2b 7081	. . . . 5
57	55, 56	sylibr 224	. . . 4
58		eleq1 2689	. . . . . . . 8
59		sseq2 3627	. . . . . . . 8
60	58, 59	anbi12d 747	. . . . . . 7 $/\$ $/\$
61		fveq2 6191	. . . . . . . . . . . 12
62	61	sseq2d 3633	. . . . . . . . . . 11
63	62	ifbid 4108	. . . . . . . . . 10
64	63	mpteq2dv 4745	. . . . . . . . 9
65	64	fveq2d 6195	. . . . . . . 8 CNF CNF
66		suceq 5790	. . . . . . . . 9
67	66	fveq2d 6195	. . . . . . . 8
68	65, 67	eleq12d 2695	. . . . . . 7 CNF CNF
69	60, 68	imbi12d 334	. . . . . 6 $/\$ CNF $/\$ CNF
70	69	imbi2d 330	. . . . 5 $/\$ CNF $/\$ CNF
71		eleq1 2689	. . . . . . . 8
72		sseq2 3627	. . . . . . . 8
73	71, 72	anbi12d 747	. . . . . . 7 $/\$ $/\$
74		fveq2 6191	. . . . . . . . . . . 12
75	74	sseq2d 3633	. . . . . . . . . . 11
76	75	ifbid 4108	. . . . . . . . . 10
77	76	mpteq2dv 4745	. . . . . . . . 9
78	77	fveq2d 6195	. . . . . . . 8 CNF CNF
79		suceq 5790	. . . . . . . . 9
80	79	fveq2d 6195	. . . . . . . 8
81	78, 80	eleq12d 2695	. . . . . . 7 CNF CNF
82	73, 81	imbi12d 334	. . . . . 6 $/\$ CNF $/\$ CNF
83		eleq1 2689	. . . . . . . 8
84		sseq2 3627	. . . . . . . 8
85	83, 84	anbi12d 747	. . . . . . 7 $/\$ $/\$
86		fveq2 6191	. . . . . . . . . . . 12
87	86	sseq2d 3633	. . . . . . . . . . 11
88	87	ifbid 4108	. . . . . . . . . 10
89	88	mpteq2dv 4745	. . . . . . . . 9
90	89	fveq2d 6195	. . . . . . . 8 CNF CNF
91		suceq 5790	. . . . . . . . 9
92	91	fveq2d 6195	. . . . . . . 8
93	90, 92	eleq12d 2695	. . . . . . 7 CNF CNF
94	85, 93	imbi12d 334	. . . . . 6 $/\$ CNF $/\$ CNF
95		eleq1 2689	. . . . . . . 8
96		sseq2 3627	. . . . . . . 8
97	95, 96	anbi12d 747	. . . . . . 7 $/\$ $/\$
98		fveq2 6191	. . . . . . . . . . . 12
99	98	sseq2d 3633	. . . . . . . . . . 11
100	99	ifbid 4108	. . . . . . . . . 10
101	100	mpteq2dv 4745	. . . . . . . . 9
102	101	fveq2d 6195	. . . . . . . 8 CNF CNF
103		suceq 5790	. . . . . . . . 9
104	103	fveq2d 6195	. . . . . . . 8
105	102, 104	eleq12d 2695	. . . . . . 7 CNF CNF
106	97, 105	imbi12d 334	. . . . . 6 $/\$ CNF $/\$ CNF
107		f1ocnvfv2 6533	. . . . . . . . . . . . 13 supp $/\$ supp
108	48, 16, 107	syl2anc 693	. . . . . . . . . . . 12
109	108	sseq2d 3633	. . . . . . . . . . 11
110	109	ifbid 4108	. . . . . . . . . 10
111	110	mpteq2dv 4745	. . . . . . . . 9
112	111	fveq2d 6195	. . . . . . . 8 CNF CNF
113		cantnflem1.h	. . . . . . . . 9 seq_𝜔
114	8, 9, 10, 11, 12, 13, 14, 15, 2, 113	cantnflem1d 8585	. . . . . . . 8 CNF
115	112, 114	eqeltrd 2701	. . . . . . 7 CNF
116		ss0 3974	. . . . . . . . . . . . . 14
117	116	fveq2d 6195	. . . . . . . . . . . . 13
118	117	sseq2d 3633	. . . . . . . . . . . 12
119	118	ifbid 4108	. . . . . . . . . . 11
120	119	mpteq2dv 4745	. . . . . . . . . 10
121	120	fveq2d 6195	. . . . . . . . 9 CNF CNF
122		suceq 5790	. . . . . . . . . . 11
123	116, 122	syl 17	. . . . . . . . . 10
124	123	fveq2d 6195	. . . . . . . . 9
125	121, 124	eleq12d 2695	. . . . . . . 8 CNF CNF
126	125	adantl 482	. . . . . . 7 $/\$ CNF CNF
127	115, 126	syl5ibcom 235	. . . . . 6 $/\$ CNF
128		ordelon 5747	. . . . . . . . . . . . 13 $/\$
129	36, 52, 128	sylancr 695	. . . . . . . . . . . 12
130	129	adantr 481	. . . . . . . . . . 11 $/\$
131	36	a1i 11	. . . . . . . . . . . 12
132		ordelon 5747	. . . . . . . . . . . 12 $/\$
133	131, 132	sylan 488	. . . . . . . . . . 11 $/\$
134		onsseleq 5765	. . . . . . . . . . 11 $/\$ $\/$
135	130, 133, 134	syl2anc 693	. . . . . . . . . 10 $/\$ $\/$
136		sucelon 7017	. . . . . . . . . . . . . . 15
137	133, 136	sylibr 224	. . . . . . . . . . . . . 14 $/\$
138		eloni 5733	. . . . . . . . . . . . . 14
139	137, 138	syl 17	. . . . . . . . . . . . 13 $/\$
140		ordsssuc 5812	. . . . . . . . . . . . 13 $/\$
141	130, 139, 140	syl2anc 693	. . . . . . . . . . . 12 $/\$
142		ordtr 5737	. . . . . . . . . . . . . . . . 17
143	36, 142	mp1i 13	. . . . . . . . . . . . . . . 16 $/\$ $/\$
144		simprl 794	. . . . . . . . . . . . . . . 16 $/\$ $/\$
145		trsuc 5810	. . . . . . . . . . . . . . . 16 $/\$
146	143, 144, 145	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$ $/\$
147		simprr 796	. . . . . . . . . . . . . . 15 $/\$ $/\$
148	146, 147	jca 554	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
149	9	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
150	10	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
151		oecl 7617	. . . . . . . . . . . . . . . . . . 19 $/\$
152	149, 150, 151	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
153	8, 149, 150	cantnff 8571	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ CNF
154	8, 9, 10	cantnfs 8563	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ finSupp
155	12, 154	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ finSupp
156	155	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . 24
157	156	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158	8, 9, 10	cantnfs 8563	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ finSupp
159	13, 158	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ finSupp
160	159	simpld 475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
161	8, 9, 10, 11, 12, 13, 14, 15	oemapvali 8581	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
162	161	simp1d 1073	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
163	160, 162	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . 26
164		ne0i 3921	. . . . . . . . . . . . . . . . . . . . . . . . . 26
165	163, 164	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
166		on0eln0 5780	. . . . . . . . . . . . . . . . . . . . . . . . . 26
167	9, 166	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25
168	165, 167	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . 24
169	168	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
170	157, 169	ifcld 4131	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
171		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22
172	170, 171	fmptd 6385	. . . . . . . . . . . . . . . . . . . . 21
173		mptexg 6484	. . . . . . . . . . . . . . . . . . . . . . 23
174	10, 173	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
175		funmpt 5926	. . . . . . . . . . . . . . . . . . . . . . 23
176	175	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22
177	155	simprd 479	. . . . . . . . . . . . . . . . . . . . . 22 finSupp
178		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 supp supp
179		eqimss2 3658	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 supp supp supp supp
180	178, 179	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . 26 supp supp
181		0ex 4790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26
183	156, 180, 10, 182	suppssr 7326	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $\$ supp
184	183	ifeq1d 4104	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$ supp
185		ifid 4125	. . . . . . . . . . . . . . . . . . . . . . . 24
186	184, 185	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ supp
187	186, 10	suppss2 7329	. . . . . . . . . . . . . . . . . . . . . 22 supp supp
188		fsuppsssupp 8291	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ finSupp $/\$ supp supp finSupp
189	174, 176, 177, 187, 188	syl22anc 1327	. . . . . . . . . . . . . . . . . . . . 21 finSupp
190	8, 9, 10	cantnfs 8563	. . . . . . . . . . . . . . . . . . . . 21 $/\$ finSupp
191	172, 189, 190	mpbir2and 957	. . . . . . . . . . . . . . . . . . . 20
192	191	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
193	153, 192	ffvelrnd 6360	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ CNF
194		onelon 5748	. . . . . . . . . . . . . . . . . 18 $/\$ CNF CNF
195	152, 193, 194	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ CNF
196	31	adantr 481	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
197		elnn 7075	. . . . . . . . . . . . . . . . . . 19 $/\$
198	144, 196, 197	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
199	113	cantnfvalf 8562	. . . . . . . . . . . . . . . . . . 19
200	199	ffvelrni 6358	. . . . . . . . . . . . . . . . . 18
201	198, 200	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
202		suppssdm 7308	. . . . . . . . . . . . . . . . . . . . . . 23 supp
203		fdm 6051	. . . . . . . . . . . . . . . . . . . . . . . 24
204	160, 203	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23
205	202, 204	syl5sseq 3653	. . . . . . . . . . . . . . . . . . . . . 22 supp
206	205	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ supp
207	2	oif 8435	. . . . . . . . . . . . . . . . . . . . . . 23 supp
208	207	ffvelrni 6358	. . . . . . . . . . . . . . . . . . . . . 22 supp
209	144, 208	syl 17	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ supp
210	206, 209	sseldd 3604	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
211		onelon 5748	. . . . . . . . . . . . . . . . . . . 20 $/\$
212	150, 210, 211	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
213		oecl 7617	. . . . . . . . . . . . . . . . . . 19 $/\$
214	149, 212, 213	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
215	156	adantr 481	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
216	215, 210	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
217		onelon 5748	. . . . . . . . . . . . . . . . . . 19 $/\$
218	149, 216, 217	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
219		omcl 7616	. . . . . . . . . . . . . . . . . 18 $/\$
220	214, 218, 219	syl2anc 693	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
221		oaord 7627	. . . . . . . . . . . . . . . . 17 CNF $/\$ $/\$ CNF CNF
222	195, 201, 220, 221	syl3anc 1326	. . . . . . . . . . . . . . . 16 $/\$ $/\$ CNF CNF
223		ifeq1 4090	. . . . . . . . . . . . . . . . . . . . . . 23
224		ifid 4125	. . . . . . . . . . . . . . . . . . . . . . 23
225	223, 224	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . 22
226		ifeq1 4090	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $\/$
227		ifid 4125	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
228	226, 227	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . 22 $\/$
229	225, 228	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . 21 $\/$
230		onss 6990	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
231	10, 230	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
232	231	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
233	232	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
234	212	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
235		onsseleq 5765	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$
236	233, 234, 235	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $\/$
237	236	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $\/$
238	233	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
239	207	ffvelrni 6358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 supp
240	146, 239	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ supp
241	206, 240	sseldd 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
242		onelon 5748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
243	150, 241, 242	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
244	243	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
245		onsssuc 5813	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
246	238, 244, 245	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
247		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
248	247	sucid 5804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
249	46	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ supp
250		isorel 6576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 supp $/\$ $/\$
251	249, 146, 144, 250	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$
252	247	sucex 7011	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
253	252	epelc 5031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
254		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
255	254	epelc 5031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
256	251, 253, 255	3bitr3g 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
257	248, 256	mpbii 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
258		eloni 5733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
259	212, 258	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$
260		ordelsuc 7020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
261	243, 259, 260	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$
262	257, 261	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$
263	262	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
264	263	sseld 3602	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
265	246, 264	sylbid 230	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
266		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$
267	249	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ supp
268	267, 47	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ supp
269	8, 9, 10, 11, 12, 13, 14, 15, 2	cantnflem1c 8584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ supp
270		f1ocnvfv2 6533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 supp $/\$ supp
271	268, 269, 270	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$
272	266, 271	eleqtrrd 2704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
273	146	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
274	268, 49, 50	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ supp
275	274, 269	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$
276		isorel 6576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 supp $/\$ $/\$
277	267, 273, 275, 276	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$
278		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
279	278	epelc 5031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
280		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
281	280	epelc 5031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
282	277, 279, 281	3bitr3g 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
283	272, 282	mpbird 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
284		ordelon 5747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
285	36, 275, 284	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$
286		eloni 5733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
287	285, 286	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
288		ordelsuc 7020	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
289	283, 287, 288	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
290	283, 289	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
291	144	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$
292	36, 291, 132	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
293		ontri1 5757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$
294	292, 285, 293	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
295	290, 294	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
296		isorel 6576	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 supp $/\$ $/\$
297	267, 275, 291, 296	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$
298	252	epelc 5031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
299	254	epelc 5031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
300	297, 298, 299	3bitr3g 302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
301	271	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$
302	300, 301	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$
303	295, 302	mtbid 314	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$
304	303	expr 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$
305	304	con2d 129	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
306		ontri1 5757	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
307	238, 244, 306	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$
308	305, 307	sylibrd 249	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$
309	265, 308	impbid 202	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
310	309	orbi1d 739	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $\/$ $\/$
311	237, 310	bitr4d 271	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $\/$
312		orcom 402	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $\/$
313	311, 312	syl6bb 276	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\/$
314	313	ifbid 4108	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $\/$
315		eqidd 2623	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
316	229, 314, 315	pm2.61ne 2879	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $\/$
317	316	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$
318	317	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ CNF CNF $\/$
319		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
320	319, 181	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . 26
321	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
322	321	ralrimivw 2967	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
323	171	fnmpt 6020	. . . . . . . . . . . . . . . . . . . . . . . 24
324	322, 323	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
325	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
326		suppvalfn 7302	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ supp
327		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25
328		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . 25
329		nffvmpt1 6199	. . . . . . . . . . . . . . . . . . . . . . . . . 26
330		nfcv 2764	. . . . . . . . . . . . . . . . . . . . . . . . . 26
331	329, 330	nfne 2894	. . . . . . . . . . . . . . . . . . . . . . . . 25
332		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . 25
333		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
334	333	neeq1d 2853	. . . . . . . . . . . . . . . . . . . . . . . . 25
335	327, 328, 331, 332, 334	cbvrab 3198	. . . . . . . . . . . . . . . . . . . . . . . 24
336	326, 335	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ supp
337	324, 150, 325, 336	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ supp
338		eqidd 2623	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
339	320	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$
340	338, 339	fvmpt2d 6293	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
341	340	neeq1d 2853	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
342	339	biantrurd 529	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
343		dif1o 7580	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $/\$
344	342, 343	syl6bbr 278	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $\$
345	341, 344	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$
346	345	rabbidva 3188	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\$
347	337, 346	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ supp $\$
348	320, 343	mpbiran 953	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$
349		ifeq1 4090	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
350	349, 185	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
351	350	necon3i 2826	. . . . . . . . . . . . . . . . . . . . . . . . . 26
352		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
353	352	necon1ai 2821	. . . . . . . . . . . . . . . . . . . . . . . . . 26
354	351, 353	jca 554	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
355	265	expimpd 629	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
356	354, 355	syl5 34	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
357	348, 356	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $\$
358	357	3impia 1261	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $\$
359	358	rabssdv 3682	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $\$
360	347, 359	eqsstrd 3639	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ supp
361		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . 24
362		sseq1 3626	. . . . . . . . . . . . . . . . . . . . . . . 24
363	361, 362	orbi12d 746	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$ $\/$
364		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23
365	363, 364	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . 22 $\/$ $\/$
366	365	cbvmptv 4750	. . . . . . . . . . . . . . . . . . . . 21 $\/$ $\/$
367		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25
368	367	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
369	368	ifeq1da 4116	. . . . . . . . . . . . . . . . . . . . . . 23
370	362, 364	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . . . . . 26
371		fvex 6201	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
372	371, 181	ifex 4156	. . . . . . . . . . . . . . . . . . . . . . . . . 26
373	370, 171, 372	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . . . . 25
374	373	ifeq2d 4105	. . . . . . . . . . . . . . . . . . . . . . . 24
375		ifor 4135	. . . . . . . . . . . . . . . . . . . . . . . 24 $\/$
376	374, 375	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . 23 $\/$
377	369, 376	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . . 22 $\/$
378	377	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . 21 $\/$
379	366, 378	eqtr4i 2647	. . . . . . . . . . . . . . . . . . . 20 $\/$
380	8, 149, 150, 192, 210, 216, 360, 379	cantnfp1 8578	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $\/$ $/\$ CNF $\/$ CNF
381	380	simprd 479	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ CNF $\/$ CNF
382	318, 381	eqtrd 2656	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ CNF CNF
383	8, 9, 10, 2, 13, 113	cantnfsuc 8567	. . . . . . . . . . . . . . . . . . 19 $/\$
384	198, 383	syldan 487	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
385	161	simp3d 1075	. . . . . . . . . . . . . . . . . . . . . 22
386	385	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
387	108	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
388	129	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
389	137	adantrr 753	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
390		onsssuc 5813	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
391	388, 389, 390	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
392	147, 391	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
393	52	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
394		isorel 6576	. . . . . . . . . . . . . . . . . . . . . . . . 25 supp $/\$ $/\$
395	249, 393, 144, 394	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
396	252	epelc 5031	. . . . . . . . . . . . . . . . . . . . . . . 24
397	254	epelc 5031	. . . . . . . . . . . . . . . . . . . . . . . 24
398	395, 396, 397	3bitr3g 302	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
399	392, 398	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
400	387, 399	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
401		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . 23
402		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
403		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
404	402, 403	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . 23
405	401, 404	imbi12d 334	. . . . . . . . . . . . . . . . . . . . . 22
406	405	rspcv 3305	. . . . . . . . . . . . . . . . . . . . 21
407	210, 386, 400, 406	syl3c 66	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
408	407	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
409	408	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
410	384, 409	eqtr4d 2659	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
411	382, 410	eleq12d 2695	. . . . . . . . . . . . . . . 16 $/\$ $/\$ CNF CNF
412	222, 411	bitr4d 271	. . . . . . . . . . . . . . 15 $/\$ $/\$ CNF CNF
413	412	biimpd 219	. . . . . . . . . . . . . 14 $/\$ $/\$ CNF CNF
414	148, 413	embantd 59	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ CNF CNF
415	414	expr 643	. . . . . . . . . . . 12 $/\$ $/\$ CNF CNF
416	141, 415	sylbird 250	. . . . . . . . . . 11 $/\$ $/\$ CNF CNF
417		fveq2 6191	. . . . . . . . . . . . . . . . . . 19
418	417	sseq2d 3633	. . . . . . . . . . . . . . . . . 18
419	418	ifbid 4108	. . . . . . . . . . . . . . . . 17
420	419	mpteq2dv 4745	. . . . . . . . . . . . . . . 16
421	420	fveq2d 6195	. . . . . . . . . . . . . . 15 CNF CNF
422		suceq 5790	. . . . . . . . . . . . . . . 16
423	422	fveq2d 6195	. . . . . . . . . . . . . . 15
424	421, 423	eleq12d 2695	. . . . . . . . . . . . . 14 CNF CNF
425	115, 424	syl5ibcom 235	. . . . . . . . . . . . 13 CNF
426	425	adantr 481	. . . . . . . . . . . 12 $/\$ CNF
427	426	a1dd 50	. . . . . . . . . . 11 $/\$ $/\$ CNF CNF
428	416, 427	jaod 395	. . . . . . . . . 10 $/\$ $\/$ $/\$ CNF CNF
429	135, 428	sylbid 230	. . . . . . . . 9 $/\$ $/\$ CNF CNF
430	429	expimpd 629	. . . . . . . 8 $/\$ $/\$ CNF CNF
431	430	com23 86	. . . . . . 7 $/\$ CNF $/\$ CNF
432	431	a1i 11	. . . . . 6 $/\$ CNF $/\$ CNF
433	82, 94, 106, 127, 432	finds2 7094	. . . . 5 $/\$ CNF
434	70, 433	vtoclga 3272	. . . 4 $/\$ CNF
435	57, 434	mpcom 38	. . 3 $/\$ CNF
436	44, 54, 435	mp2and 715	. 2 CNF
437	156	feqmptd 6249	. . . 4
438		eqeq2 2633	. . . . . 6
439		eqeq2 2633	. . . . . 6
440		eqidd 2623	. . . . . 6 $/\$ $/\$
441	207	ffvelrni 6358	. . . . . . . . . . . . . 14 supp
442	44, 441	syl 17	. . . . . . . . . . . . 13 supp
443	205, 442	sseldd 3604	. . . . . . . . . . . 12
444		onelon 5748	. . . . . . . . . . . 12 $/\$
445	10, 443, 444	syl2anc 693	. . . . . . . . . . 11
446	445	adantr 481	. . . . . . . . . 10 $/\$
447		ontri1 5757	. . . . . . . . . 10 $/\$
448	232, 446, 447	syl2anc 693	. . . . . . . . 9 $/\$
449	448	con2bid 344	. . . . . . . 8 $/\$
450		simprl 794	. . . . . . . . . . 11 $/\$ $/\$
451	385	adantr 481	. . . . . . . . . . 11 $/\$ $/\$
452		eloni 5733	. . . . . . . . . . . . . . . . . 18
453	129, 452	syl 17	. . . . . . . . . . . . . . . . 17
454		orduni 6994	. . . . . . . . . . . . . . . . . 18
455	36, 454	ax-mp 5	. . . . . . . . . . . . . . . . 17
456		ordtri1 5756	. . . . . . . . . . . . . . . . 17 $/\$
457	453, 455, 456	sylancl 694	. . . . . . . . . . . . . . . 16
458	54, 457	mpbid 222	. . . . . . . . . . . . . . 15
459		isorel 6576	. . . . . . . . . . . . . . . . . 18 supp $/\$ $/\$
460	46, 44, 52, 459	syl12anc 1324	. . . . . . . . . . . . . . . . 17
461		fvex 6201	. . . . . . . . . . . . . . . . . 18
462	461	epelc 5031	. . . . . . . . . . . . . . . . 17
463		fvex 6201	. . . . . . . . . . . . . . . . . 18
464	463	epelc 5031	. . . . . . . . . . . . . . . . 17
465	460, 462, 464	3bitr3g 302	. . . . . . . . . . . . . . . 16
466	108	eleq2d 2687	. . . . . . . . . . . . . . . 16
467	465, 466	bitrd 268	. . . . . . . . . . . . . . 15
468	458, 467	mtbid 314	. . . . . . . . . . . . . 14
469		onelon 5748	. . . . . . . . . . . . . . . 16 $/\$
470	10, 162, 469	syl2anc 693	. . . . . . . . . . . . . . 15
471		ontri1 5757	. . . . . . . . . . . . . . 15 $/\$
472	470, 445, 471	syl2anc 693	. . . . . . . . . . . . . 14
473	468, 472	mpbird 247	. . . . . . . . . . . . 13
474	473	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$
475		simprr 796	. . . . . . . . . . . 12 $/\$ $/\$
476	470	adantr 481	. . . . . . . . . . . . 13 $/\$ $/\$
477	232	adantrr 753	. . . . . . . . . . . . 13 $/\$ $/\$
478		ontr2 5772	. . . . . . . . . . . . 13 $/\$ $/\$
479	476, 477, 478	syl2anc 693	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
480	474, 475, 479	mp2and 715	. . . . . . . . . . 11 $/\$ $/\$
481		eleq2 2690	. . . . . . . . . . . . 13
482		fveq2 6191	. . . . . . . . . . . . . 14
483		fveq2 6191	. . . . . . . . . . . . . 14
484	482, 483	eqeq12d 2637	. . . . . . . . . . . . 13
485	481, 484	imbi12d 334	. . . . . . . . . . . 12
486	485	rspcv 3305	. . . . . . . . . . 11
487	450, 451, 480, 486	syl3c 66	. . . . . . . . . 10 $/\$ $/\$
488	475	adantr 481	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ supp
489	46	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp supp
490	44	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
491	51	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ supp supp
492		ffvelrn 6357	. . . . . . . . . . . . . . . . . 18 supp $/\$ supp
493	491, 492	sylancom 701	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp
494		isorel 6576	. . . . . . . . . . . . . . . . 17 supp $/\$ $/\$
495	489, 490, 493, 494	syl12anc 1324	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ supp
496	278	epelc 5031	. . . . . . . . . . . . . . . 16
497	280	epelc 5031	. . . . . . . . . . . . . . . 16
498	495, 496, 497	3bitr3g 302	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ supp
499	48	ad2antrr 762	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ supp supp
500	499, 270	sylancom 701	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ supp
501	500	eleq2d 2687	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ supp
502	498, 501	bitrd 268	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ supp
503	488, 502	mpbird 247	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ supp
504		elssuni 4467	. . . . . . . . . . . . . . 15
505	493, 504	syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ supp
506	36, 493, 284	sylancr 695	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ supp
507	506, 286	syl 17	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ supp
508		ordtri1 5756	. . . . . . . . . . . . . . 15 $/\$
509	507, 455, 508	sylancl 694	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ supp
510	505, 509	mpbid 222	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ supp
511	503, 510	pm2.65da 600	. . . . . . . . . . . 12 $/\$ $/\$ supp
512	450, 511	eldifd 3585	. . . . . . . . . . 11 $/\$ $/\$ $\$ supp
513		ssid 3624	. . . . . . . . . . . . 13 supp supp
514	513	a1i 11	. . . . . . . . . . . 12 supp supp
515	160, 514, 10, 182	suppssr 7326	. . . . . . . . . . 11 $/\$ $\$ supp
516	512, 515	syldan 487	. . . . . . . . . 10 $/\$ $/\$
517	487, 516	eqtrd 2656	. . . . . . . . 9 $/\$ $/\$
518	517	expr 643	. . . . . . . 8 $/\$
519	449, 518	sylbird 250	. . . . . . 7 $/\$
520	519	imp 445	. . . . . 6 $/\$ $/\$
521	438, 439, 440, 520	ifbothda 4123	. . . . 5 $/\$
522	521	mpteq2dva 4744	. . . 4
523	437, 522	eqtrd 2656	. . 3
524	523	fveq2d 6195	. 2 CNF CNF
525	8, 9, 10, 2, 13, 113	cantnfval 8565	. . 3 CNF
526	43	fveq2d 6195	. . 3
527	525, 526	eqtrd 2656	. 2 CNF
528	436, 524, 527	3eltr4d 2716	1 CNF CNF

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200 $\$ cdif 3571

wss 3574

c0 3915

cif 4086

cuni 4436 class class class wbr 4653

copab 4712

cmpt 4729

wtr 4752

cep 5028

wwe 5072

ccnv 5113

cdm 5114

word 5722

con0 5723

wlim 5724

csuc 5725

wfun 5882

wfn 5883

wf 5884

wf1o 5887

cfv 5888

wiso 5889 (class class class)co 6650

cmpt2 6652

com 7065 supp csupp 7295 seq_𝜔cseqom 7542

c1o 7553

coa 7557

comu 7558

coe 7559

cen 7952 finSupp cfsupp 8275 OrdIsocoi 8414 CNF ccnf 8558

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-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 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-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 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-int 4476 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-se 5074 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-pred 5680 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-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-om 7066 df-1st 7168 df-2nd 7169 df-supp 7296 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-seqom 7543 df-1o 7560 df-2o 7561 df-oadd 7564 df-omul 7565 df-oexp 7566 df-er 7742 df-map 7859 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fsupp 8276 df-oi 8415 df-cnf 8559

This theorem is referenced by: cantnf 8590

W3C validator