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=⋃n∈Fn×n
filnet.d ⊢D=xy|x∈H∧y∈H∧1st⁡y⊆1st⁡x
Assertion filnetlem4 ⊢F∈Fil⁡X→∃d∈DirRel∃ff:dom⁡d⟶X∧F=XFilMapf⁡ran⁡tail⁡d

Proof

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