Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  filnetlem4 Unicode version

Theorem filnetlem4 25654
Description: Lemma for filnet 25655. (Contributed by Jeff Hankins, 15-Dec-2009.) (Revised by Mario Carneiro, 8-Aug-2015.)
Hypotheses
Ref Expression
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
Ref Expression
filnetlem4  |-  ( F  e.  ( Fil `  X
)  ->  E. d  e.  DirRel  E. f ( f : dom  d --> X  /\  F  =  ( ( X  FilMap  f ) `
 ran  ( tail `  d ) ) ) )
Distinct variable groups:    x, y    f, d, n, x, y, F    H, d, f, x, y    D, d, f    X, d, f, n
Allowed substitution hints:    D( x, y, n)    H( n)    X( x, y)

Proof of Theorem filnetlem4
Dummy variables  k  m  t  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 filnet.h . . . . 5  |-  H  = 
U_ n  e.  F  ( { n }  X.  n )
2 filnet.d . . . . 5  |-  D  =  { <. x ,  y
>.  |  ( (
x  e.  H  /\  y  e.  H )  /\  ( 1st `  y
)  C_  ( 1st `  x ) ) }
31, 2filnetlem3 25653 . . . 4  |-  ( H  =  U. U. D  /\  ( F  e.  ( Fil `  X )  ->  ( H  C_  ( F  X.  X
)  /\  D  e.  DirRel ) ) )
43simpri 448 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( H  C_  ( F  X.  X
)  /\  D  e.  DirRel ) )
54simprd 449 . 2  |-  ( F  e.  ( Fil `  X
)  ->  D  e.  DirRel )
6 f2ndres 6229 . . . . 5  |-  ( 2nd  |`  ( F  X.  X
) ) : ( F  X.  X ) --> X
74simpld 445 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  H  C_  ( F  X.  X ) )
8 fssres2 5492 . . . . 5  |-  ( ( ( 2nd  |`  ( F  X.  X ) ) : ( F  X.  X ) --> X  /\  H  C_  ( F  X.  X ) )  -> 
( 2nd  |`  H ) : H --> X )
96, 7, 8sylancr 644 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H ) : H --> X )
10 filtop 17652 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  X  e.  F )
11 xpexg 4882 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  X  e.  F )  ->  ( F  X.  X )  e. 
_V )
1210, 11mpdan 649 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( F  X.  X )  e.  _V )
13 ssexg 4241 . . . . 5  |-  ( ( H  C_  ( F  X.  X )  /\  ( F  X.  X )  e. 
_V )  ->  H  e.  _V )
147, 12, 13syl2anc 642 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  H  e.  _V )
15 fex 5835 . . . 4  |-  ( ( ( 2nd  |`  H ) : H --> X  /\  H  e.  _V )  ->  ( 2nd  |`  H )  e.  _V )
169, 14, 15syl2anc 642 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H )  e.  _V )
17 dirdm 14455 . . . . . . . 8  |-  ( D  e.  DirRel  ->  dom  D  =  U. U. D )
185, 17syl 15 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  dom  D  = 
U. U. D )
193simpli 444 . . . . . . 7  |-  H  = 
U. U. D
2018, 19syl6reqr 2409 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  H  =  dom  D )
2120feq2d 5462 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( ( 2nd  |`  H ) : H --> X  <->  ( 2nd  |`  H ) : dom  D --> X ) )
229, 21mpbid 201 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H ) : dom  D --> X )
23 eqid 2358 . . . . . . . . . . . . . 14  |-  dom  D  =  dom  D
2423tailf 25648 . . . . . . . . . . . . 13  |-  ( D  e.  DirRel  ->  ( tail `  D
) : dom  D --> ~P dom  D )
255, 24syl 15 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  ( tail `  D ) : dom  D --> ~P dom  D )
2620feq2d 5462 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  ( ( tail `  D ) : H --> ~P dom  D  <->  (
tail `  D ) : dom  D --> ~P dom  D ) )
2725, 26mpbird 223 . . . . . . . . . . 11  |-  ( F  e.  ( Fil `  X
)  ->  ( tail `  D ) : H --> ~P dom  D )
2827adantr 451 . . . . . . . . . 10  |-  ( ( F  e.  ( Fil `  X )  /\  t  C_  X )  ->  ( tail `  D ) : H --> ~P dom  D
)
29 ffn 5472 . . . . . . . . . 10  |-  ( (
tail `  D ) : H --> ~P dom  D  ->  ( tail `  D
)  Fn  H )
30 imaeq2 5090 . . . . . . . . . . . 12  |-  ( d  =  ( ( tail `  D ) `  f
)  ->  ( ( 2nd  |`  H ) "
d )  =  ( ( 2nd  |`  H )
" ( ( tail `  D ) `  f
) ) )
3130sseq1d 3281 . . . . . . . . . . 11  |-  ( d  =  ( ( tail `  D ) `  f
)  ->  ( (
( 2nd  |`  H )
" d )  C_  t 
<->  ( ( 2nd  |`  H )
" ( ( tail `  D ) `  f
) )  C_  t
) )
3231rexrn 5750 . . . . . . . . . 10  |-  ( (
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
) )
3328, 29, 323syl 18 . . . . . . . . 9  |-  ( ( 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
) )
34 fo2nd 6227 . . . . . . . . . . . . . . 15  |-  2nd : _V -onto-> _V
35 fofn 5536 . . . . . . . . . . . . . . 15  |-  ( 2nd
: _V -onto-> _V  ->  2nd 
Fn  _V )
3634, 35ax-mp 8 . . . . . . . . . . . . . 14  |-  2nd  Fn  _V
37 ssv 3274 . . . . . . . . . . . . . 14  |-  H  C_  _V
38 fnssres 5439 . . . . . . . . . . . . . 14  |-  ( ( 2nd  Fn  _V  /\  H  C_  _V )  -> 
( 2nd  |`  H )  Fn  H )
3936, 37, 38mp2an 653 . . . . . . . . . . . . 13  |-  ( 2nd  |`  H )  Fn  H
40 fnfun 5423 . . . . . . . . . . . . 13  |-  ( ( 2nd  |`  H )  Fn  H  ->  Fun  ( 2nd  |`  H ) )
4139, 40ax-mp 8 . . . . . . . . . . . 12  |-  Fun  ( 2nd  |`  H )
42 ffvelrn 5746 . . . . . . . . . . . . . . . 16  |-  ( ( ( tail `  D
) : H --> ~P dom  D  /\  f  e.  H
)  ->  ( ( tail `  D ) `  f )  e.  ~P dom  D )
4328, 42sylan 457 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  e.  ~P dom  D )
44 elpwi 3709 . . . . . . . . . . . . . . 15  |-  ( ( ( tail `  D
) `  f )  e.  ~P dom  D  -> 
( ( tail `  D
) `  f )  C_ 
dom  D )
4543, 44syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  dom  D )
4620ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  H  =  dom  D )
4745, 46sseqtr4d 3291 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  H
)
48 fndm 5425 . . . . . . . . . . . . . 14  |-  ( ( 2nd  |`  H )  Fn  H  ->  dom  ( 2nd  |`  H )  =  H )
4939, 48ax-mp 8 . . . . . . . . . . . . 13  |-  dom  ( 2nd  |`  H )  =  H
5047, 49syl6sseqr 3301 . . . . . . . . . . . 12  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  dom  ( 2nd  |`  H )
)
51 funimass4 5656 . . . . . . . . . . . 12  |-  ( ( 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 ) )
5241, 50, 51sylancr 644 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
535ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  D  e.  DirRel )
54 simpr 447 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  f  e.  H )
5554, 46eleqtrd 2434 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  f  e.  dom  D )
56 vex 2867 . . . . . . . . . . . . . . . . 17  |-  d  e. 
_V
5756a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  d  e.  _V )
5823eltail 25647 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  DirRel  /\  f  e.  dom  D  /\  d  e.  _V )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  f D
d ) )
5953, 55, 57, 58syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  f D
d ) )
6054biantrurd 494 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
d  e.  H  <->  ( f  e.  H  /\  d  e.  H ) ) )
6160anbi1d 685 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) ) )
62 vex 2867 . . . . . . . . . . . . . . . . 17  |-  f  e. 
_V
631, 2, 62, 56filnetlem1 25651 . . . . . . . . . . . . . . . 16  |-  ( f D d  <->  ( (
f  e.  H  /\  d  e.  H )  /\  ( 1st `  d
)  C_  ( 1st `  f ) ) )
6461, 63syl6bbr 254 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( d  e.  H  /\  ( 1st `  d
)  C_  ( 1st `  f ) )  <->  f D
d ) )
6559, 64bitr4d 247 . . . . . . . . . . . . . 14  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  ( d  e.  H  /\  ( 1st `  d )  C_  ( 1st `  f ) ) ) )
6665imbi1d 308 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
67 fvres 5625 . . . . . . . . . . . . . . . . 17  |-  ( d  e.  H  ->  (
( 2nd  |`  H ) `
 d )  =  ( 2nd `  d
) )
6867eleq1d 2424 . . . . . . . . . . . . . . . 16  |-  ( d  e.  H  ->  (
( ( 2nd  |`  H ) `
 d )  e.  t  <->  ( 2nd `  d
)  e.  t ) )
6968adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( d  e.  H  /\  ( 1st `  d ) 
C_  ( 1st `  f
) )  ->  (
( ( 2nd  |`  H ) `
 d )  e.  t  <->  ( 2nd `  d
)  e.  t ) )
7069pm5.74i 236 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) )
71 impexp 433 . . . . . . . . . . . . . 14  |-  ( ( ( d  e.  H  /\  ( 1st `  d
)  C_  ( 1st `  f ) )  -> 
( 2nd `  d
)  e.  t )  <-> 
( d  e.  H  ->  ( ( 1st `  d
)  C_  ( 1st `  f )  ->  ( 2nd `  d )  e.  t ) ) )
7270, 71bitri 240 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
7366, 72syl6bb 252 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) )
7473ralbidv2 2641 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
7552, 74bitrd 244 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
7675rexbidva 2636 . . . . . . . . 9  |-  ( ( 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 ) ) )
77 vex 2867 . . . . . . . . . . . . . . . . 17  |-  k  e. 
_V
78 vex 2867 . . . . . . . . . . . . . . . . 17  |-  v  e. 
_V
7977, 78op1std 6217 . . . . . . . . . . . . . . . 16  |-  ( d  =  <. k ,  v
>.  ->  ( 1st `  d
)  =  k )
8079sseq1d 3281 . . . . . . . . . . . . . . 15  |-  ( d  =  <. k ,  v
>.  ->  ( ( 1st `  d )  C_  ( 1st `  f )  <->  k  C_  ( 1st `  f ) ) )
8177, 78op2ndd 6218 . . . . . . . . . . . . . . . 16  |-  ( d  =  <. k ,  v
>.  ->  ( 2nd `  d
)  =  v )
8281eleq1d 2424 . . . . . . . . . . . . . . 15  |-  ( d  =  <. k ,  v
>.  ->  ( ( 2nd `  d )  e.  t  <-> 
v  e.  t ) )
8380, 82imbi12d 311 . . . . . . . . . . . . . 14  |-  ( d  =  <. k ,  v
>.  ->  ( ( ( 1st `  d ) 
C_  ( 1st `  f
)  ->  ( 2nd `  d )  e.  t )  <->  ( k  C_  ( 1st `  f )  ->  v  e.  t ) ) )
8483raliunxp 4907 . . . . . . . . . . . . 13  |-  ( 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 ) )
85 sneq 3727 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  { n }  =  { k } )
86 id 19 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  n  =  k )
8785, 86xpeq12d 4796 . . . . . . . . . . . . . . . 16  |-  ( n  =  k  ->  ( { n }  X.  n )  =  ( { k }  X.  k ) )
8887cbviunv 4022 . . . . . . . . . . . . . . 15  |-  U_ n  e.  F  ( {
n }  X.  n
)  =  U_ k  e.  F  ( {
k }  X.  k
)
891, 88eqtri 2378 . . . . . . . . . . . . . 14  |-  H  = 
U_ k  e.  F  ( { k }  X.  k )
9089raleqi 2816 . . . . . . . . . . . . 13  |-  ( 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 ) )
91 dfss3 3246 . . . . . . . . . . . . . . . 16  |-  ( k 
C_  t  <->  A. v  e.  k  v  e.  t )
9291imbi2i 303 . . . . . . . . . . . . . . 15  |-  ( ( k  C_  ( 1st `  f )  ->  k  C_  t )  <->  ( k  C_  ( 1st `  f
)  ->  A. v  e.  k  v  e.  t ) )
93 r19.21v 2706 . . . . . . . . . . . . . . 15  |-  ( A. v  e.  k  (
k  C_  ( 1st `  f )  ->  v  e.  t )  <->  ( k  C_  ( 1st `  f
)  ->  A. v  e.  k  v  e.  t ) )
9492, 93bitr4i 243 . . . . . . . . . . . . . 14  |-  ( ( k  C_  ( 1st `  f )  ->  k  C_  t )  <->  A. v  e.  k  ( k  C_  ( 1st `  f
)  ->  v  e.  t ) )
9594ralbii 2643 . . . . . . . . . . . . 13  |-  ( 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 ) )
9684, 90, 953bitr4i 268 . . . . . . . . . . . 12  |-  ( A. d  e.  H  (
( 1st `  d
)  C_  ( 1st `  f )  ->  ( 2nd `  d )  e.  t )  <->  A. k  e.  F  ( k  C_  ( 1st `  f
)  ->  k  C_  t ) )
9796rexbii 2644 . . . . . . . . . . 11  |-  ( 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 ) )
981rexeqi 2817 . . . . . . . . . . 11  |-  ( 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 ) )
99 vex 2867 . . . . . . . . . . . . . . . 16  |-  n  e. 
_V
100 vex 2867 . . . . . . . . . . . . . . . 16  |-  m  e. 
_V
10199, 100op1std 6217 . . . . . . . . . . . . . . 15  |-  ( f  =  <. n ,  m >.  ->  ( 1st `  f
)  =  n )
102101sseq2d 3282 . . . . . . . . . . . . . 14  |-  ( f  =  <. n ,  m >.  ->  ( k  C_  ( 1st `  f )  <-> 
k  C_  n )
)
103102imbi1d 308 . . . . . . . . . . . . 13  |-  ( f  =  <. n ,  m >.  ->  ( ( k 
C_  ( 1st `  f
)  ->  k  C_  t )  <->  ( k  C_  n  ->  k  C_  t ) ) )
104103ralbidv 2639 . . . . . . . . . . . 12  |-  ( f  =  <. n ,  m >.  ->  ( A. k  e.  F  ( k  C_  ( 1st `  f
)  ->  k  C_  t )  <->  A. k  e.  F  ( k  C_  n  ->  k  C_  t ) ) )
105104rexiunxp 4908 . . . . . . . . . . 11  |-  ( 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 )
)
10697, 98, 1053bitri 262 . . . . . . . . . 10  |-  ( 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 ) )
107 fileln0 17647 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  n  =/=  (/) )
108107adantlr 695 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  n  e.  F )  ->  n  =/=  (/) )
109 r19.9rzv 3624 . . . . . . . . . . . . 13  |-  ( 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 ) ) )
110108, 109syl 15 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
111 ssid 3273 . . . . . . . . . . . . . . 15  |-  n  C_  n
112 sseq1 3275 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  (
k  C_  n  <->  n  C_  n
) )
113 sseq1 3275 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  (
k  C_  t  <->  n  C_  t
) )
114112, 113imbi12d 311 . . . . . . . . . . . . . . . 16  |-  ( k  =  n  ->  (
( k  C_  n  ->  k  C_  t )  <->  ( n  C_  n  ->  n 
C_  t ) ) )
115114rspcv 2956 . . . . . . . . . . . . . . 15  |-  ( n  e.  F  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  ->  ( n  C_  n  ->  n  C_  t )
) )
116111, 115mpii 39 . . . . . . . . . . . . . 14  |-  ( n  e.  F  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  ->  n  C_  t )
)
117116adantl 452 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  n  e.  F )  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  ->  n  C_  t )
)
118 sstr2 3262 . . . . . . . . . . . . . . 15  |-  ( k 
C_  n  ->  (
n  C_  t  ->  k 
C_  t ) )
119118com12 27 . . . . . . . . . . . . . 14  |-  ( n 
C_  t  ->  (
k  C_  n  ->  k 
C_  t ) )
120119ralrimivw 2703 . . . . . . . . . . . . 13  |-  ( n 
C_  t  ->  A. k  e.  F  ( k  C_  n  ->  k  C_  t ) )
121117, 120impbid1 194 . . . . . . . . . . . 12  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  n  e.  F )  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  <->  n 
C_  t ) )
122110, 121bitr3d 246 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
123122rexbidva 2636 . . . . . . . . . 10  |-  ( ( 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 ) )
124106, 123syl5bb 248 . . . . . . . . 9  |-  ( ( 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
) )
12533, 76, 1243bitrd 270 . . . . . . . 8  |-  ( ( 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 ) )
126125pm5.32da 622 . . . . . . 7  |-  ( 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
) ) )
127 filn0 17659 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  F  =/=  (/) )
12899snnz 3820 . . . . . . . . . . . . . . . 16  |-  { n }  =/=  (/)
129107, 128jctil 523 . . . . . . . . . . . . . . 15  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  ( { n }  =/=  (/) 
/\  n  =/=  (/) ) )
130 neanior 2606 . . . . . . . . . . . . . . 15  |-  ( ( { n }  =/=  (/) 
/\  n  =/=  (/) )  <->  -.  ( { n }  =  (/) 
\/  n  =  (/) ) )
131129, 130sylib 188 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  -.  ( { n }  =  (/) 
\/  n  =  (/) ) )
132 ss0b 3560 . . . . . . . . . . . . . . 15  |-  ( ( { n }  X.  n )  C_  (/)  <->  ( {
n }  X.  n
)  =  (/) )
133 xpeq0 5182 . . . . . . . . . . . . . . 15  |-  ( ( { n }  X.  n )  =  (/)  <->  ( { n }  =  (/) 
\/  n  =  (/) ) )
134132, 133bitri 240 . . . . . . . . . . . . . 14  |-  ( ( { n }  X.  n )  C_  (/)  <->  ( {
n }  =  (/)  \/  n  =  (/) ) )
135131, 134sylnibr 296 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  -.  ( { n }  X.  n )  C_  (/) )
136135ralrimiva 2702 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  A. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
137 r19.2z 3619 . . . . . . . . . . . 12  |-  ( ( F  =/=  (/)  /\  A. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )  ->  E. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
138127, 136, 137syl2anc 642 . . . . . . . . . . 11  |-  ( F  e.  ( Fil `  X
)  ->  E. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
139 rexnal 2630 . . . . . . . . . . 11  |-  ( E. n  e.  F  -.  ( { n }  X.  n )  C_  (/)  <->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
140138, 139sylib 188 . . . . . . . . . 10  |-  ( F  e.  ( Fil `  X
)  ->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
1411sseq1i 3278 . . . . . . . . . . . 12  |-  ( H 
C_  (/)  <->  U_ n  e.  F  ( { n }  X.  n )  C_  (/) )
142 ss0b 3560 . . . . . . . . . . . 12  |-  ( H 
C_  (/)  <->  H  =  (/) )
143 iunss 4024 . . . . . . . . . . . 12  |-  ( U_ n  e.  F  ( { n }  X.  n )  C_  (/)  <->  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
144141, 142, 1433bitr3i 266 . . . . . . . . . . 11  |-  ( H  =  (/)  <->  A. n  e.  F  ( { n }  X.  n )  C_  (/) )
145144necon3abii 2551 . . . . . . . . . 10  |-  ( H  =/=  (/)  <->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
146140, 145sylibr 203 . . . . . . . . 9  |-  ( F  e.  ( Fil `  X
)  ->  H  =/=  (/) )
147 dmresi 5087 . . . . . . . . . . . 12  |-  dom  (  _I  |`  H )  =  H
1481, 2filnetlem2 25652 . . . . . . . . . . . . . 14  |-  ( (  _I  |`  H )  C_  D  /\  D  C_  ( H  X.  H
) )
149148simpli 444 . . . . . . . . . . . . 13  |-  (  _I  |`  H )  C_  D
150 dmss 4960 . . . . . . . . . . . . 13  |-  ( (  _I  |`  H )  C_  D  ->  dom  (  _I  |`  H )  C_  dom  D )
151149, 150ax-mp 8 . . . . . . . . . . . 12  |-  dom  (  _I  |`  H )  C_  dom  D
152147, 151eqsstr3i 3285 . . . . . . . . . . 11  |-  H  C_  dom  D
153148simpri 448 . . . . . . . . . . . . 13  |-  D  C_  ( H  X.  H
)
154 dmss 4960 . . . . . . . . . . . . 13  |-  ( D 
C_  ( H  X.  H )  ->  dom  D 
C_  dom  ( H  X.  H ) )
155153, 154ax-mp 8 . . . . . . . . . . . 12  |-  dom  D  C_ 
dom  ( H  X.  H )
156 dmxpid 4980 . . . . . . . . . . . 12  |-  dom  ( H  X.  H )  =  H
157155, 156sseqtri 3286 . . . . . . . . . . 11  |-  dom  D  C_  H
158152, 157eqssi 3271 . . . . . . . . . 10  |-  H  =  dom  D
159158tailfb 25650 . . . . . . . . 9  |-  ( ( D  e.  DirRel  /\  H  =/=  (/) )  ->  ran  ( tail `  D )  e.  ( fBas `  H
) )
1605, 146, 159syl2anc 642 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  ran  ( tail `  D )  e.  (
fBas `  H )
)
161 elfm 17744 . . . . . . . 8  |-  ( ( 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 )
) )
16210, 160, 9, 161syl3anc 1182 . . . . . . 7  |-  ( 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 )
) )
163 filfbas 17645 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  F  e.  ( fBas `  X )
)
164 elfg 17668 . . . . . . . 8  |-  ( F  e.  ( fBas `  X
)  ->  ( t  e.  ( X filGen F )  <-> 
( t  C_  X  /\  E. n  e.  F  n  C_  t ) ) )
165163, 164syl 15 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  ( t  e.  ( X filGen F )  <-> 
( t  C_  X  /\  E. n  e.  F  n  C_  t ) ) )
166126, 162, 1653bitr4d 276 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  ( t  e.  ( ( X  FilMap  ( 2nd  |`  H )
) `  ran  ( tail `  D ) )  <->  t  e.  ( X filGen F ) ) )
167166eqrdv 2356 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) )  =  ( X filGen F ) )
168 fgfil 17672 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( X filGen F )  =  F )
169167, 168eqtr2d 2391 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  F  =  ( ( X  FilMap  ( 2nd  |`  H )
) `  ran  ( tail `  D ) ) )
17022, 169jca 518 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( ( 2nd  |`  H ) : dom  D --> X  /\  F  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) ) )
171 feq1 5457 . . . . 5  |-  ( f  =  ( 2nd  |`  H )  ->  ( f : dom  D --> X  <->  ( 2nd  |`  H ) : dom  D --> X ) )
172 oveq2 5953 . . . . . . 7  |-  ( f  =  ( 2nd  |`  H )  ->  ( X  FilMap  f )  =  ( X 
FilMap  ( 2nd  |`  H ) ) )
173172fveq1d 5610 . . . . . 6  |-  ( f  =  ( 2nd  |`  H )  ->  ( ( X 
FilMap  f ) `  ran  ( tail `  D )
)  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) )
174173eqeq2d 2369 . . . . 5  |-  ( f  =  ( 2nd  |`  H )  ->  ( F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) )  <-> 
F  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) ) )
175171, 174anbi12d 691 . . . 4  |-  ( 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 ) ) ) ) )
176175spcegv 2945 . . 3  |-  ( ( 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 ) ) ) ) )
17716, 170, 176sylc 56 . 2  |-  ( F  e.  ( Fil `  X
)  ->  E. f
( f : dom  D --> X  /\  F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) ) )
178 dmeq 4961 . . . . . 6  |-  ( d  =  D  ->  dom  d  =  dom  D )
179178feq2d 5462 . . . . 5  |-  ( d  =  D  ->  (
f : dom  d --> X 
<->  f : dom  D --> X ) )
180 fveq2 5608 . . . . . . . 8  |-  ( d  =  D  ->  ( tail `  d )  =  ( tail `  D
) )
181180rneqd 4988 . . . . . . 7  |-  ( d  =  D  ->  ran  ( tail `  d )  =  ran  ( tail `  D
) )
182181fveq2d 5612 . . . . . 6  |-  ( d  =  D  ->  (
( X  FilMap  f ) `
 ran  ( tail `  d ) )  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) )
183182eqeq2d 2369 . . . . 5  |-  ( d  =  D  ->  ( F  =  ( ( X  FilMap  f ) `  ran  ( tail `  d
) )  <->  F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) ) )
184179, 183anbi12d 691 . . . 4  |-  ( d  =  D  ->  (
( f : dom  d
--> X  /\  F  =  ( ( X  FilMap  f ) `  ran  ( tail `  d ) ) )  <->  ( f : dom  D --> X  /\  F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D
) ) ) ) )
185184exbidv 1626 . . 3  |-  ( 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 ) ) ) ) )
186185rspcev 2960 . 2  |-  ( ( 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
) ) ) )
1875, 177, 186syl2anc 642 1  |-  ( F  e.  ( Fil `  X
)  ->  E. d  e.  DirRel  E. f ( f : dom  d --> X  /\  F  =  ( ( X  FilMap  f ) `
 ran  ( tail `  d ) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358   E.wex 1541    = wceq 1642    e. wcel 1710    =/= wne 2521   A.wral 2619   E.wrex 2620   _Vcvv 2864    C_ wss 3228   (/)c0 3531   ~Pcpw 3701   {csn 3716   <.cop 3719   U.cuni 3908   U_ciun 3986   class class class wbr 4104   {copab 4157    _I cid 4386    X. cxp 4769   dom cdm 4771   ran crn 4772    |` cres 4773   "cima 4774   Fun wfun 5331    Fn wfn 5332   -->wf 5333   -onto->wfo 5335   ` cfv 5337  (class class class)co 5945   1stc1st 6207   2ndc2nd 6208   DirRelcdir 14449   tailctail 14450   fBascfbas 16471   filGencfg 16472   Filcfil 17642    FilMap cfm 17730
This theorem is referenced by:  filnet  25655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4212  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-iun 3988  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-ov 5948  df-oprab 5949  df-mpt2 5950  df-1st 6209  df-2nd 6210  df-dir 14451  df-tail 14452  df-fbas 16479  df-fg 16480  df-fil 17643  df-fm 17735
  Copyright terms: Public domain W3C validator