Metamath Proof Explorer

Theorem filnetlem4

Description: Lemma for filnet . (Contributed by Jeff Hankins, 15-Dec-2009) (Revised by Mario Carneiro, 8-Aug-2015)

Ref Expression
Hypotheses filnet.h 
|- H = U_ n e. F ( { n } X. n )
filnet.d 
|- D = { <. x , y >. | ( ( x e. H /\ y e. H ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) }
Assertion filnetlem4 
|- ( F e. ( Fil ` X ) -> E. d e. DirRel E. f ( f : dom d --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` d ) ) ) )

Proof

Step Hyp Ref Expression
1 filnet.h 
 |-  H = U_ n e. F ( { n } X. n )
2 filnet.d 
 |-  D = { <. x , y >. | ( ( x e. H /\ y e. H ) /\ ( 1st ` y ) C_ ( 1st ` x ) ) }
3 1 2 filnetlem3 
 |-  ( H = U. U. D /\ ( F e. ( Fil ` X ) -> ( H C_ ( F X. X ) /\ D e. DirRel ) ) )
4 3 simpri 
 |-  ( F e. ( Fil ` X ) -> ( H C_ ( F X. X ) /\ D e. DirRel ) )
5 4 simprd 
 |-  ( F e. ( Fil ` X ) -> D e. DirRel )
6 f2ndres 
 |-  ( 2nd |` ( F X. X ) ) : ( F X. X ) --> X
7 4 simpld 
 |-  ( F e. ( Fil ` X ) -> H C_ ( F X. X ) )
8 fssres2 
 |-  ( ( ( 2nd |` ( F X. X ) ) : ( F X. X ) --> X /\ H C_ ( F X. X ) ) -> ( 2nd |` H ) : H --> X )
9 6 7 8 sylancr 
 |-  ( F e. ( Fil ` X ) -> ( 2nd |` H ) : H --> X )
10 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
11 xpexg 
 |-  ( ( F e. ( Fil ` X ) /\ X e. F ) -> ( F X. X ) e. _V )
12 10 11 mpdan 
 |-  ( F e. ( Fil ` X ) -> ( F X. X ) e. _V )
13 12 7 ssexd 
 |-  ( F e. ( Fil ` X ) -> H e. _V )
14 9 13 fexd 
 |-  ( F e. ( Fil ` X ) -> ( 2nd |` H ) e. _V )
15 3 simpli 
 |-  H = U. U. D
16 dirdm 
 |-  ( D e. DirRel -> dom D = U. U. D )
17 5 16 syl 
 |-  ( F e. ( Fil ` X ) -> dom D = U. U. D )
18 15 17 eqtr4id 
 |-  ( F e. ( Fil ` X ) -> H = dom D )
19 18 feq2d 
 |-  ( F e. ( Fil ` X ) -> ( ( 2nd |` H ) : H --> X <-> ( 2nd |` H ) : dom D --> X ) )
20 9 19 mpbid 
 |-  ( F e. ( Fil ` X ) -> ( 2nd |` H ) : dom D --> X )
21 eqid 
 |-  dom D = dom D
22 21 tailf 
 |-  ( D e. DirRel -> ( tail ` D ) : dom D --> ~P dom D )
23 5 22 syl 
 |-  ( F e. ( Fil ` X ) -> ( tail ` D ) : dom D --> ~P dom D )
24 18 feq2d 
 |-  ( F e. ( Fil ` X ) -> ( ( tail ` D ) : H --> ~P dom D <-> ( tail ` D ) : dom D --> ~P dom D ) )
25 23 24 mpbird 
 |-  ( F e. ( Fil ` X ) -> ( tail ` D ) : H --> ~P dom D )
26 25 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ t C_ X ) -> ( tail ` D ) : H --> ~P dom D )
27 ffn 
 |-  ( ( tail ` D ) : H --> ~P dom D -> ( tail ` D ) Fn H )
28 imaeq2 
 |-  ( d = ( ( tail ` D ) ` f ) -> ( ( 2nd |` H ) " d ) = ( ( 2nd |` H ) " ( ( tail ` D ) ` f ) ) )
29 28 sseq1d 
 |-  ( d = ( ( tail ` D ) ` f ) -> ( ( ( 2nd |` H ) " d ) C_ t <-> ( ( 2nd |` H ) " ( ( tail ` D ) ` f ) ) C_ t ) )
30 29 rexrn 
 |-  ( ( tail ` D ) Fn H -> ( E. d e. ran ( tail ` D ) ( ( 2nd |` H ) " d ) C_ t <-> E. f e. H ( ( 2nd |` H ) " ( ( tail ` D ) ` f ) ) C_ t ) )
31 26 27 30 3syl 
 |-  ( ( F e. ( Fil ` X ) /\ t C_ X ) -> ( E. d e. ran ( tail ` D ) ( ( 2nd |` H ) " d ) C_ t <-> E. f e. H ( ( 2nd |` H ) " ( ( tail ` D ) ` f ) ) C_ t ) )
32 fo2nd 
 |-  2nd : _V -onto-> _V
33 fofn 
 |-  ( 2nd : _V -onto-> _V -> 2nd Fn _V )
34 32 33 ax-mp 
 |-  2nd Fn _V
35 ssv 
 |-  H C_ _V
36 fnssres 
 |-  ( ( 2nd Fn _V /\ H C_ _V ) -> ( 2nd |` H ) Fn H )
37 34 35 36 mp2an 
 |-  ( 2nd |` H ) Fn H
38 fnfun 
 |-  ( ( 2nd |` H ) Fn H -> Fun ( 2nd |` H ) )
39 37 38 ax-mp 
 |-  Fun ( 2nd |` H )
40 26 ffvelrnda 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( ( tail ` D ) ` f ) e. ~P dom D )
41 40 elpwid 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( ( tail ` D ) ` f ) C_ dom D )
42 18 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> H = dom D )
43 41 42 sseqtrrd 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( ( tail ` D ) ` f ) C_ H )
44 37 fndmi 
 |-  dom ( 2nd |` H ) = H
45 43 44 sseqtrrdi 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( ( tail ` D ) ` f ) C_ dom ( 2nd |` H ) )
46 funimass4 
 |-  ( ( Fun ( 2nd |` H ) /\ ( ( tail ` D ) ` f ) C_ dom ( 2nd |` H ) ) -> ( ( ( 2nd |` H ) " ( ( tail ` D ) ` f ) ) C_ t <-> A. d e. ( ( tail ` D ) ` f ) ( ( 2nd |` H ) ` d ) e. t ) )
47 39 45 46 sylancr 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( ( ( 2nd |` H ) " ( ( tail ` D ) ` f ) ) C_ t <-> A. d e. ( ( tail ` D ) ` f ) ( ( 2nd |` H ) ` d ) e. t ) )
48 5 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> D e. DirRel )
49 simpr 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> f e. H )
50 49 42 eleqtrd 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> f e. dom D )
51 vex 
 |-  d e. _V
52 51 a1i 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> d e. _V )
53 21 eltail 
 |-  ( ( D e. DirRel /\ f e. dom D /\ d e. _V ) -> ( d e. ( ( tail ` D ) ` f ) <-> f D d ) )
54 48 50 52 53 syl3anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( d e. ( ( tail ` D ) ` f ) <-> f D d ) )
55 49 biantrurd 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( d e. H <-> ( f e. H /\ d e. H ) ) )
56 55 anbi1d 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( ( d e. H /\ ( 1st ` d ) C_ ( 1st ` f ) ) <-> ( ( f e. H /\ d e. H ) /\ ( 1st ` d ) C_ ( 1st ` f ) ) ) )
57 vex 
 |-  f e. _V
58 1 2 57 51 filnetlem1 
 |-  ( f D d <-> ( ( f e. H /\ d e. H ) /\ ( 1st ` d ) C_ ( 1st ` f ) ) )
59 56 58 bitr4di 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( ( d e. H /\ ( 1st ` d ) C_ ( 1st ` f ) ) <-> f D d ) )
60 54 59 bitr4d 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( d e. ( ( tail ` D ) ` f ) <-> ( d e. H /\ ( 1st ` d ) C_ ( 1st ` f ) ) ) )
61 60 imbi1d 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( ( d e. ( ( tail ` D ) ` f ) -> ( ( 2nd |` H ) ` d ) e. t ) <-> ( ( d e. H /\ ( 1st ` d ) C_ ( 1st ` f ) ) -> ( ( 2nd |` H ) ` d ) e. t ) ) )
62 fvres 
 |-  ( d e. H -> ( ( 2nd |` H ) ` d ) = ( 2nd ` d ) )
63 62 eleq1d 
 |-  ( d e. H -> ( ( ( 2nd |` H ) ` d ) e. t <-> ( 2nd ` d ) e. t ) )
64 63 adantr 
 |-  ( ( d e. H /\ ( 1st ` d ) C_ ( 1st ` f ) ) -> ( ( ( 2nd |` H ) ` d ) e. t <-> ( 2nd ` d ) e. t ) )
65 64 pm5.74i 
 |-  ( ( ( d e. H /\ ( 1st ` d ) C_ ( 1st ` f ) ) -> ( ( 2nd |` H ) ` d ) e. t ) <-> ( ( d e. H /\ ( 1st ` d ) C_ ( 1st ` f ) ) -> ( 2nd ` d ) e. t ) )
66 impexp 
 |-  ( ( ( d e. H /\ ( 1st ` d ) C_ ( 1st ` f ) ) -> ( 2nd ` d ) e. t ) <-> ( d e. H -> ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) ) )
67 65 66 bitri 
 |-  ( ( ( d e. H /\ ( 1st ` d ) C_ ( 1st ` f ) ) -> ( ( 2nd |` H ) ` d ) e. t ) <-> ( d e. H -> ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) ) )
68 61 67 bitrdi 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( ( d e. ( ( tail ` D ) ` f ) -> ( ( 2nd |` H ) ` d ) e. t ) <-> ( d e. H -> ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) ) ) )
69 68 ralbidv2 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( A. d e. ( ( tail ` D ) ` f ) ( ( 2nd |` H ) ` d ) e. t <-> A. d e. H ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) ) )
70 47 69 bitrd 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ f e. H ) -> ( ( ( 2nd |` H ) " ( ( tail ` D ) ` f ) ) C_ t <-> A. d e. H ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) ) )
71 70 rexbidva 
 |-  ( ( F e. ( Fil ` X ) /\ t C_ X ) -> ( E. f e. H ( ( 2nd |` H ) " ( ( tail ` D ) ` f ) ) C_ t <-> E. f e. H A. d e. H ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) ) )
72 vex 
 |-  k e. _V
73 vex 
 |-  v e. _V
74 72 73 op1std 
 |-  ( d = <. k , v >. -> ( 1st ` d ) = k )
75 74 sseq1d 
 |-  ( d = <. k , v >. -> ( ( 1st ` d ) C_ ( 1st ` f ) <-> k C_ ( 1st ` f ) ) )
76 72 73 op2ndd 
 |-  ( d = <. k , v >. -> ( 2nd ` d ) = v )
77 76 eleq1d 
 |-  ( d = <. k , v >. -> ( ( 2nd ` d ) e. t <-> v e. t ) )
78 75 77 imbi12d 
 |-  ( d = <. k , v >. -> ( ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) <-> ( k C_ ( 1st ` f ) -> v e. t ) ) )
79 78 raliunxp 
 |-  ( A. d e. U_ k e. F ( { k } X. k ) ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) <-> A. k e. F A. v e. k ( k C_ ( 1st ` f ) -> v e. t ) )
80 sneq 
 |-  ( n = k -> { n } = { k } )
81 id 
 |-  ( n = k -> n = k )
82 80 81 xpeq12d 
 |-  ( n = k -> ( { n } X. n ) = ( { k } X. k ) )
83 82 cbviunv 
 |-  U_ n e. F ( { n } X. n ) = U_ k e. F ( { k } X. k )
84 1 83 eqtri 
 |-  H = U_ k e. F ( { k } X. k )
85 84 raleqi 
 |-  ( A. d e. H ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) <-> A. d e. U_ k e. F ( { k } X. k ) ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) )
86 dfss3 
 |-  ( k C_ t <-> A. v e. k v e. t )
87 86 imbi2i 
 |-  ( ( k C_ ( 1st ` f ) -> k C_ t ) <-> ( k C_ ( 1st ` f ) -> A. v e. k v e. t ) )
88 r19.21v 
 |-  ( A. v e. k ( k C_ ( 1st ` f ) -> v e. t ) <-> ( k C_ ( 1st ` f ) -> A. v e. k v e. t ) )
89 87 88 bitr4i 
 |-  ( ( k C_ ( 1st ` f ) -> k C_ t ) <-> A. v e. k ( k C_ ( 1st ` f ) -> v e. t ) )
90 89 ralbii 
 |-  ( A. k e. F ( k C_ ( 1st ` f ) -> k C_ t ) <-> A. k e. F A. v e. k ( k C_ ( 1st ` f ) -> v e. t ) )
91 79 85 90 3bitr4i 
 |-  ( A. d e. H ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) <-> A. k e. F ( k C_ ( 1st ` f ) -> k C_ t ) )
92 91 rexbii 
 |-  ( E. f e. H A. d e. H ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) <-> E. f e. H A. k e. F ( k C_ ( 1st ` f ) -> k C_ t ) )
93 1 rexeqi 
 |-  ( E. f e. H A. k e. F ( k C_ ( 1st ` f ) -> k C_ t ) <-> E. f e. U_ n e. F ( { n } X. n ) A. k e. F ( k C_ ( 1st ` f ) -> k C_ t ) )
94 vex 
 |-  n e. _V
95 vex 
 |-  m e. _V
96 94 95 op1std 
 |-  ( f = <. n , m >. -> ( 1st ` f ) = n )
97 96 sseq2d 
 |-  ( f = <. n , m >. -> ( k C_ ( 1st ` f ) <-> k C_ n ) )
98 97 imbi1d 
 |-  ( f = <. n , m >. -> ( ( k C_ ( 1st ` f ) -> k C_ t ) <-> ( k C_ n -> k C_ t ) ) )
99 98 ralbidv 
 |-  ( f = <. n , m >. -> ( A. k e. F ( k C_ ( 1st ` f ) -> k C_ t ) <-> A. k e. F ( k C_ n -> k C_ t ) ) )
100 99 rexiunxp 
 |-  ( E. f e. U_ n e. F ( { n } X. n ) A. k e. F ( k C_ ( 1st ` f ) -> k C_ t ) <-> E. n e. F E. m e. n A. k e. F ( k C_ n -> k C_ t ) )
101 92 93 100 3bitri 
 |-  ( E. f e. H A. d e. H ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) <-> E. n e. F E. m e. n A. k e. F ( k C_ n -> k C_ t ) )
102 fileln0 
 |-  ( ( F e. ( Fil ` X ) /\ n e. F ) -> n =/= (/) )
103 102 adantlr 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ n e. F ) -> n =/= (/) )
104 r19.9rzv 
 |-  ( n =/= (/) -> ( A. k e. F ( k C_ n -> k C_ t ) <-> E. m e. n A. k e. F ( k C_ n -> k C_ t ) ) )
105 103 104 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ n e. F ) -> ( A. k e. F ( k C_ n -> k C_ t ) <-> E. m e. n A. k e. F ( k C_ n -> k C_ t ) ) )
106 ssid 
 |-  n C_ n
107 sseq1 
 |-  ( k = n -> ( k C_ n <-> n C_ n ) )
108 sseq1 
 |-  ( k = n -> ( k C_ t <-> n C_ t ) )
109 107 108 imbi12d 
 |-  ( k = n -> ( ( k C_ n -> k C_ t ) <-> ( n C_ n -> n C_ t ) ) )
110 109 rspcv 
 |-  ( n e. F -> ( A. k e. F ( k C_ n -> k C_ t ) -> ( n C_ n -> n C_ t ) ) )
111 106 110 mpii 
 |-  ( n e. F -> ( A. k e. F ( k C_ n -> k C_ t ) -> n C_ t ) )
112 111 adantl 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ n e. F ) -> ( A. k e. F ( k C_ n -> k C_ t ) -> n C_ t ) )
113 sstr2 
 |-  ( k C_ n -> ( n C_ t -> k C_ t ) )
114 113 com12 
 |-  ( n C_ t -> ( k C_ n -> k C_ t ) )
115 114 ralrimivw 
 |-  ( n C_ t -> A. k e. F ( k C_ n -> k C_ t ) )
116 112 115 impbid1 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ n e. F ) -> ( A. k e. F ( k C_ n -> k C_ t ) <-> n C_ t ) )
117 105 116 bitr3d 
 |-  ( ( ( F e. ( Fil ` X ) /\ t C_ X ) /\ n e. F ) -> ( E. m e. n A. k e. F ( k C_ n -> k C_ t ) <-> n C_ t ) )
118 117 rexbidva 
 |-  ( ( F e. ( Fil ` X ) /\ t C_ X ) -> ( E. n e. F E. m e. n A. k e. F ( k C_ n -> k C_ t ) <-> E. n e. F n C_ t ) )
119 101 118 syl5bb 
 |-  ( ( F e. ( Fil ` X ) /\ t C_ X ) -> ( E. f e. H A. d e. H ( ( 1st ` d ) C_ ( 1st ` f ) -> ( 2nd ` d ) e. t ) <-> E. n e. F n C_ t ) )
120 31 71 119 3bitrd 
 |-  ( ( F e. ( Fil ` X ) /\ t C_ X ) -> ( E. d e. ran ( tail ` D ) ( ( 2nd |` H ) " d ) C_ t <-> E. n e. F n C_ t ) )
121 120 pm5.32da 
 |-  ( F e. ( Fil ` X ) -> ( ( t C_ X /\ E. d e. ran ( tail ` D ) ( ( 2nd |` H ) " d ) C_ t ) <-> ( t C_ X /\ E. n e. F n C_ t ) ) )
122 filn0 
 |-  ( F e. ( Fil ` X ) -> F =/= (/) )
123 94 snnz 
 |-  { n } =/= (/)
124 102 123 jctil 
 |-  ( ( F e. ( Fil ` X ) /\ n e. F ) -> ( { n } =/= (/) /\ n =/= (/) ) )
125 neanior 
 |-  ( ( { n } =/= (/) /\ n =/= (/) ) <-> -. ( { n } = (/) \/ n = (/) ) )
126 124 125 sylib 
 |-  ( ( F e. ( Fil ` X ) /\ n e. F ) -> -. ( { n } = (/) \/ n = (/) ) )
127 ss0b 
 |-  ( ( { n } X. n ) C_ (/) <-> ( { n } X. n ) = (/) )
128 xpeq0 
 |-  ( ( { n } X. n ) = (/) <-> ( { n } = (/) \/ n = (/) ) )
129 127 128 bitri 
 |-  ( ( { n } X. n ) C_ (/) <-> ( { n } = (/) \/ n = (/) ) )
130 126 129 sylnibr 
 |-  ( ( F e. ( Fil ` X ) /\ n e. F ) -> -. ( { n } X. n ) C_ (/) )
131 130 ralrimiva 
 |-  ( F e. ( Fil ` X ) -> A. n e. F -. ( { n } X. n ) C_ (/) )
132 r19.2z 
 |-  ( ( F =/= (/) /\ A. n e. F -. ( { n } X. n ) C_ (/) ) -> E. n e. F -. ( { n } X. n ) C_ (/) )
133 122 131 132 syl2anc 
 |-  ( F e. ( Fil ` X ) -> E. n e. F -. ( { n } X. n ) C_ (/) )
134 rexnal 
 |-  ( E. n e. F -. ( { n } X. n ) C_ (/) <-> -. A. n e. F ( { n } X. n ) C_ (/) )
135 133 134 sylib 
 |-  ( F e. ( Fil ` X ) -> -. A. n e. F ( { n } X. n ) C_ (/) )
136 1 sseq1i 
 |-  ( H C_ (/) <-> U_ n e. F ( { n } X. n ) C_ (/) )
137 ss0b 
 |-  ( H C_ (/) <-> H = (/) )
138 iunss 
 |-  ( U_ n e. F ( { n } X. n ) C_ (/) <-> A. n e. F ( { n } X. n ) C_ (/) )
139 136 137 138 3bitr3i 
 |-  ( H = (/) <-> A. n e. F ( { n } X. n ) C_ (/) )
140 139 necon3abii 
 |-  ( H =/= (/) <-> -. A. n e. F ( { n } X. n ) C_ (/) )
141 135 140 sylibr 
 |-  ( F e. ( Fil ` X ) -> H =/= (/) )
142 dmresi 
 |-  dom ( _I |` H ) = H
143 1 2 filnetlem2 
 |-  ( ( _I |` H ) C_ D /\ D C_ ( H X. H ) )
144 143 simpli 
 |-  ( _I |` H ) C_ D
145 dmss 
 |-  ( ( _I |` H ) C_ D -> dom ( _I |` H ) C_ dom D )
146 144 145 ax-mp 
 |-  dom ( _I |` H ) C_ dom D
147 142 146 eqsstrri 
 |-  H C_ dom D
148 143 simpri 
 |-  D C_ ( H X. H )
149 dmss 
 |-  ( D C_ ( H X. H ) -> dom D C_ dom ( H X. H ) )
150 148 149 ax-mp 
 |-  dom D C_ dom ( H X. H )
151 dmxpid 
 |-  dom ( H X. H ) = H
152 150 151 sseqtri 
 |-  dom D C_ H
153 147 152 eqssi 
 |-  H = dom D
154 153 tailfb 
 |-  ( ( D e. DirRel /\ H =/= (/) ) -> ran ( tail ` D ) e. ( fBas ` H ) )
155 5 141 154 syl2anc 
 |-  ( F e. ( Fil ` X ) -> ran ( tail ` D ) e. ( fBas ` H ) )
156 elfm 
 |-  ( ( X e. F /\ ran ( tail ` D ) e. ( fBas ` H ) /\ ( 2nd |` H ) : H --> X ) -> ( t e. ( ( X FilMap ( 2nd |` H ) ) ` ran ( tail ` D ) ) <-> ( t C_ X /\ E. d e. ran ( tail ` D ) ( ( 2nd |` H ) " d ) C_ t ) ) )
157 10 155 9 156 syl3anc 
 |-  ( F e. ( Fil ` X ) -> ( t e. ( ( X FilMap ( 2nd |` H ) ) ` ran ( tail ` D ) ) <-> ( t C_ X /\ E. d e. ran ( tail ` D ) ( ( 2nd |` H ) " d ) C_ t ) ) )
158 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
159 elfg 
 |-  ( F e. ( fBas ` X ) -> ( t e. ( X filGen F ) <-> ( t C_ X /\ E. n e. F n C_ t ) ) )
160 158 159 syl 
 |-  ( F e. ( Fil ` X ) -> ( t e. ( X filGen F ) <-> ( t C_ X /\ E. n e. F n C_ t ) ) )
161 121 157 160 3bitr4d 
 |-  ( F e. ( Fil ` X ) -> ( t e. ( ( X FilMap ( 2nd |` H ) ) ` ran ( tail ` D ) ) <-> t e. ( X filGen F ) ) )
162 161 eqrdv 
 |-  ( F e. ( Fil ` X ) -> ( ( X FilMap ( 2nd |` H ) ) ` ran ( tail ` D ) ) = ( X filGen F ) )
163 fgfil 
 |-  ( F e. ( Fil ` X ) -> ( X filGen F ) = F )
164 162 163 eqtr2d 
 |-  ( F e. ( Fil ` X ) -> F = ( ( X FilMap ( 2nd |` H ) ) ` ran ( tail ` D ) ) )
165 20 164 jca 
 |-  ( F e. ( Fil ` X ) -> ( ( 2nd |` H ) : dom D --> X /\ F = ( ( X FilMap ( 2nd |` H ) ) ` ran ( tail ` D ) ) ) )
166 feq1 
 |-  ( f = ( 2nd |` H ) -> ( f : dom D --> X <-> ( 2nd |` H ) : dom D --> X ) )
167 oveq2 
 |-  ( f = ( 2nd |` H ) -> ( X FilMap f ) = ( X FilMap ( 2nd |` H ) ) )
168 167 fveq1d 
 |-  ( f = ( 2nd |` H ) -> ( ( X FilMap f ) ` ran ( tail ` D ) ) = ( ( X FilMap ( 2nd |` H ) ) ` ran ( tail ` D ) ) )
169 168 eqeq2d 
 |-  ( f = ( 2nd |` H ) -> ( F = ( ( X FilMap f ) ` ran ( tail ` D ) ) <-> F = ( ( X FilMap ( 2nd |` H ) ) ` ran ( tail ` D ) ) ) )
170 166 169 anbi12d 
 |-  ( f = ( 2nd |` H ) -> ( ( f : dom D --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` D ) ) ) <-> ( ( 2nd |` H ) : dom D --> X /\ F = ( ( X FilMap ( 2nd |` H ) ) ` ran ( tail ` D ) ) ) ) )
171 170 spcegv 
 |-  ( ( 2nd |` H ) e. _V -> ( ( ( 2nd |` H ) : dom D --> X /\ F = ( ( X FilMap ( 2nd |` H ) ) ` ran ( tail ` D ) ) ) -> E. f ( f : dom D --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` D ) ) ) ) )
172 14 165 171 sylc 
 |-  ( F e. ( Fil ` X ) -> E. f ( f : dom D --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` D ) ) ) )
173 dmeq 
 |-  ( d = D -> dom d = dom D )
174 173 feq2d 
 |-  ( d = D -> ( f : dom d --> X <-> f : dom D --> X ) )
175 fveq2 
 |-  ( d = D -> ( tail ` d ) = ( tail ` D ) )
176 175 rneqd 
 |-  ( d = D -> ran ( tail ` d ) = ran ( tail ` D ) )
177 176 fveq2d 
 |-  ( d = D -> ( ( X FilMap f ) ` ran ( tail ` d ) ) = ( ( X FilMap f ) ` ran ( tail ` D ) ) )
178 177 eqeq2d 
 |-  ( d = D -> ( F = ( ( X FilMap f ) ` ran ( tail ` d ) ) <-> F = ( ( X FilMap f ) ` ran ( tail ` D ) ) ) )
179 174 178 anbi12d 
 |-  ( d = D -> ( ( f : dom d --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` d ) ) ) <-> ( f : dom D --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` D ) ) ) ) )
180 179 exbidv 
 |-  ( d = D -> ( E. f ( f : dom d --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` d ) ) ) <-> E. f ( f : dom D --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` D ) ) ) ) )
181 180 rspcev 
 |-  ( ( D e. DirRel /\ E. f ( f : dom D --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` D ) ) ) ) -> E. d e. DirRel E. f ( f : dom d --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` d ) ) ) )
182 5 172 181 syl2anc 
 |-  ( F e. ( Fil ` X ) -> E. d e. DirRel E. f ( f : dom d --> X /\ F = ( ( X FilMap f ) ` ran ( tail ` d ) ) ) )