tailfb - Mathbox for Jeff Hankins

Mathbox for Jeff Hankins

< Previous Next >
Related theorems
Unicode version

Theorem tailfb 15639

Description: The collection of tails of a directed set is a filter base.

**Hypothesis**
Ref	Expression
tailfb.1

**Assertion**
Ref	Expression
tailfb	Dir $/\$ tail fBas

**Proof of Theorem tailfb**
Step	Hyp	Ref	Expression
1		tailfb.1	. . . . . . . . 9
2	1	tailmap 15636	. . . . . . . 8 Dir tail
3		ffn 4562	. . . . . . . 8 tail tail
4		fnfvelrn 4786	. . . . . . . . 9 tail $/\$ tail tail
5	4	ex 402	. . . . . . . 8 tail tail tail
6	2, 3, 5	3syl 24	. . . . . . 7 Dir tail tail
7		ne0i 2881	. . . . . . 7 tail tail tail
8	6, 7	syl6 25	. . . . . 6 Dir tail
9	8	19.23adv 1584	. . . . 5 Dir tail
10		n0 2884	. . . . 5
11	9, 10	syl5ib 223	. . . 4 Dir tail
12	11	imp 377	. . 3 Dir $/\$ tail
13	1	tailini 15637	. . . . . . . 8 Dir $/\$ tail
14		n0i 2880	. . . . . . . 8 tail tail
15	13, 14	syl 12	. . . . . . 7 Dir $/\$ tail
16	15	nrexdv 2193	. . . . . 6 Dir tail
17	16	adantr 425	. . . . 5 Dir $/\$ tail
18		fvelrnb 4719	. . . . . . 7 tail tail tail
19	2, 3, 18	3syl 24	. . . . . 6 Dir tail tail
20	19	adantr 425	. . . . 5 Dir $/\$ tail tail
21	17, 20	mtbird 783	. . . 4 Dir $/\$ tail
22		df-nel 2020	. . . 4 tail tail
23	21, 22	sylibr 217	. . 3 Dir $/\$ tail
24		fvelrnb 4719	. . . . . . . 8 tail tail tail
25		fvelrnb 4719	. . . . . . . 8 tail tail tail
26	24, 25	anbi12d 690	. . . . . . 7 tail tail $/\$ tail tail $/\$ tail
27	2, 3, 26	3syl 24	. . . . . 6 Dir tail $/\$ tail tail $/\$ tail
28		ineq1 2789	. . . . . . . . . . . . 13 tail tail tail tail
29	28	sseq2d 2645	. . . . . . . . . . . 12 tail tail tail tail
30	29	rexbidv 2124	. . . . . . . . . . 11 tail tail tail tail tail tail
31		ineq2 2790	. . . . . . . . . . . . 13 tail tail
32	31	sseq2d 2645	. . . . . . . . . . . 12 tail tail
33	32	rexbidv 2124	. . . . . . . . . . 11 tail tail tail tail
34	30, 33	sylan9bb 599	. . . . . . . . . 10 tail $/\$ tail tail tail tail tail
35	1	dirge 10357	. . . . . . . . . . . 12 Dir $/\$ $/\$ $/\$
36	35	3expb 1068	. . . . . . . . . . 11 Dir $/\$ $/\$ $/\$
37		fnfvelrn 4786	. . . . . . . . . . . . . . . 16 tail $/\$ tail tail
38	2, 3	syl 12	. . . . . . . . . . . . . . . 16 Dir tail
39	37, 38	sylan 497	. . . . . . . . . . . . . . 15 Dir $/\$ tail tail
40	39	ad2ant2r 445	. . . . . . . . . . . . . 14 Dir $/\$ $/\$ $/\$ $/\$ $/\$ tail tail
41		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . . 25
42		dirtr 10356	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Dir $/\$ $/\$ $/\$
43	42	exp32 408	. . . . . . . . . . . . . . . . . . . . . . . . 25 Dir $/\$
44	41, 43	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . 24 Dir
45	44	com23 36	. . . . . . . . . . . . . . . . . . . . . . 23 Dir
46	45	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 Dir $/\$
47	46	ad2ant2rl 447	. . . . . . . . . . . . . . . . . . . . 21 Dir $/\$ $/\$ $/\$ $/\$
48		dirtr 10356	. . . . . . . . . . . . . . . . . . . . . . . . . 26 Dir $/\$ $/\$ $/\$
49	48	exp32 408	. . . . . . . . . . . . . . . . . . . . . . . . 25 Dir $/\$
50	41, 49	mpan2 760	. . . . . . . . . . . . . . . . . . . . . . . 24 Dir
51	50	com23 36	. . . . . . . . . . . . . . . . . . . . . . 23 Dir
52	51	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 Dir $/\$
53	52	ad2ant2rl 447	. . . . . . . . . . . . . . . . . . . . 21 Dir $/\$ $/\$ $/\$ $/\$
54	47, 53	anim12d 617	. . . . . . . . . . . . . . . . . . . 20 Dir $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	54	expr 418	. . . . . . . . . . . . . . . . . . 19 Dir $/\$ $/\$ $/\$ $/\$ $/\$
56	55	com23 36	. . . . . . . . . . . . . . . . . 18 Dir $/\$ $/\$ $/\$ $/\$ $/\$
57	56	impr 422	. . . . . . . . . . . . . . . . 17 Dir $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
58	1	eltail 15635	. . . . . . . . . . . . . . . . . . 19 Dir $/\$ $/\$ tail
59	41, 58	mp3an3 1180	. . . . . . . . . . . . . . . . . 18 Dir $/\$ tail
60	59	ad2ant2r 445	. . . . . . . . . . . . . . . . 17 Dir $/\$ $/\$ $/\$ $/\$ $/\$ tail
61	1	eltail 15635	. . . . . . . . . . . . . . . . . . . . 21 Dir $/\$ $/\$ tail
62	41, 61	mp3an3 1180	. . . . . . . . . . . . . . . . . . . 20 Dir $/\$ tail
63	62	adantrr 431	. . . . . . . . . . . . . . . . . . 19 Dir $/\$ $/\$ tail
64	1	eltail 15635	. . . . . . . . . . . . . . . . . . . . 21 Dir $/\$ $/\$ tail
65	41, 64	mp3an3 1180	. . . . . . . . . . . . . . . . . . . 20 Dir $/\$ tail
66	65	adantrl 430	. . . . . . . . . . . . . . . . . . 19 Dir $/\$ $/\$ tail
67	63, 66	anbi12d 690	. . . . . . . . . . . . . . . . . 18 Dir $/\$ $/\$ tail $/\$ tail $/\$
68	67	adantr 425	. . . . . . . . . . . . . . . . 17 Dir $/\$ $/\$ $/\$ $/\$ $/\$ tail $/\$ tail $/\$
69	57, 60, 68	3imtr4d 602	. . . . . . . . . . . . . . . 16 Dir $/\$ $/\$ $/\$ $/\$ $/\$ tail tail $/\$ tail
70		elin 2786	. . . . . . . . . . . . . . . 16 tail tail tail $/\$ tail
71	69, 70	syl6ibr 230	. . . . . . . . . . . . . . 15 Dir $/\$ $/\$ $/\$ $/\$ $/\$ tail tail tail
72	71	ssrdv 2622	. . . . . . . . . . . . . 14 Dir $/\$ $/\$ $/\$ $/\$ $/\$ tail tail tail
73		sseq1 2637	. . . . . . . . . . . . . . 15 tail tail tail tail tail tail
74	73	rcla4ev 2381	. . . . . . . . . . . . . 14 tail tail $/\$ tail tail tail tail tail tail
75	40, 72, 74	syl11anc 524	. . . . . . . . . . . . 13 Dir $/\$ $/\$ $/\$ $/\$ $/\$ tail tail tail
76	75	exp32 408	. . . . . . . . . . . 12 Dir $/\$ $/\$ $/\$ tail tail tail
77	76	r19.23adv 2215	. . . . . . . . . . 11 Dir $/\$ $/\$ $/\$ tail tail tail
78	36, 77	mpd 29	. . . . . . . . . 10 Dir $/\$ $/\$ tail tail tail
79	34, 78	syl5cbi 226	. . . . . . . . 9 Dir $/\$ $/\$ tail $/\$ tail tail
80	79	ex 402	. . . . . . . 8 Dir $/\$ tail $/\$ tail tail
81	80	r19.23advv 2218	. . . . . . 7 Dir tail $/\$ tail tail
82		reeanv 2249	. . . . . . 7 tail $/\$ tail tail $/\$ tail
83	81, 82	syl5ibr 224	. . . . . 6 Dir tail $/\$ tail tail
84	27, 83	sylbid 220	. . . . 5 Dir tail $/\$ tail tail
85	84	adantr 425	. . . 4 Dir $/\$ tail $/\$ tail tail
86	85	r19.21aivv 2183	. . 3 Dir $/\$ tail tail tail
87	12, 23, 86	3jca 1050	. 2 Dir $/\$ tail $/\$ tail $/\$ tail tail tail
88		fvex 4689	. . . 4 tail
89	88	rnex 4209	. . 3 tail
90		isfbas2 10263	. . 3 tail tail fBas tail $/\$ tail $/\$ tail tail tail
91	89, 90	ax-mp 7	. 2 tail fBas tail $/\$ tail $/\$ tail tail tail
92	87, 91	sylibr 217	1 Dir $/\$ tail fBas

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 163 $/\$ wa 240 $/\$ w3a 858

wceq 1298

wcel 1300

wex 1326

wne 2017

wnel 2018

wral 2105

wrex 2106

cvv 2292

cin 2592

wss 2593

c0 2875

cpw 3032 class class class wbr 3338

cdm 3986

crn 3987

wfn 3993

wf 3994

cfv 3998 fBascfbas 10257 Dircdir 10348 tailctail 10349

This theorem is referenced by: filnet 15645

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

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 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-nel 2020 df-ral 2109 df-rex 2110 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-id 3586 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-f 4010 df-fv 4014 df-fbas 10259 df-dir 10350 df-tail 10351