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