neibastop2lem4 - Mathbox for Jeff Hankins

Mathbox for Jeff Hankins

< Previous Next >
Related theorems
Unicode version

Theorem neibastop2lem4 15522

Description: Lemma for neibastop2 15523.

**Hypotheses**
Ref	Expression
neibastop1.1
neibastop2.1	$/\$
neibastop2.2	$/\$

**Assertion**
Ref	Expression
neibastop2lem4	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$

Distinct variable groups:

**Proof of Theorem neibastop2lem4**
Step	Hyp	Ref	Expression
1		neibastop1.1	. . . . . . . . . . 11
2		neibastop2.1	. . . . . . . . . . 11 $/\$
3		neibastop2.2	. . . . . . . . . . 11 $/\$
4	1, 2, 3	neibastop2lem2 15520	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
5		sstr 2625	. . . . . . . . . . . . 13 $/\$
6	5	ancoms 484	. . . . . . . . . . . 12 $/\$
7		simprlr 457	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
8	6, 7	sylan 497	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$
9		ax-17 1317	. . . . . . . . . . . . . 14
10		hbra1 2147	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11	9, 10	hban 1356	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
12		eleq2 1958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
13	12	imbi1d 675	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
14	13	imbi2d 674	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
15		peano2 3972	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
16	15	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
17	1, 2, 3	neibastop2lem3 15521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
18	17	exp44 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
19	18	exp5c 15335	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20	19	r19.23adv 2215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
21		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
22	21	cbvrexv 2281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
23	20, 22	syl5ib 223	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24	23	com24 41	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
25	24	imp511 15334	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	3	fveq1i 4682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$
27	26	imaeq2i 4262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$
28	27	unieqi 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$
29	28	sseq2i 2642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$
30	29	rexbii 2128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$
31		funopabeq 4456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$
32		eqid 1884	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$
33		rexeq 2267	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$
34	33	abbidv 2008	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$
35	34	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
36		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
37	35, 36	sylan9bb 599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
38	37	cbvopabv 3404	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
39	38	eleq2i 1961	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$
40		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42
41		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
42		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
43	41, 42	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 $/\$ $/\$
44	43	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
45	44	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$ $/\$
46	45	cbvabv 2420	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$ $/\$
47		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54
48		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
49	48	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 $/\$ $/\$
50	47, 49	rexeqbidv 2275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 $/\$ $/\$
51	50	cbvrexv 2281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$ $/\$
52	51	abbii 2006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$ $/\$
53	46, 52	eqtri 1908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$ $/\$
54	53	eqeq2i 1894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$
55	54	opabbii 3402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 $/\$ $/\$
56	3, 55	eqtri 1908	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$
57		rdgeq1 5142	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$ $/\$
58	56, 57	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$
59	58	fveq1i 4682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
60		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
61		hbre1 2150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 $/\$ $/\$
62	61	hbab 1875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 $/\$ $/\$
63	60, 62	hbeq 1995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$ $/\$
64	63	hbopab 3560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$
65	3, 64	hbxfr 1992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
66		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
67	65, 66	hbrdg 5144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
68		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
69	67, 68	hbfv 4686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
70		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$ $/\$
71	69, 70	rexeqf 2264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$ $/\$ $/\$ $/\$
72	59, 71	ax-mp 7	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$ $/\$
73	72	abbii 2006	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$ $/\$
74		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
75		fvex 4689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
76		df-pw 3035	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
77		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48
78	77	pwex 3487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
79	76, 78	eqeltrri 1968	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
80		simpr 350	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 $/\$
81	80	ss2abi 2679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 $/\$
82	79, 81	ssexi 3456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 $/\$
83	75, 82	abrexex2 4847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$
84	74, 83	abrexex2 4847	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$
85	73, 84	eqeltri 1967	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$
86		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
87		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50
88		hbab1 1874	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 $/\$ $/\$
89	87, 88	hbeq 1995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 $/\$ $/\$
90	89	hbopab 3560	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 $/\$ $/\$
91	3, 90	hbxfr 1992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
92		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
93	91, 92	hbrdg 5144	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
94		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
95	93, 94	hbfv 4686	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
96	86, 95	hbeq 1995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44
97		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
98	97, 69	rexeqf 2264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 $/\$ $/\$
99	96, 98	abbid 2007	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 $/\$ $/\$
100	99	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$
101		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 $/\$ $/\$ $/\$ $/\$
102	40, 85, 100, 101	opelopab 3570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 $/\$ $/\$ $/\$ $/\$
103	39, 102	bitri 190	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 $/\$ $/\$ $/\$ $/\$
104	32, 103	mpbir 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$
105	85	funopfv 4710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 $/\$ $/\$ $/\$ $/\$ $/\$
106	31, 104, 105	mp2 54	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 $/\$ $/\$
107	106	imaeq2i 4262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 $/\$ $/\$
108	107	unieqi 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 $/\$ $/\$
109	108	sseq2i 2642	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 $/\$ $/\$
110	109	rexbii 2128	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 $/\$ $/\$
111	30, 110	bitr2i 191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
112	25, 111	sylib 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
113		nnon 3957	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
114		rdgsuc 5153	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38
115	113, 114	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
116	115	imaeq2d 4264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
117	116	unieqd 3188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
118	117	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
119	118	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
120	119	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
121	112, 120	mpbird 213	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
122		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
123	122	imaeq2d 4264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
124	123	unieqd 3188	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
125	124	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
126	125	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
127	126	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
128	16, 121, 127	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
129	128	ex 402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
130		rexcom 2243	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
131	129, 130	syl6ib 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
132		ssiun 3293	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
133	132	reximi 2198	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
134	131, 133	syl6 25	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
135	134	exp4c 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
136		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
137		eleq1 1957	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
138	1	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
139	138	eqcoms 1887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
140	139	rexeqdv 2270	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
141	137, 140	anbi12d 690	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
142	136, 141	elab 2403	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
143	135, 142	syl7ib 233	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
144	14, 143	syl5cbir 228	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
145	144	com23 36	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
146	145	imp3a 388	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
147	2	eleq2i 1961	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
148		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . 25
149		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . 25
150		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
151	150	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
152	151	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
153	152	abbidv 2008	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
154	153	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
155		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
156	148, 149, 154, 155	opelopab 3570	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
157	147, 156	bitri 190	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
158	157	anbi2i 538	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
159	146, 158	syl5ib 223	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
160	159	19.23adv 1584	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
161	160	com23 36	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
162	161	imp3a 388	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
163	162	19.23adv 1584	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
164		eluni 3180	. . . . . . . . . . . . . . . . . 18 $/\$
165	149	elima3 4272	. . . . . . . . . . . . . . . . . . . 20 $/\$
166	165	anbi2i 538	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
167	166	exbii 1398	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
168	164, 167	bitri 190	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
169	163, 168	syl5ib 223	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
170	169	com23 36	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
171	170	r19.23adv 2215	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
172		eliun 3259	. . . . . . . . . . . . . . 15
173		fveq2 4681	. . . . . . . . . . . . . . . . . . 19
174	173	imaeq2d 4264	. . . . . . . . . . . . . . . . . 18
175	174	unieqd 3188	. . . . . . . . . . . . . . . . 17
176	175	eleq2d 1964	. . . . . . . . . . . . . . . 16
177	176	cbvrexv 2281	. . . . . . . . . . . . . . 15
178	172, 177	bitri 190	. . . . . . . . . . . . . 14
179	171, 178	syl5ib 223	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
180	11, 179	r19.21ai 2174	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
181	180	ad2antrr 440	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$
182	139	rexeqdv 2270	. . . . . . . . . . . . . . . . . . . 20
183	137, 182	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
184	136, 183	elab 2403	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
185		simplr 449	. . . . . . . . . . . . . . . . . . 19 $/\$ Top $/\$ $/\$
186	185	ad2antrl 442	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
187		ssid 2634	. . . . . . . . . . . . . . . . . . . . 21
188		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . 22
189	188	rcla4ev 2381	. . . . . . . . . . . . . . . . . . . . 21 $/\$
190	187, 189	mpan2 760	. . . . . . . . . . . . . . . . . . . 20
191	190	adantr 425	. . . . . . . . . . . . . . . . . . 19 $/\$
192	191	ad2antll 443	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
193	184, 186, 192	sylanbrc 527	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$
194		rabexg 3460	. . . . . . . . . . . . . . . . . . . . 21
195		df-rab 2112	. . . . . . . . . . . . . . . . . . . . 21 $/\$
196	194, 195	syl5eqelr 1976	. . . . . . . . . . . . . . . . . . . 20 $/\$
197	196	ad2antrr 440	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$
198		funopabeq 4456	. . . . . . . . . . . . . . . . . . . 20 $/\$
199		funeq 4441	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
200	2, 199	ax-mp 7	. . . . . . . . . . . . . . . . . . . 20 $/\$
201	198, 200	mpbir 207	. . . . . . . . . . . . . . . . . . 19
202	197, 201	jctir 317	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
203		eqid 1884	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
204		visset 2295	. . . . . . . . . . . . . . . . . . . . . 22
205		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
206	205	rexbidv 2124	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
207	206	anbi2d 678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
208	207	abbidv 2008	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
209	208	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
210		eqeq1 1890	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
211	209, 210	opelopabg 3567	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
212	2	eleq2i 1961	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
213	211, 212	syl5bb 591	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$ $/\$
214	204, 213	mpan 759	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
215	196, 214	syl 12	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
216	203, 215	mpbiri 211	. . . . . . . . . . . . . . . . . . 19 $/\$
217	216	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$
218		funopfvg 4711	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
219	202, 217, 218	sylc 83	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$
220	193, 219	eleqtrrd 1974	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
221		rabexg 3460	. . . . . . . . . . . . . . . . . . . . . . 23
222		df-rab 2112	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
223	221, 222	syl5eqelr 1976	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
224	223	a1d 15	. . . . . . . . . . . . . . . . . . . . 21 $/\$
225	224	r19.21aiv 2175	. . . . . . . . . . . . . . . . . . . 20 $/\$
226		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . 24
227	226	biantrur 794	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
228	227	opabbii 3402	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$
229	2, 228	eqtri 1908	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
230	229	fnopab2g 4547	. . . . . . . . . . . . . . . . . . . 20 $/\$
231	225, 230	sylib 215	. . . . . . . . . . . . . . . . . . 19
232		fnsnfv 4728	. . . . . . . . . . . . . . . . . . . . 21 $/\$
233	232	unieqd 3188	. . . . . . . . . . . . . . . . . . . 20 $/\$
234	204, 233	mpan2 760	. . . . . . . . . . . . . . . . . . 19
235	231, 234	syl 12	. . . . . . . . . . . . . . . . . 18
236	235	ad2antrr 440	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
237		fvex 4689	. . . . . . . . . . . . . . . . . 18
238	237	unisn 3193	. . . . . . . . . . . . . . . . 17
239	236, 238	syl5eqr 1942	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
240	220, 239	eleqtrd 1973	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
241		snex 3492	. . . . . . . . . . . . . . . . . 18
242	241	rdg0 5149	. . . . . . . . . . . . . . . . 17
243	242	imaeq2i 4262	. . . . . . . . . . . . . . . 16
244	243	unieqi 3187	. . . . . . . . . . . . . . 15
245	240, 244	syl6eleqr 1982	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
246		peano1 3971	. . . . . . . . . . . . . . 15
247		fveq2 4681	. . . . . . . . . . . . . . . . . . 19
248	247	imaeq2d 4264	. . . . . . . . . . . . . . . . . 18
249	248	unieqd 3188	. . . . . . . . . . . . . . . . 17
250	249	eleq2d 1964	. . . . . . . . . . . . . . . 16
251	250	rcla4ev 2381	. . . . . . . . . . . . . . 15 $/\$
252	246, 251	mpan 759	. . . . . . . . . . . . . 14
253	245, 252	syl 12	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
254	253, 172	sylibr 217	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
255	254	anim1i 361	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
256	8, 181, 255	jca31 311	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
257	4, 256	mpdan 768	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
258		omex 5733	. . . . . . . . . . . 12
259		fvex 4689	. . . . . . . . . . . . . . 15
260	259	funimaex 4496	. . . . . . . . . . . . . 14
261	201, 260	ax-mp 7	. . . . . . . . . . . . 13
262	261	uniex 3794	. . . . . . . . . . . 12
263	258, 262	iunex 4839	. . . . . . . . . . 11
264		sseq1 2637	. . . . . . . . . . . 12
265		ax-17 1317	. . . . . . . . . . . . . 14
266		ax-17 1317	. . . . . . . . . . . . . . . 16
267		ax-17 1317	. . . . . . . . . . . . . . . . . 18
268		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . 23
269		ax-17 1317	. . . . . . . . . . . . . . . . . . . . . . . . 25
270		hbre1 2150	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
271	269, 270	hbrex 2149	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
272	271	hbab 1875	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
273	268, 272	hbeq 1995	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
274	273	hbopab 3560	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
275	3, 274	hbxfr 1992	. . . . . . . . . . . . . . . . . . . 20
276		ax-17 1317	. . . . . . . . . . . . . . . . . . . 20
277	275, 276	hbrdg 5144	. . . . . . . . . . . . . . . . . . 19
278		ax-17 1317	. . . . . . . . . . . . . . . . . . 19
279	277, 278	hbfv 4686	. . . . . . . . . . . . . . . . . 18
280	267, 279	hbima 4273	. . . . . . . . . . . . . . . . 17
281	280	hbuni 3183	. . . . . . . . . . . . . . . 16
282	266, 281	hbrex 2149	. . . . . . . . . . . . . . 15
283		eliun 3259	. . . . . . . . . . . . . . 15
284	283	albii 1346	. . . . . . . . . . . . . . 15
285	282, 283, 284	3imtr4i 236	. . . . . . . . . . . . . 14
286	265, 285	raleqf 2263	. . . . . . . . . . . . 13
287	265, 285	hbeq 1995	. . . . . . . . . . . . . 14
288		sseq2 2639	. . . . . . . . . . . . . . 15
289	288	rexbidv 2124	. . . . . . . . . . . . . 14
290	287, 289	ralbid 2121	. . . . . . . . . . . . 13
291	286, 290	bitrd 587	. . . . . . . . . . . 12
292	264, 291	anbi12d 690	. . . . . . . . . . 11 $/\$ $/\$
293	263, 292	elab 2403	. . . . . . . . . 10 $/\$ $/\$
294	293	anbi1i 539	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
295	257, 294	sylibr 217	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
296		eleq2 1958	. . . . . . . . . 10
297		sseq1 2637	. . . . . . . . . 10
298	296, 297	anbi12d 690	. . . . . . . . 9 $/\$ $/\$
299	298	rcla4ev 2381	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
300	295, 299	syl 12	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
301	300	expr 418	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$
302	301	exp3a 405	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
303	302	r19.23adv 2215	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
304	303	expr 418	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$
305	304	imp3a 388	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$
306	305	impr 422	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ Top $/\$ $/\$ $/\$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wi 3

wb 163 $/\$ wa 240

wal 1296

wceq 1298

wcel 1300

wex 1326

cab 1871

wne 2017

wral 2105

wrex 2106

crab 2108

cvv 2292

cin 2592

wss 2593

c0 2875

cpw 3032

csn 3044

cop 3046

cuni 3177

ciun 3255

copab 3395

con0 3657

csuc 3659

com 3949

cima 3989

wfun 3992

wfn 3993

cfv 3998

crdg 5139 Topctop 8857

This theorem is referenced by: neibastop2 15523

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-rep 3428 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 ax-inf2 5731

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-rab 2112 df-v 2294 df-sbc 2454 df-csb 2541 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-if 2983 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-iun 3257 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-id 3586 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-lim 3662 df-suc 3663 df-om 3950 df-xp 4000 df-rel 4001 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-fv 4014 df-rdg 5140