Metamath Proof Explorer

Theorem filnetlem3

Description: Lemma for filnet . (Contributed by Jeff Hankins, 13-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 filnetlem3 
|- ( H = U. U. D /\ ( F e. ( Fil ` X ) -> ( H C_ ( F X. X ) /\ D e. DirRel ) ) )

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 dmresi 
 |-  dom ( _I |` H ) = H
4 1 2 filnetlem2 
 |-  ( ( _I |` H ) C_ D /\ D C_ ( H X. H ) )
5 4 simpli 
 |-  ( _I |` H ) C_ D
6 dmss 
 |-  ( ( _I |` H ) C_ D -> dom ( _I |` H ) C_ dom D )
7 5 6 ax-mp 
 |-  dom ( _I |` H ) C_ dom D
8 3 7 eqsstrri 
 |-  H C_ dom D
9 ssun1 
 |-  dom D C_ ( dom D u. ran D )
10 8 9 sstri 
 |-  H C_ ( dom D u. ran D )
11 dmrnssfld 
 |-  ( dom D u. ran D ) C_ U. U. D
12 10 11 sstri 
 |-  H C_ U. U. D
13 4 simpri 
 |-  D C_ ( H X. H )
14 uniss 
 |-  ( D C_ ( H X. H ) -> U. D C_ U. ( H X. H ) )
15 uniss 
 |-  ( U. D C_ U. ( H X. H ) -> U. U. D C_ U. U. ( H X. H ) )
16 13 14 15 mp2b 
 |-  U. U. D C_ U. U. ( H X. H )
17 unixpss 
 |-  U. U. ( H X. H ) C_ ( H u. H )
18 unidm 
 |-  ( H u. H ) = H
19 17 18 sseqtri 
 |-  U. U. ( H X. H ) C_ H
20 16 19 sstri 
 |-  U. U. D C_ H
21 12 20 eqssi 
 |-  H = U. U. D
22 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ n e. F ) -> n C_ X )
23 xpss2 
 |-  ( n C_ X -> ( { n } X. n ) C_ ( { n } X. X ) )
24 22 23 syl 
 |-  ( ( F e. ( Fil ` X ) /\ n e. F ) -> ( { n } X. n ) C_ ( { n } X. X ) )
25 24 ralrimiva 
 |-  ( F e. ( Fil ` X ) -> A. n e. F ( { n } X. n ) C_ ( { n } X. X ) )
26 ss2iun 
 |-  ( A. n e. F ( { n } X. n ) C_ ( { n } X. X ) -> U_ n e. F ( { n } X. n ) C_ U_ n e. F ( { n } X. X ) )
27 25 26 syl 
 |-  ( F e. ( Fil ` X ) -> U_ n e. F ( { n } X. n ) C_ U_ n e. F ( { n } X. X ) )
28 iunxpconst 
 |-  U_ n e. F ( { n } X. X ) = ( F X. X )
29 27 28 sseqtrdi 
 |-  ( F e. ( Fil ` X ) -> U_ n e. F ( { n } X. n ) C_ ( F X. X ) )
30 1 29 eqsstrid 
 |-  ( F e. ( Fil ` X ) -> H C_ ( F X. X ) )
31 5 a1i 
 |-  ( F e. ( Fil ` X ) -> ( _I |` H ) C_ D )
32 2 relopabiv 
 |-  Rel D
33 31 32 jctil 
 |-  ( F e. ( Fil ` X ) -> ( Rel D /\ ( _I |` H ) C_ D ) )
34 simpl 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> F e. ( Fil ` X ) )
35 30 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> H C_ ( F X. X ) )
36 simprl 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> v e. H )
37 35 36 sseldd 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> v e. ( F X. X ) )
38 xp1st 
 |-  ( v e. ( F X. X ) -> ( 1st ` v ) e. F )
39 37 38 syl 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> ( 1st ` v ) e. F )
40 simprr 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> z e. H )
41 35 40 sseldd 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> z e. ( F X. X ) )
42 xp1st 
 |-  ( z e. ( F X. X ) -> ( 1st ` z ) e. F )
43 41 42 syl 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> ( 1st ` z ) e. F )
44 filinn0 
 |-  ( ( F e. ( Fil ` X ) /\ ( 1st ` v ) e. F /\ ( 1st ` z ) e. F ) -> ( ( 1st ` v ) i^i ( 1st ` z ) ) =/= (/) )
45 34 39 43 44 syl3anc 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> ( ( 1st ` v ) i^i ( 1st ` z ) ) =/= (/) )
46 n0 
 |-  ( ( ( 1st ` v ) i^i ( 1st ` z ) ) =/= (/) <-> E. u u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) )
47 45 46 sylib 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> E. u u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) )
48 36 adantr 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) /\ u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) ) -> v e. H )
49 filin 
 |-  ( ( F e. ( Fil ` X ) /\ ( 1st ` v ) e. F /\ ( 1st ` z ) e. F ) -> ( ( 1st ` v ) i^i ( 1st ` z ) ) e. F )
50 34 39 43 49 syl3anc 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> ( ( 1st ` v ) i^i ( 1st ` z ) ) e. F )
51 50 adantr 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) /\ u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) ) -> ( ( 1st ` v ) i^i ( 1st ` z ) ) e. F )
52 simpr 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) /\ u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) ) -> u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) )
53 id 
 |-  ( n = ( ( 1st ` v ) i^i ( 1st ` z ) ) -> n = ( ( 1st ` v ) i^i ( 1st ` z ) ) )
54 53 opeliunxp2 
 |-  ( <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. e. U_ n e. F ( { n } X. n ) <-> ( ( ( 1st ` v ) i^i ( 1st ` z ) ) e. F /\ u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) ) )
55 51 52 54 sylanbrc 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) /\ u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) ) -> <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. e. U_ n e. F ( { n } X. n ) )
56 55 1 eleqtrrdi 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) /\ u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) ) -> <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. e. H )
57 fvex 
 |-  ( 1st ` v ) e. _V
58 57 inex1 
 |-  ( ( 1st ` v ) i^i ( 1st ` z ) ) e. _V
59 vex 
 |-  u e. _V
60 58 59 op1st 
 |-  ( 1st ` <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. ) = ( ( 1st ` v ) i^i ( 1st ` z ) )
61 inss1 
 |-  ( ( 1st ` v ) i^i ( 1st ` z ) ) C_ ( 1st ` v )
62 60 61 eqsstri 
 |-  ( 1st ` <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. ) C_ ( 1st ` v )
63 vex 
 |-  v e. _V
64 opex 
 |-  <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. e. _V
65 1 2 63 64 filnetlem1 
 |-  ( v D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. <-> ( ( v e. H /\ <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. e. H ) /\ ( 1st ` <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. ) C_ ( 1st ` v ) ) )
66 62 65 mpbiran2 
 |-  ( v D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. <-> ( v e. H /\ <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. e. H ) )
67 48 56 66 sylanbrc 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) /\ u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) ) -> v D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. )
68 40 adantr 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) /\ u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) ) -> z e. H )
69 inss2 
 |-  ( ( 1st ` v ) i^i ( 1st ` z ) ) C_ ( 1st ` z )
70 60 69 eqsstri 
 |-  ( 1st ` <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. ) C_ ( 1st ` z )
71 vex 
 |-  z e. _V
72 1 2 71 64 filnetlem1 
 |-  ( z D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. <-> ( ( z e. H /\ <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. e. H ) /\ ( 1st ` <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. ) C_ ( 1st ` z ) ) )
73 70 72 mpbiran2 
 |-  ( z D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. <-> ( z e. H /\ <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. e. H ) )
74 68 56 73 sylanbrc 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) /\ u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) ) -> z D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. )
75 breq2 
 |-  ( w = <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. -> ( v D w <-> v D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. ) )
76 breq2 
 |-  ( w = <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. -> ( z D w <-> z D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. ) )
77 75 76 anbi12d 
 |-  ( w = <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. -> ( ( v D w /\ z D w ) <-> ( v D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. /\ z D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. ) ) )
78 64 77 spcev 
 |-  ( ( v D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. /\ z D <. ( ( 1st ` v ) i^i ( 1st ` z ) ) , u >. ) -> E. w ( v D w /\ z D w ) )
79 67 74 78 syl2anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) /\ u e. ( ( 1st ` v ) i^i ( 1st ` z ) ) ) -> E. w ( v D w /\ z D w ) )
80 47 79 exlimddv 
 |-  ( ( F e. ( Fil ` X ) /\ ( v e. H /\ z e. H ) ) -> E. w ( v D w /\ z D w ) )
81 80 ralrimivva 
 |-  ( F e. ( Fil ` X ) -> A. v e. H A. z e. H E. w ( v D w /\ z D w ) )
82 codir 
 |-  ( ( H X. H ) C_ ( `' D o. D ) <-> A. v e. H A. z e. H E. w ( v D w /\ z D w ) )
83 81 82 sylibr 
 |-  ( F e. ( Fil ` X ) -> ( H X. H ) C_ ( `' D o. D ) )
84 vex 
 |-  w e. _V
85 1 2 63 84 filnetlem1 
 |-  ( v D w <-> ( ( v e. H /\ w e. H ) /\ ( 1st ` w ) C_ ( 1st ` v ) ) )
86 85 simplbi 
 |-  ( v D w -> ( v e. H /\ w e. H ) )
87 86 simpld 
 |-  ( v D w -> v e. H )
88 1 2 84 71 filnetlem1 
 |-  ( w D z <-> ( ( w e. H /\ z e. H ) /\ ( 1st ` z ) C_ ( 1st ` w ) ) )
89 88 simplbi 
 |-  ( w D z -> ( w e. H /\ z e. H ) )
90 89 simprd 
 |-  ( w D z -> z e. H )
91 87 90 anim12i 
 |-  ( ( v D w /\ w D z ) -> ( v e. H /\ z e. H ) )
92 88 simprbi 
 |-  ( w D z -> ( 1st ` z ) C_ ( 1st ` w ) )
93 85 simprbi 
 |-  ( v D w -> ( 1st ` w ) C_ ( 1st ` v ) )
94 92 93 sylan9ssr 
 |-  ( ( v D w /\ w D z ) -> ( 1st ` z ) C_ ( 1st ` v ) )
95 1 2 63 71 filnetlem1 
 |-  ( v D z <-> ( ( v e. H /\ z e. H ) /\ ( 1st ` z ) C_ ( 1st ` v ) ) )
96 91 94 95 sylanbrc 
 |-  ( ( v D w /\ w D z ) -> v D z )
97 96 ax-gen 
 |-  A. z ( ( v D w /\ w D z ) -> v D z )
98 97 gen2 
 |-  A. v A. w A. z ( ( v D w /\ w D z ) -> v D z )
99 cotr 
 |-  ( ( D o. D ) C_ D <-> A. v A. w A. z ( ( v D w /\ w D z ) -> v D z ) )
100 98 99 mpbir 
 |-  ( D o. D ) C_ D
101 83 100 jctil 
 |-  ( F e. ( Fil ` X ) -> ( ( D o. D ) C_ D /\ ( H X. H ) C_ ( `' D o. D ) ) )
102 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
103 xpexg 
 |-  ( ( F e. ( Fil ` X ) /\ X e. F ) -> ( F X. X ) e. _V )
104 102 103 mpdan 
 |-  ( F e. ( Fil ` X ) -> ( F X. X ) e. _V )
105 104 30 ssexd 
 |-  ( F e. ( Fil ` X ) -> H e. _V )
106 105 105 xpexd 
 |-  ( F e. ( Fil ` X ) -> ( H X. H ) e. _V )
107 ssexg 
 |-  ( ( D C_ ( H X. H ) /\ ( H X. H ) e. _V ) -> D e. _V )
108 13 106 107 sylancr 
 |-  ( F e. ( Fil ` X ) -> D e. _V )
109 21 isdir 
 |-  ( D e. _V -> ( D e. DirRel <-> ( ( Rel D /\ ( _I |` H ) C_ D ) /\ ( ( D o. D ) C_ D /\ ( H X. H ) C_ ( `' D o. D ) ) ) ) )
110 108 109 syl 
 |-  ( F e. ( Fil ` X ) -> ( D e. DirRel <-> ( ( Rel D /\ ( _I |` H ) C_ D ) /\ ( ( D o. D ) C_ D /\ ( H X. H ) C_ ( `' D o. D ) ) ) ) )
111 33 101 110 mpbir2and 
 |-  ( F e. ( Fil ` X ) -> D e. DirRel )
112 30 111 jca 
 |-  ( F e. ( Fil ` X ) -> ( H C_ ( F X. X ) /\ D e. DirRel ) )
113 21 112 pm3.2i 
 |-  ( H = U. U. D /\ ( F e. ( Fil ` X ) -> ( H C_ ( F X. X ) /\ D e. DirRel ) ) )