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 e. DirRel /\ X =/= (/) ) -> ran ( tail ` D ) e. ( fBas ` X ) )

Proof

Step Hyp Ref Expression
1 tailfb.1 
 |-  X = dom D
2 1 tailf 
 |-  ( D e. DirRel -> ( tail ` D ) : X --> ~P X )
3 2 frnd 
 |-  ( D e. DirRel -> ran ( tail ` D ) C_ ~P X )
4 3 adantr 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> ran ( tail ` D ) C_ ~P X )
5 n0 
 |-  ( X =/= (/) <-> E. x x e. X )
6 ffn 
 |-  ( ( tail ` D ) : X --> ~P X -> ( tail ` D ) Fn X )
7 fnfvelrn 
 |-  ( ( ( tail ` D ) Fn X /\ x e. X ) -> ( ( tail ` D ) ` x ) e. ran ( tail ` D ) )
8 7 ex 
 |-  ( ( tail ` D ) Fn X -> ( x e. X -> ( ( tail ` D ) ` x ) e. ran ( tail ` D ) ) )
9 2 6 8 3syl 
 |-  ( D e. DirRel -> ( x e. X -> ( ( tail ` D ) ` x ) e. ran ( tail ` D ) ) )
10 ne0i 
 |-  ( ( ( tail ` D ) ` x ) e. ran ( tail ` D ) -> ran ( tail ` D ) =/= (/) )
11 9 10 syl6 
 |-  ( D e. DirRel -> ( x e. X -> ran ( tail ` D ) =/= (/) ) )
12 11 exlimdv 
 |-  ( D e. DirRel -> ( E. x x e. X -> ran ( tail ` D ) =/= (/) ) )
13 5 12 syl5bi 
 |-  ( D e. DirRel -> ( X =/= (/) -> ran ( tail ` D ) =/= (/) ) )
14 13 imp 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> ran ( tail ` D ) =/= (/) )
15 1 tailini 
 |-  ( ( D e. DirRel /\ x e. X ) -> x e. ( ( tail ` D ) ` x ) )
16 n0i 
 |-  ( x e. ( ( tail ` D ) ` x ) -> -. ( ( tail ` D ) ` x ) = (/) )
17 15 16 syl 
 |-  ( ( D e. DirRel /\ x e. X ) -> -. ( ( tail ` D ) ` x ) = (/) )
18 17 nrexdv 
 |-  ( D e. DirRel -> -. E. x e. X ( ( tail ` D ) ` x ) = (/) )
19 18 adantr 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> -. E. x e. X ( ( tail ` D ) ` x ) = (/) )
20 fvelrnb 
 |-  ( ( tail ` D ) Fn X -> ( (/) e. ran ( tail ` D ) <-> E. x e. X ( ( tail ` D ) ` x ) = (/) ) )
21 2 6 20 3syl 
 |-  ( D e. DirRel -> ( (/) e. ran ( tail ` D ) <-> E. x e. X ( ( tail ` D ) ` x ) = (/) ) )
22 21 adantr 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> ( (/) e. ran ( tail ` D ) <-> E. x e. X ( ( tail ` D ) ` x ) = (/) ) )
23 19 22 mtbird 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> -. (/) e. ran ( tail ` D ) )
24 df-nel 
 |-  ( (/) e/ ran ( tail ` D ) <-> -. (/) e. ran ( tail ` D ) )
25 23 24 sylibr 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> (/) e/ ran ( tail ` D ) )
26 fvelrnb 
 |-  ( ( tail ` D ) Fn X -> ( x e. ran ( tail ` D ) <-> E. u e. X ( ( tail ` D ) ` u ) = x ) )
27 fvelrnb 
 |-  ( ( tail ` D ) Fn X -> ( y e. ran ( tail ` D ) <-> E. v e. X ( ( tail ` D ) ` v ) = y ) )
28 26 27 anbi12d 
 |-  ( ( tail ` D ) Fn X -> ( ( x e. ran ( tail ` D ) /\ y e. ran ( tail ` D ) ) <-> ( E. u e. X ( ( tail ` D ) ` u ) = x /\ E. v e. X ( ( tail ` D ) ` v ) = y ) ) )
29 2 6 28 3syl 
 |-  ( D e. DirRel -> ( ( x e. ran ( tail ` D ) /\ y e. ran ( tail ` D ) ) <-> ( E. u e. X ( ( tail ` D ) ` u ) = x /\ E. v e. X ( ( tail ` D ) ` v ) = y ) ) )
30 reeanv 
 |-  ( E. u e. X E. v e. X ( ( ( tail ` D ) ` u ) = x /\ ( ( tail ` D ) ` v ) = y ) <-> ( E. u e. X ( ( tail ` D ) ` u ) = x /\ E. v e. X ( ( tail ` D ) ` v ) = y ) )
31 1 dirge 
 |-  ( ( D e. DirRel /\ u e. X /\ v e. X ) -> E. w e. X ( u D w /\ v D w ) )
32 31 3expb 
 |-  ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) -> E. w e. X ( u D w /\ v D w ) )
33 2 6 syl 
 |-  ( D e. DirRel -> ( tail ` D ) Fn X )
34 fnfvelrn 
 |-  ( ( ( tail ` D ) Fn X /\ w e. X ) -> ( ( tail ` D ) ` w ) e. ran ( tail ` D ) )
35 33 34 sylan 
 |-  ( ( D e. DirRel /\ w e. X ) -> ( ( tail ` D ) ` w ) e. ran ( tail ` D ) )
36 35 ad2ant2r 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ ( u D w /\ v D w ) ) ) -> ( ( tail ` D ) ` w ) e. ran ( tail ` D ) )
37 dirtr 
 |-  ( ( ( D e. DirRel /\ x e. _V ) /\ ( u D w /\ w D x ) ) -> u D x )
38 37 exp32 
 |-  ( ( D e. DirRel /\ x e. _V ) -> ( u D w -> ( w D x -> u D x ) ) )
39 38 elvd 
 |-  ( D e. DirRel -> ( u D w -> ( w D x -> u D x ) ) )
40 39 com23 
 |-  ( D e. DirRel -> ( w D x -> ( u D w -> u D x ) ) )
41 40 imp 
 |-  ( ( D e. DirRel /\ w D x ) -> ( u D w -> u D x ) )
42 41 ad2ant2rl 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ w D x ) ) -> ( u D w -> u D x ) )
43 dirtr 
 |-  ( ( ( D e. DirRel /\ x e. _V ) /\ ( v D w /\ w D x ) ) -> v D x )
44 43 exp32 
 |-  ( ( D e. DirRel /\ x e. _V ) -> ( v D w -> ( w D x -> v D x ) ) )
45 44 elvd 
 |-  ( D e. DirRel -> ( v D w -> ( w D x -> v D x ) ) )
46 45 com23 
 |-  ( D e. DirRel -> ( w D x -> ( v D w -> v D x ) ) )
47 46 imp 
 |-  ( ( D e. DirRel /\ w D x ) -> ( v D w -> v D x ) )
48 47 ad2ant2rl 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ w D x ) ) -> ( v D w -> v D x ) )
49 42 48 anim12d 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ w D x ) ) -> ( ( u D w /\ v D w ) -> ( u D x /\ v D x ) ) )
50 49 expr 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ w e. X ) -> ( w D x -> ( ( u D w /\ v D w ) -> ( u D x /\ v D x ) ) ) )
51 50 com23 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ w e. X ) -> ( ( u D w /\ v D w ) -> ( w D x -> ( u D x /\ v D x ) ) ) )
52 51 impr 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ ( u D w /\ v D w ) ) ) -> ( w D x -> ( u D x /\ v D x ) ) )
53 vex 
 |-  x e. _V
54 1 eltail 
 |-  ( ( D e. DirRel /\ w e. X /\ x e. _V ) -> ( x e. ( ( tail ` D ) ` w ) <-> w D x ) )
55 53 54 mp3an3 
 |-  ( ( D e. DirRel /\ w e. X ) -> ( x e. ( ( tail ` D ) ` w ) <-> w D x ) )
56 55 ad2ant2r 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ ( u D w /\ v D w ) ) ) -> ( x e. ( ( tail ` D ) ` w ) <-> w D x ) )
57 1 eltail 
 |-  ( ( D e. DirRel /\ u e. X /\ x e. _V ) -> ( x e. ( ( tail ` D ) ` u ) <-> u D x ) )
58 53 57 mp3an3 
 |-  ( ( D e. DirRel /\ u e. X ) -> ( x e. ( ( tail ` D ) ` u ) <-> u D x ) )
59 58 adantrr 
 |-  ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) -> ( x e. ( ( tail ` D ) ` u ) <-> u D x ) )
60 1 eltail 
 |-  ( ( D e. DirRel /\ v e. X /\ x e. _V ) -> ( x e. ( ( tail ` D ) ` v ) <-> v D x ) )
61 53 60 mp3an3 
 |-  ( ( D e. DirRel /\ v e. X ) -> ( x e. ( ( tail ` D ) ` v ) <-> v D x ) )
62 61 adantrl 
 |-  ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) -> ( x e. ( ( tail ` D ) ` v ) <-> v D x ) )
63 59 62 anbi12d 
 |-  ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) -> ( ( x e. ( ( tail ` D ) ` u ) /\ x e. ( ( tail ` D ) ` v ) ) <-> ( u D x /\ v D x ) ) )
64 63 adantr 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ ( u D w /\ v D w ) ) ) -> ( ( x e. ( ( tail ` D ) ` u ) /\ x e. ( ( tail ` D ) ` v ) ) <-> ( u D x /\ v D x ) ) )
65 52 56 64 3imtr4d 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ ( u D w /\ v D w ) ) ) -> ( x e. ( ( tail ` D ) ` w ) -> ( x e. ( ( tail ` D ) ` u ) /\ x e. ( ( tail ` D ) ` v ) ) ) )
66 elin 
 |-  ( x e. ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) <-> ( x e. ( ( tail ` D ) ` u ) /\ x e. ( ( tail ` D ) ` v ) ) )
67 65 66 syl6ibr 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ ( u D w /\ v D w ) ) ) -> ( x e. ( ( tail ` D ) ` w ) -> x e. ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) ) )
68 67 ssrdv 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ ( u D w /\ v D w ) ) ) -> ( ( tail ` D ) ` w ) C_ ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) )
69 sseq1 
 |-  ( z = ( ( tail ` D ) ` w ) -> ( z C_ ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) <-> ( ( tail ` D ) ` w ) C_ ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) ) )
70 69 rspcev 
 |-  ( ( ( ( tail ` D ) ` w ) e. ran ( tail ` D ) /\ ( ( tail ` D ) ` w ) C_ ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) ) -> E. z e. ran ( tail ` D ) z C_ ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) )
71 36 68 70 syl2anc 
 |-  ( ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) /\ ( w e. X /\ ( u D w /\ v D w ) ) ) -> E. z e. ran ( tail ` D ) z C_ ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) )
72 32 71 rexlimddv 
 |-  ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) -> E. z e. ran ( tail ` D ) z C_ ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) )
73 ineq1 
 |-  ( ( ( tail ` D ) ` u ) = x -> ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) = ( x i^i ( ( tail ` D ) ` v ) ) )
74 73 sseq2d 
 |-  ( ( ( tail ` D ) ` u ) = x -> ( z C_ ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) <-> z C_ ( x i^i ( ( tail ` D ) ` v ) ) ) )
75 74 rexbidv 
 |-  ( ( ( tail ` D ) ` u ) = x -> ( E. z e. ran ( tail ` D ) z C_ ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) <-> E. z e. ran ( tail ` D ) z C_ ( x i^i ( ( tail ` D ) ` v ) ) ) )
76 ineq2 
 |-  ( ( ( tail ` D ) ` v ) = y -> ( x i^i ( ( tail ` D ) ` v ) ) = ( x i^i y ) )
77 76 sseq2d 
 |-  ( ( ( tail ` D ) ` v ) = y -> ( z C_ ( x i^i ( ( tail ` D ) ` v ) ) <-> z C_ ( x i^i y ) ) )
78 77 rexbidv 
 |-  ( ( ( tail ` D ) ` v ) = y -> ( E. z e. ran ( tail ` D ) z C_ ( x i^i ( ( tail ` D ) ` v ) ) <-> E. z e. ran ( tail ` D ) z C_ ( x i^i y ) ) )
79 75 78 sylan9bb 
 |-  ( ( ( ( tail ` D ) ` u ) = x /\ ( ( tail ` D ) ` v ) = y ) -> ( E. z e. ran ( tail ` D ) z C_ ( ( ( tail ` D ) ` u ) i^i ( ( tail ` D ) ` v ) ) <-> E. z e. ran ( tail ` D ) z C_ ( x i^i y ) ) )
80 72 79 syl5ibcom 
 |-  ( ( D e. DirRel /\ ( u e. X /\ v e. X ) ) -> ( ( ( ( tail ` D ) ` u ) = x /\ ( ( tail ` D ) ` v ) = y ) -> E. z e. ran ( tail ` D ) z C_ ( x i^i y ) ) )
81 80 rexlimdvva 
 |-  ( D e. DirRel -> ( E. u e. X E. v e. X ( ( ( tail ` D ) ` u ) = x /\ ( ( tail ` D ) ` v ) = y ) -> E. z e. ran ( tail ` D ) z C_ ( x i^i y ) ) )
82 30 81 syl5bir 
 |-  ( D e. DirRel -> ( ( E. u e. X ( ( tail ` D ) ` u ) = x /\ E. v e. X ( ( tail ` D ) ` v ) = y ) -> E. z e. ran ( tail ` D ) z C_ ( x i^i y ) ) )
83 29 82 sylbid 
 |-  ( D e. DirRel -> ( ( x e. ran ( tail ` D ) /\ y e. ran ( tail ` D ) ) -> E. z e. ran ( tail ` D ) z C_ ( x i^i y ) ) )
84 83 adantr 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> ( ( x e. ran ( tail ` D ) /\ y e. ran ( tail ` D ) ) -> E. z e. ran ( tail ` D ) z C_ ( x i^i y ) ) )
85 84 ralrimivv 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> A. x e. ran ( tail ` D ) A. y e. ran ( tail ` D ) E. z e. ran ( tail ` D ) z C_ ( x i^i y ) )
86 14 25 85 3jca 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> ( ran ( tail ` D ) =/= (/) /\ (/) e/ ran ( tail ` D ) /\ A. x e. ran ( tail ` D ) A. y e. ran ( tail ` D ) E. z e. ran ( tail ` D ) z C_ ( x i^i y ) ) )
87 dmexg 
 |-  ( D e. DirRel -> dom D e. _V )
88 1 87 eqeltrid 
 |-  ( D e. DirRel -> X e. _V )
89 88 adantr 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> X e. _V )
90 isfbas2 
 |-  ( X e. _V -> ( ran ( tail ` D ) e. ( fBas ` X ) <-> ( ran ( tail ` D ) C_ ~P X /\ ( ran ( tail ` D ) =/= (/) /\ (/) e/ ran ( tail ` D ) /\ A. x e. ran ( tail ` D ) A. y e. ran ( tail ` D ) E. z e. ran ( tail ` D ) z C_ ( x i^i y ) ) ) ) )
91 89 90 syl 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> ( ran ( tail ` D ) e. ( fBas ` X ) <-> ( ran ( tail ` D ) C_ ~P X /\ ( ran ( tail ` D ) =/= (/) /\ (/) e/ ran ( tail ` D ) /\ A. x e. ran ( tail ` D ) A. y e. ran ( tail ` D ) E. z e. ran ( tail ` D ) z C_ ( x i^i y ) ) ) ) )
92 4 86 91 mpbir2and 
 |-  ( ( D e. DirRel /\ X =/= (/) ) -> ran ( tail ` D ) e. ( fBas ` X ) )