Metamath Proof Explorer

Theorem tailfb

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)

Ref Expression
Hypothesis tailfb.1 ⊢X=dom⁡D
Assertion tailfb ⊢D∈DirRel∧X≠∅→ran⁡tail⁡D∈fBas⁡X

Proof

Step Hyp Ref Expression
1 tailfb.1 ⊢X=dom⁡D
2 1 tailf ⊢D∈DirRel→tail⁡D:X⟶𝒫X
3 2 frnd ⊢D∈DirRel→ran⁡tail⁡D⊆𝒫X
4 3 adantr ⊢D∈DirRel∧X≠∅→ran⁡tail⁡D⊆𝒫X
5 n0 ⊢X≠∅↔∃xx∈X
6 ffn ⊢tail⁡D:X⟶𝒫X→tail⁡DFnX
7 fnfvelrn ⊢tail⁡DFnX∧x∈X→tail⁡D⁡x∈ran⁡tail⁡D
8 7 ex ⊢tail⁡DFnX→x∈X→tail⁡D⁡x∈ran⁡tail⁡D
9 2 6 8 3syl ⊢D∈DirRel→x∈X→tail⁡D⁡x∈ran⁡tail⁡D
10 ne0i ⊢tail⁡D⁡x∈ran⁡tail⁡D→ran⁡tail⁡D≠∅
11 9 10 syl6 ⊢D∈DirRel→x∈X→ran⁡tail⁡D≠∅
12 11 exlimdv ⊢D∈DirRel→∃xx∈X→ran⁡tail⁡D≠∅
13 5 12 biimtrid ⊢D∈DirRel→X≠∅→ran⁡tail⁡D≠∅
14 13 imp ⊢D∈DirRel∧X≠∅→ran⁡tail⁡D≠∅
15 1 tailini ⊢D∈DirRel∧x∈X→x∈tail⁡D⁡x
16 n0i ⊢x∈tail⁡D⁡x→¬tail⁡D⁡x=∅
17 15 16 syl ⊢D∈DirRel∧x∈X→¬tail⁡D⁡x=∅
18 17 nrexdv ⊢D∈DirRel→¬∃x∈Xtail⁡D⁡x=∅
19 18 adantr ⊢D∈DirRel∧X≠∅→¬∃x∈Xtail⁡D⁡x=∅
20 fvelrnb ⊢tail⁡DFnX→∅∈ran⁡tail⁡D↔∃x∈Xtail⁡D⁡x=∅
21 2 6 20 3syl ⊢D∈DirRel→∅∈ran⁡tail⁡D↔∃x∈Xtail⁡D⁡x=∅
22 21 adantr ⊢D∈DirRel∧X≠∅→∅∈ran⁡tail⁡D↔∃x∈Xtail⁡D⁡x=∅
23 19 22 mtbird ⊢D∈DirRel∧X≠∅→¬∅∈ran⁡tail⁡D
24 df-nel ⊢∅∉ran⁡tail⁡D↔¬∅∈ran⁡tail⁡D
25 23 24 sylibr ⊢D∈DirRel∧X≠∅→∅∉ran⁡tail⁡D
26 fvelrnb ⊢tail⁡DFnX→x∈ran⁡tail⁡D↔∃u∈Xtail⁡D⁡u=x
27 fvelrnb ⊢tail⁡DFnX→y∈ran⁡tail⁡D↔∃v∈Xtail⁡D⁡v=y
28 26 27 anbi12d ⊢tail⁡DFnX→x∈ran⁡tail⁡D∧y∈ran⁡tail⁡D↔∃u∈Xtail⁡D⁡u=x∧∃v∈Xtail⁡D⁡v=y
29 2 6 28 3syl ⊢D∈DirRel→x∈ran⁡tail⁡D∧y∈ran⁡tail⁡D↔∃u∈Xtail⁡D⁡u=x∧∃v∈Xtail⁡D⁡v=y
30 reeanv ⊢∃u∈X∃v∈Xtail⁡D⁡u=x∧tail⁡D⁡v=y↔∃u∈Xtail⁡D⁡u=x∧∃v∈Xtail⁡D⁡v=y
31 1 dirge ⊢D∈DirRel∧u∈X∧v∈X→∃w∈XuDw∧vDw
32 31 3expb ⊢D∈DirRel∧u∈X∧v∈X→∃w∈XuDw∧vDw
33 2 6 syl ⊢D∈DirRel→tail⁡DFnX
34 fnfvelrn ⊢tail⁡DFnX∧w∈X→tail⁡D⁡w∈ran⁡tail⁡D
35 33 34 sylan ⊢D∈DirRel∧w∈X→tail⁡D⁡w∈ran⁡tail⁡D
36 35 ad2ant2r ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧uDw∧vDw→tail⁡D⁡w∈ran⁡tail⁡D
37 dirtr ⊢D∈DirRel∧x∈V∧uDw∧wDx→uDx
38 37 exp32 ⊢D∈DirRel∧x∈V→uDw→wDx→uDx
39 38 elvd ⊢D∈DirRel→uDw→wDx→uDx
40 39 com23 ⊢D∈DirRel→wDx→uDw→uDx
41 40 imp ⊢D∈DirRel∧wDx→uDw→uDx
42 41 ad2ant2rl ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧wDx→uDw→uDx
43 dirtr ⊢D∈DirRel∧x∈V∧vDw∧wDx→vDx
44 43 exp32 ⊢D∈DirRel∧x∈V→vDw→wDx→vDx
45 44 elvd ⊢D∈DirRel→vDw→wDx→vDx
46 45 com23 ⊢D∈DirRel→wDx→vDw→vDx
47 46 imp ⊢D∈DirRel∧wDx→vDw→vDx
48 47 ad2ant2rl ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧wDx→vDw→vDx
49 42 48 anim12d ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧wDx→uDw∧vDw→uDx∧vDx
50 49 expr ⊢D∈DirRel∧u∈X∧v∈X∧w∈X→wDx→uDw∧vDw→uDx∧vDx
51 50 com23 ⊢D∈DirRel∧u∈X∧v∈X∧w∈X→uDw∧vDw→wDx→uDx∧vDx
52 51 impr ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧uDw∧vDw→wDx→uDx∧vDx
53 vex ⊢x∈V
54 1 eltail ⊢D∈DirRel∧w∈X∧x∈V→x∈tail⁡D⁡w↔wDx
55 53 54 mp3an3 ⊢D∈DirRel∧w∈X→x∈tail⁡D⁡w↔wDx
56 55 ad2ant2r ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧uDw∧vDw→x∈tail⁡D⁡w↔wDx
57 1 eltail ⊢D∈DirRel∧u∈X∧x∈V→x∈tail⁡D⁡u↔uDx
58 53 57 mp3an3 ⊢D∈DirRel∧u∈X→x∈tail⁡D⁡u↔uDx
59 58 adantrr ⊢D∈DirRel∧u∈X∧v∈X→x∈tail⁡D⁡u↔uDx
60 1 eltail ⊢D∈DirRel∧v∈X∧x∈V→x∈tail⁡D⁡v↔vDx
61 53 60 mp3an3 ⊢D∈DirRel∧v∈X→x∈tail⁡D⁡v↔vDx
62 61 adantrl ⊢D∈DirRel∧u∈X∧v∈X→x∈tail⁡D⁡v↔vDx
63 59 62 anbi12d ⊢D∈DirRel∧u∈X∧v∈X→x∈tail⁡D⁡u∧x∈tail⁡D⁡v↔uDx∧vDx
64 63 adantr ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧uDw∧vDw→x∈tail⁡D⁡u∧x∈tail⁡D⁡v↔uDx∧vDx
65 52 56 64 3imtr4d ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧uDw∧vDw→x∈tail⁡D⁡w→x∈tail⁡D⁡u∧x∈tail⁡D⁡v
66 elin ⊢x∈tail⁡D⁡u∩tail⁡D⁡v↔x∈tail⁡D⁡u∧x∈tail⁡D⁡v
67 65 66 syl6ibr ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧uDw∧vDw→x∈tail⁡D⁡w→x∈tail⁡D⁡u∩tail⁡D⁡v
68 67 ssrdv ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧uDw∧vDw→tail⁡D⁡w⊆tail⁡D⁡u∩tail⁡D⁡v
69 sseq1 ⊢z=tail⁡D⁡w→z⊆tail⁡D⁡u∩tail⁡D⁡v↔tail⁡D⁡w⊆tail⁡D⁡u∩tail⁡D⁡v
70 69 rspcev ⊢tail⁡D⁡w∈ran⁡tail⁡D∧tail⁡D⁡w⊆tail⁡D⁡u∩tail⁡D⁡v→∃z∈ran⁡tail⁡Dz⊆tail⁡D⁡u∩tail⁡D⁡v
71 36 68 70 syl2anc ⊢D∈DirRel∧u∈X∧v∈X∧w∈X∧uDw∧vDw→∃z∈ran⁡tail⁡Dz⊆tail⁡D⁡u∩tail⁡D⁡v
72 32 71 rexlimddv ⊢D∈DirRel∧u∈X∧v∈X→∃z∈ran⁡tail⁡Dz⊆tail⁡D⁡u∩tail⁡D⁡v
73 ineq1 ⊢tail⁡D⁡u=x→tail⁡D⁡u∩tail⁡D⁡v=x∩tail⁡D⁡v
74 73 sseq2d ⊢tail⁡D⁡u=x→z⊆tail⁡D⁡u∩tail⁡D⁡v↔z⊆x∩tail⁡D⁡v
75 74 rexbidv ⊢tail⁡D⁡u=x→∃z∈ran⁡tail⁡Dz⊆tail⁡D⁡u∩tail⁡D⁡v↔∃z∈ran⁡tail⁡Dz⊆x∩tail⁡D⁡v
76 ineq2 ⊢tail⁡D⁡v=y→x∩tail⁡D⁡v=x∩y
77 76 sseq2d ⊢tail⁡D⁡v=y→z⊆x∩tail⁡D⁡v↔z⊆x∩y
78 77 rexbidv ⊢tail⁡D⁡v=y→∃z∈ran⁡tail⁡Dz⊆x∩tail⁡D⁡v↔∃z∈ran⁡tail⁡Dz⊆x∩y
79 75 78 sylan9bb ⊢tail⁡D⁡u=x∧tail⁡D⁡v=y→∃z∈ran⁡tail⁡Dz⊆tail⁡D⁡u∩tail⁡D⁡v↔∃z∈ran⁡tail⁡Dz⊆x∩y
80 72 79 syl5ibcom ⊢D∈DirRel∧u∈X∧v∈X→tail⁡D⁡u=x∧tail⁡D⁡v=y→∃z∈ran⁡tail⁡Dz⊆x∩y
81 80 rexlimdvva ⊢D∈DirRel→∃u∈X∃v∈Xtail⁡D⁡u=x∧tail⁡D⁡v=y→∃z∈ran⁡tail⁡Dz⊆x∩y
82 30 81 biimtrrid ⊢D∈DirRel→∃u∈Xtail⁡D⁡u=x∧∃v∈Xtail⁡D⁡v=y→∃z∈ran⁡tail⁡Dz⊆x∩y
83 29 82 sylbid ⊢D∈DirRel→x∈ran⁡tail⁡D∧y∈ran⁡tail⁡D→∃z∈ran⁡tail⁡Dz⊆x∩y
84 83 adantr ⊢D∈DirRel∧X≠∅→x∈ran⁡tail⁡D∧y∈ran⁡tail⁡D→∃z∈ran⁡tail⁡Dz⊆x∩y
85 84 ralrimivv ⊢D∈DirRel∧X≠∅→∀x∈ran⁡tail⁡D∀y∈ran⁡tail⁡D∃z∈ran⁡tail⁡Dz⊆x∩y
86 14 25 85 3jca ⊢D∈DirRel∧X≠∅→ran⁡tail⁡D≠∅∧∅∉ran⁡tail⁡D∧∀x∈ran⁡tail⁡D∀y∈ran⁡tail⁡D∃z∈ran⁡tail⁡Dz⊆x∩y
87 dmexg ⊢D∈DirRel→dom⁡D∈V
88 1 87 eqeltrid ⊢D∈DirRel→X∈V
89 88 adantr ⊢D∈DirRel∧X≠∅→X∈V
90 isfbas2 ⊢X∈V→ran⁡tail⁡D∈fBas⁡X↔ran⁡tail⁡D⊆𝒫X∧ran⁡tail⁡D≠∅∧∅∉ran⁡tail⁡D∧∀x∈ran⁡tail⁡D∀y∈ran⁡tail⁡D∃z∈ran⁡tail⁡Dz⊆x∩y
91 89 90 syl ⊢D∈DirRel∧X≠∅→ran⁡tail⁡D∈fBas⁡X↔ran⁡tail⁡D⊆𝒫X∧ran⁡tail⁡D≠∅∧∅∉ran⁡tail⁡D∧∀x∈ran⁡tail⁡D∀y∈ran⁡tail⁡D∃z∈ran⁡tail⁡Dz⊆x∩y
92 4 86 91 mpbir2and ⊢D∈DirRel∧X≠∅→ran⁡tail⁡D∈fBas⁡X