tailfb - Mathbox for Jeff Hankins

	Mathbox for Jeff Hankins	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > tailfb		Structured version Unicode version

Theorem tailfb 28551

Description: The collection of tails of a directed set is a filter base. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)

**Hypothesis**
Ref	Expression
tailfb.1

**Assertion**
Ref	Expression
tailfb	$/\$

Proof of Theorem tailfb Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tailfb.1	. . . . 5
2	1	tailf 28549	. . . 4
3		frn 5560	. . . 4
4	2, 3	syl 16	. . 3
5	4	adantr 465	. 2 $/\$
6		n0 3641	. . . . 5
7		ffn 5554	. . . . . . . 8
8		fnfvelrn 5835	. . . . . . . . 9 $/\$
9	8	ex 434	. . . . . . . 8
10	2, 7, 9	3syl 20	. . . . . . 7
11		ne0i 3638	. . . . . . 7
12	10, 11	syl6 33	. . . . . 6
13	12	exlimdv 1690	. . . . 5
14	6, 13	syl5bi 217	. . . 4
15	14	imp 429	. . 3 $/\$
16	1	tailini 28550	. . . . . . . 8 $/\$
17		n0i 3637	. . . . . . . 8
18	16, 17	syl 16	. . . . . . 7 $/\$
19	18	nrexdv 2814	. . . . . 6
20	19	adantr 465	. . . . 5 $/\$
21		fvelrnb 5734	. . . . . . 7
22	2, 7, 21	3syl 20	. . . . . 6
23	22	adantr 465	. . . . 5 $/\$
24	20, 23	mtbird 301	. . . 4 $/\$
25		df-nel 2604	. . . 4
26	24, 25	sylibr 212	. . 3 $/\$
27		fvelrnb 5734	. . . . . . . 8
28		fvelrnb 5734	. . . . . . . 8
29	27, 28	anbi12d 710	. . . . . . 7 $/\$ $/\$
30	2, 7, 29	3syl 20	. . . . . 6 $/\$ $/\$
31		reeanv 2883	. . . . . . 7 $/\$ $/\$
32	1	dirge 15399	. . . . . . . . . . 11 $/\$ $/\$ $/\$
33	32	3expb 1188	. . . . . . . . . 10 $/\$ $/\$ $/\$
34	2, 7	syl 16	. . . . . . . . . . . . 13
35		fnfvelrn 5835	. . . . . . . . . . . . 13 $/\$
36	34, 35	sylan 471	. . . . . . . . . . . 12 $/\$
37	36	ad2ant2r 746	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
38		vex 2970	. . . . . . . . . . . . . . . . . . . . . 22
39		dirtr 15398	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
40	39	exp32 605	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
41	38, 40	mpan2 671	. . . . . . . . . . . . . . . . . . . . 21
42	41	com23 78	. . . . . . . . . . . . . . . . . . . 20
43	42	imp 429	. . . . . . . . . . . . . . . . . . 19 $/\$
44	43	ad2ant2rl 748	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
45		dirtr 15398	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$
46	45	exp32 605	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
47	38, 46	mpan2 671	. . . . . . . . . . . . . . . . . . . . 21
48	47	com23 78	. . . . . . . . . . . . . . . . . . . 20
49	48	imp 429	. . . . . . . . . . . . . . . . . . 19 $/\$
50	49	ad2ant2rl 748	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
51	44, 50	anim12d 563	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
52	51	expr 615	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$
53	52	com23 78	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
54	53	impr 619	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
55	1	eltail 28548	. . . . . . . . . . . . . . . 16 $/\$ $/\$
56	38, 55	mp3an3 1303	. . . . . . . . . . . . . . 15 $/\$
57	56	ad2ant2r 746	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
58	1	eltail 28548	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
59	38, 58	mp3an3 1303	. . . . . . . . . . . . . . . . 17 $/\$
60	59	adantrr 716	. . . . . . . . . . . . . . . 16 $/\$ $/\$
61	1	eltail 28548	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
62	38, 61	mp3an3 1303	. . . . . . . . . . . . . . . . 17 $/\$
63	62	adantrl 715	. . . . . . . . . . . . . . . 16 $/\$ $/\$
64	60, 63	anbi12d 710	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
65	64	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
66	54, 57, 65	3imtr4d 268	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67		elin 3534	. . . . . . . . . . . . 13 $/\$
68	66, 67	syl6ibr 227	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
69	68	ssrdv 3357	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
70		sseq1 3372	. . . . . . . . . . . 12
71	70	rspcev 3068	. . . . . . . . . . 11 $/\$
72	37, 69, 71	syl2anc 661	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
73	33, 72	rexlimddv 2840	. . . . . . . . 9 $/\$ $/\$
74		ineq1 3540	. . . . . . . . . . . 12
75	74	sseq2d 3379	. . . . . . . . . . 11
76	75	rexbidv 2731	. . . . . . . . . 10
77		ineq2 3541	. . . . . . . . . . . 12
78	77	sseq2d 3379	. . . . . . . . . . 11
79	78	rexbidv 2731	. . . . . . . . . 10
80	76, 79	sylan9bb 699	. . . . . . . . 9 $/\$
81	73, 80	syl5ibcom 220	. . . . . . . 8 $/\$ $/\$ $/\$
82	81	rexlimdvva 2843	. . . . . . 7 $/\$
83	31, 82	syl5bir 218	. . . . . 6 $/\$
84	30, 83	sylbid 215	. . . . 5 $/\$
85	84	adantr 465	. . . 4 $/\$ $/\$
86	85	ralrimivv 2802	. . 3 $/\$
87	15, 26, 86	3jca 1168	. 2 $/\$ $/\$ $/\$
88		dmexg 6504	. . . . 5
89	1, 88	syl5eqel 2522	. . . 4
90	89	adantr 465	. . 3 $/\$
91		isfbas2 19383	. . 3 $/\$ $/\$ $/\$
92	90, 91	syl 16	. 2 $/\$ $/\$ $/\$ $/\$
93	5, 87, 92	mpbir2and 913	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wex 1586

wcel 1756

wne 2601

wnel 2602

wral 2710

wrex 2711

cvv 2967

cin 3322

wss 3323

c0 3632

cpw 3855 class class class wbr 4287

cdm 4835

crn 4836

wfn 5408

wf 5409

cfv 5413

cdir 15390

ctail 15391

cfbas 17779

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-op 3879 df-uni 4087 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-id 4631 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-dir 15392 df-tail 15393 df-fbas 17789

This theorem is referenced by: filnetlem4 28555

W3C validator