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

Theorem filnetlem4 28599
Description: Lemma for filnet 28600. (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 28598 . . . 4  |-  ( H  =  U. U. D  /\  ( F  e.  ( Fil `  X )  ->  ( H  C_  ( F  X.  X
)  /\  D  e.  DirRel ) ) )
43simpri 462 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( H  C_  ( F  X.  X
)  /\  D  e.  DirRel ) )
54simprd 463 . 2  |-  ( F  e.  ( Fil `  X
)  ->  D  e.  DirRel )
6 f2ndres 6597 . . . . 5  |-  ( 2nd  |`  ( F  X.  X
) ) : ( F  X.  X ) --> X
74simpld 459 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  H  C_  ( F  X.  X ) )
8 fssres2 5577 . . . . 5  |-  ( ( ( 2nd  |`  ( F  X.  X ) ) : ( F  X.  X ) --> X  /\  H  C_  ( F  X.  X ) )  -> 
( 2nd  |`  H ) : H --> X )
96, 7, 8sylancr 663 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H ) : H --> X )
10 filtop 19426 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  X  e.  F )
11 xpexg 6505 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  X  e.  F )  ->  ( F  X.  X )  e. 
_V )
1210, 11mpdan 668 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( F  X.  X )  e.  _V )
1312, 7ssexd 4437 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  H  e.  _V )
14 fex 5948 . . . 4  |-  ( ( ( 2nd  |`  H ) : H --> X  /\  H  e.  _V )  ->  ( 2nd  |`  H )  e.  _V )
159, 13, 14syl2anc 661 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H )  e.  _V )
16 dirdm 15402 . . . . . . . 8  |-  ( D  e.  DirRel  ->  dom  D  =  U. U. D )
175, 16syl 16 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  dom  D  = 
U. U. D )
183simpli 458 . . . . . . 7  |-  H  = 
U. U. D
1917, 18syl6reqr 2492 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  H  =  dom  D )
2019feq2d 5545 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( ( 2nd  |`  H ) : H --> X  <->  ( 2nd  |`  H ) : dom  D --> X ) )
219, 20mpbid 210 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H ) : dom  D --> X )
22 eqid 2441 . . . . . . . . . . . . . 14  |-  dom  D  =  dom  D
2322tailf 28593 . . . . . . . . . . . . 13  |-  ( D  e.  DirRel  ->  ( tail `  D
) : dom  D --> ~P dom  D )
245, 23syl 16 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  ( tail `  D ) : dom  D --> ~P dom  D )
2519feq2d 5545 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  ( ( tail `  D ) : H --> ~P dom  D  <->  (
tail `  D ) : dom  D --> ~P dom  D ) )
2624, 25mpbird 232 . . . . . . . . . . 11  |-  ( F  e.  ( Fil `  X
)  ->  ( tail `  D ) : H --> ~P dom  D )
2726adantr 465 . . . . . . . . . 10  |-  ( ( F  e.  ( Fil `  X )  /\  t  C_  X )  ->  ( tail `  D ) : H --> ~P dom  D
)
28 ffn 5557 . . . . . . . . . 10  |-  ( (
tail `  D ) : H --> ~P dom  D  ->  ( tail `  D
)  Fn  H )
29 imaeq2 5163 . . . . . . . . . . . 12  |-  ( d  =  ( ( tail `  D ) `  f
)  ->  ( ( 2nd  |`  H ) "
d )  =  ( ( 2nd  |`  H )
" ( ( tail `  D ) `  f
) ) )
3029sseq1d 3381 . . . . . . . . . . 11  |-  ( d  =  ( ( tail `  D ) `  f
)  ->  ( (
( 2nd  |`  H )
" d )  C_  t 
<->  ( ( 2nd  |`  H )
" ( ( tail `  D ) `  f
) )  C_  t
) )
3130rexrn 5843 . . . . . . . . . 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
) )
3227, 28, 313syl 20 . . . . . . . . 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
) )
33 fo2nd 6595 . . . . . . . . . . . . . . 15  |-  2nd : _V -onto-> _V
34 fofn 5620 . . . . . . . . . . . . . . 15  |-  ( 2nd
: _V -onto-> _V  ->  2nd 
Fn  _V )
3533, 34ax-mp 5 . . . . . . . . . . . . . 14  |-  2nd  Fn  _V
36 ssv 3374 . . . . . . . . . . . . . 14  |-  H  C_  _V
37 fnssres 5522 . . . . . . . . . . . . . 14  |-  ( ( 2nd  Fn  _V  /\  H  C_  _V )  -> 
( 2nd  |`  H )  Fn  H )
3835, 36, 37mp2an 672 . . . . . . . . . . . . 13  |-  ( 2nd  |`  H )  Fn  H
39 fnfun 5506 . . . . . . . . . . . . 13  |-  ( ( 2nd  |`  H )  Fn  H  ->  Fun  ( 2nd  |`  H ) )
4038, 39ax-mp 5 . . . . . . . . . . . 12  |-  Fun  ( 2nd  |`  H )
4127ffvelrnda 5841 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  e.  ~P dom  D )
4241elpwid 3868 . . . . . . . . . . . . . 14  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  dom  D )
4319ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  H  =  dom  D )
4442, 43sseqtr4d 3391 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  H
)
45 fndm 5508 . . . . . . . . . . . . . 14  |-  ( ( 2nd  |`  H )  Fn  H  ->  dom  ( 2nd  |`  H )  =  H )
4638, 45ax-mp 5 . . . . . . . . . . . . 13  |-  dom  ( 2nd  |`  H )  =  H
4744, 46syl6sseqr 3401 . . . . . . . . . . . 12  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  dom  ( 2nd  |`  H )
)
48 funimass4 5740 . . . . . . . . . . . 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 ) )
4940, 47, 48sylancr 663 . . . . . . . . . . 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 ) )
505ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  D  e.  DirRel )
51 simpr 461 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  f  e.  H )
5251, 43eleqtrd 2517 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  f  e.  dom  D )
53 vex 2973 . . . . . . . . . . . . . . . . 17  |-  d  e. 
_V
5453a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  d  e.  _V )
5522eltail 28592 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  DirRel  /\  f  e.  dom  D  /\  d  e.  _V )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  f D
d ) )
5650, 52, 54, 55syl3anc 1218 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  f D
d ) )
5751biantrurd 508 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
d  e.  H  <->  ( f  e.  H  /\  d  e.  H ) ) )
5857anbi1d 704 . . . . . . . . . . . . . . . 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 ) ) ) )
59 vex 2973 . . . . . . . . . . . . . . . . 17  |-  f  e. 
_V
601, 2, 59, 53filnetlem1 28596 . . . . . . . . . . . . . . . 16  |-  ( f D d  <->  ( (
f  e.  H  /\  d  e.  H )  /\  ( 1st `  d
)  C_  ( 1st `  f ) ) )
6158, 60syl6bbr 263 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( d  e.  H  /\  ( 1st `  d
)  C_  ( 1st `  f ) )  <->  f D
d ) )
6256, 61bitr4d 256 . . . . . . . . . . . . . 14  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  ( d  e.  H  /\  ( 1st `  d )  C_  ( 1st `  f ) ) ) )
6362imbi1d 317 . . . . . . . . . . . . 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 ) ) )
64 fvres 5702 . . . . . . . . . . . . . . . . 17  |-  ( d  e.  H  ->  (
( 2nd  |`  H ) `
 d )  =  ( 2nd `  d
) )
6564eleq1d 2507 . . . . . . . . . . . . . . . 16  |-  ( d  e.  H  ->  (
( ( 2nd  |`  H ) `
 d )  e.  t  <->  ( 2nd `  d
)  e.  t ) )
6665adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( d  e.  H  /\  ( 1st `  d ) 
C_  ( 1st `  f
) )  ->  (
( ( 2nd  |`  H ) `
 d )  e.  t  <->  ( 2nd `  d
)  e.  t ) )
6766pm5.74i 245 . . . . . . . . . . . . . 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 ) )
68 impexp 446 . . . . . . . . . . . . . 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 ) ) )
6967, 68bitri 249 . . . . . . . . . . . . 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 ) ) )
7063, 69syl6bb 261 . . . . . . . . . . . 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 ) ) ) )
7170ralbidv2 2735 . . . . . . . . . . 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 ) ) )
7249, 71bitrd 253 . . . . . . . . . 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 ) ) )
7372rexbidva 2730 . . . . . . . . 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 ) ) )
74 vex 2973 . . . . . . . . . . . . . . . . 17  |-  k  e. 
_V
75 vex 2973 . . . . . . . . . . . . . . . . 17  |-  v  e. 
_V
7674, 75op1std 6585 . . . . . . . . . . . . . . . 16  |-  ( d  =  <. k ,  v
>.  ->  ( 1st `  d
)  =  k )
7776sseq1d 3381 . . . . . . . . . . . . . . 15  |-  ( d  =  <. k ,  v
>.  ->  ( ( 1st `  d )  C_  ( 1st `  f )  <->  k  C_  ( 1st `  f ) ) )
7874, 75op2ndd 6586 . . . . . . . . . . . . . . . 16  |-  ( d  =  <. k ,  v
>.  ->  ( 2nd `  d
)  =  v )
7978eleq1d 2507 . . . . . . . . . . . . . . 15  |-  ( d  =  <. k ,  v
>.  ->  ( ( 2nd `  d )  e.  t  <-> 
v  e.  t ) )
8077, 79imbi12d 320 . . . . . . . . . . . . . 14  |-  ( d  =  <. k ,  v
>.  ->  ( ( ( 1st `  d ) 
C_  ( 1st `  f
)  ->  ( 2nd `  d )  e.  t )  <->  ( k  C_  ( 1st `  f )  ->  v  e.  t ) ) )
8180raliunxp 4977 . . . . . . . . . . . . 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 ) )
82 sneq 3885 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  { n }  =  { k } )
83 id 22 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  n  =  k )
8482, 83xpeq12d 4863 . . . . . . . . . . . . . . . 16  |-  ( n  =  k  ->  ( { n }  X.  n )  =  ( { k }  X.  k ) )
8584cbviunv 4207 . . . . . . . . . . . . . . 15  |-  U_ n  e.  F  ( {
n }  X.  n
)  =  U_ k  e.  F  ( {
k }  X.  k
)
861, 85eqtri 2461 . . . . . . . . . . . . . 14  |-  H  = 
U_ k  e.  F  ( { k }  X.  k )
8786raleqi 2919 . . . . . . . . . . . . 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 ) )
88 dfss3 3344 . . . . . . . . . . . . . . . 16  |-  ( k 
C_  t  <->  A. v  e.  k  v  e.  t )
8988imbi2i 312 . . . . . . . . . . . . . . 15  |-  ( ( k  C_  ( 1st `  f )  ->  k  C_  t )  <->  ( k  C_  ( 1st `  f
)  ->  A. v  e.  k  v  e.  t ) )
90 r19.21v 2801 . . . . . . . . . . . . . . 15  |-  ( A. v  e.  k  (
k  C_  ( 1st `  f )  ->  v  e.  t )  <->  ( k  C_  ( 1st `  f
)  ->  A. v  e.  k  v  e.  t ) )
9189, 90bitr4i 252 . . . . . . . . . . . . . 14  |-  ( ( k  C_  ( 1st `  f )  ->  k  C_  t )  <->  A. v  e.  k  ( k  C_  ( 1st `  f
)  ->  v  e.  t ) )
9291ralbii 2737 . . . . . . . . . . . . 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 ) )
9381, 87, 923bitr4i 277 . . . . . . . . . . . 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 ) )
9493rexbii 2738 . . . . . . . . . . 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 ) )
951rexeqi 2920 . . . . . . . . . . 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 ) )
96 vex 2973 . . . . . . . . . . . . . . . 16  |-  n  e. 
_V
97 vex 2973 . . . . . . . . . . . . . . . 16  |-  m  e. 
_V
9896, 97op1std 6585 . . . . . . . . . . . . . . 15  |-  ( f  =  <. n ,  m >.  ->  ( 1st `  f
)  =  n )
9998sseq2d 3382 . . . . . . . . . . . . . 14  |-  ( f  =  <. n ,  m >.  ->  ( k  C_  ( 1st `  f )  <-> 
k  C_  n )
)
10099imbi1d 317 . . . . . . . . . . . . 13  |-  ( f  =  <. n ,  m >.  ->  ( ( k 
C_  ( 1st `  f
)  ->  k  C_  t )  <->  ( k  C_  n  ->  k  C_  t ) ) )
101100ralbidv 2733 . . . . . . . . . . . 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 ) ) )
102101rexiunxp 4978 . . . . . . . . . . 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 )
)
10394, 95, 1023bitri 271 . . . . . . . . . 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 ) )
104 fileln0 19421 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  n  =/=  (/) )
105104adantlr 714 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  n  e.  F )  ->  n  =/=  (/) )
106 r19.9rzv 3772 . . . . . . . . . . . . 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 ) ) )
107105, 106syl 16 . . . . . . . . . . . 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 ) ) )
108 ssid 3373 . . . . . . . . . . . . . . 15  |-  n  C_  n
109 sseq1 3375 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  (
k  C_  n  <->  n  C_  n
) )
110 sseq1 3375 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  (
k  C_  t  <->  n  C_  t
) )
111109, 110imbi12d 320 . . . . . . . . . . . . . . . 16  |-  ( k  =  n  ->  (
( k  C_  n  ->  k  C_  t )  <->  ( n  C_  n  ->  n 
C_  t ) ) )
112111rspcv 3067 . . . . . . . . . . . . . . 15  |-  ( n  e.  F  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  ->  ( n  C_  n  ->  n  C_  t )
) )
113108, 112mpii 43 . . . . . . . . . . . . . 14  |-  ( n  e.  F  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  ->  n  C_  t )
)
114113adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  n  e.  F )  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  ->  n  C_  t )
)
115 sstr2 3361 . . . . . . . . . . . . . . 15  |-  ( k 
C_  n  ->  (
n  C_  t  ->  k 
C_  t ) )
116115com12 31 . . . . . . . . . . . . . 14  |-  ( n 
C_  t  ->  (
k  C_  n  ->  k 
C_  t ) )
117116ralrimivw 2798 . . . . . . . . . . . . 13  |-  ( n 
C_  t  ->  A. k  e.  F  ( k  C_  n  ->  k  C_  t ) )
118114, 117impbid1 203 . . . . . . . . . . . 12  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  n  e.  F )  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  <->  n 
C_  t ) )
119107, 118bitr3d 255 . . . . . . . . . . 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 ) )
120119rexbidva 2730 . . . . . . . . . 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 ) )
121103, 120syl5bb 257 . . . . . . . . 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
) )
12232, 73, 1213bitrd 279 . . . . . . . 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 ) )
123122pm5.32da 641 . . . . . . 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
) ) )
124 filn0 19433 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  F  =/=  (/) )
12596snnz 3991 . . . . . . . . . . . . . . . 16  |-  { n }  =/=  (/)
126104, 125jctil 537 . . . . . . . . . . . . . . 15  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  ( { n }  =/=  (/) 
/\  n  =/=  (/) ) )
127 neanior 2695 . . . . . . . . . . . . . . 15  |-  ( ( { n }  =/=  (/) 
/\  n  =/=  (/) )  <->  -.  ( { n }  =  (/) 
\/  n  =  (/) ) )
128126, 127sylib 196 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  -.  ( { n }  =  (/) 
\/  n  =  (/) ) )
129 ss0b 3665 . . . . . . . . . . . . . . 15  |-  ( ( { n }  X.  n )  C_  (/)  <->  ( {
n }  X.  n
)  =  (/) )
130 xpeq0 5256 . . . . . . . . . . . . . . 15  |-  ( ( { n }  X.  n )  =  (/)  <->  ( { n }  =  (/) 
\/  n  =  (/) ) )
131129, 130bitri 249 . . . . . . . . . . . . . 14  |-  ( ( { n }  X.  n )  C_  (/)  <->  ( {
n }  =  (/)  \/  n  =  (/) ) )
132128, 131sylnibr 305 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  -.  ( { n }  X.  n )  C_  (/) )
133132ralrimiva 2797 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  A. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
134 r19.2z 3767 . . . . . . . . . . . 12  |-  ( ( F  =/=  (/)  /\  A. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )  ->  E. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
135124, 133, 134syl2anc 661 . . . . . . . . . . 11  |-  ( F  e.  ( Fil `  X
)  ->  E. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
136 rexnal 2724 . . . . . . . . . . 11  |-  ( E. n  e.  F  -.  ( { n }  X.  n )  C_  (/)  <->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
137135, 136sylib 196 . . . . . . . . . 10  |-  ( F  e.  ( Fil `  X
)  ->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
1381sseq1i 3378 . . . . . . . . . . . 12  |-  ( H 
C_  (/)  <->  U_ n  e.  F  ( { n }  X.  n )  C_  (/) )
139 ss0b 3665 . . . . . . . . . . . 12  |-  ( H 
C_  (/)  <->  H  =  (/) )
140 iunss 4209 . . . . . . . . . . . 12  |-  ( U_ n  e.  F  ( { n }  X.  n )  C_  (/)  <->  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
141138, 139, 1403bitr3i 275 . . . . . . . . . . 11  |-  ( H  =  (/)  <->  A. n  e.  F  ( { n }  X.  n )  C_  (/) )
142141necon3abii 2636 . . . . . . . . . 10  |-  ( H  =/=  (/)  <->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
143137, 142sylibr 212 . . . . . . . . 9  |-  ( F  e.  ( Fil `  X
)  ->  H  =/=  (/) )
144 dmresi 5159 . . . . . . . . . . . 12  |-  dom  (  _I  |`  H )  =  H
1451, 2filnetlem2 28597 . . . . . . . . . . . . . 14  |-  ( (  _I  |`  H )  C_  D  /\  D  C_  ( H  X.  H
) )
146145simpli 458 . . . . . . . . . . . . 13  |-  (  _I  |`  H )  C_  D
147 dmss 5037 . . . . . . . . . . . . 13  |-  ( (  _I  |`  H )  C_  D  ->  dom  (  _I  |`  H )  C_  dom  D )
148146, 147ax-mp 5 . . . . . . . . . . . 12  |-  dom  (  _I  |`  H )  C_  dom  D
149144, 148eqsstr3i 3385 . . . . . . . . . . 11  |-  H  C_  dom  D
150145simpri 462 . . . . . . . . . . . . 13  |-  D  C_  ( H  X.  H
)
151 dmss 5037 . . . . . . . . . . . . 13  |-  ( D 
C_  ( H  X.  H )  ->  dom  D 
C_  dom  ( H  X.  H ) )
152150, 151ax-mp 5 . . . . . . . . . . . 12  |-  dom  D  C_ 
dom  ( H  X.  H )
153 dmxpid 5057 . . . . . . . . . . . 12  |-  dom  ( H  X.  H )  =  H
154152, 153sseqtri 3386 . . . . . . . . . . 11  |-  dom  D  C_  H
155149, 154eqssi 3370 . . . . . . . . . 10  |-  H  =  dom  D
156155tailfb 28595 . . . . . . . . 9  |-  ( ( D  e.  DirRel  /\  H  =/=  (/) )  ->  ran  ( tail `  D )  e.  ( fBas `  H
) )
1575, 143, 156syl2anc 661 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  ran  ( tail `  D )  e.  (
fBas `  H )
)
158 elfm 19518 . . . . . . . 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 )
) )
15910, 157, 9, 158syl3anc 1218 . . . . . . 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 )
) )
160 filfbas 19419 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  F  e.  ( fBas `  X )
)
161 elfg 19442 . . . . . . . 8  |-  ( F  e.  ( fBas `  X
)  ->  ( t  e.  ( X filGen F )  <-> 
( t  C_  X  /\  E. n  e.  F  n  C_  t ) ) )
162160, 161syl 16 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  ( t  e.  ( X filGen F )  <-> 
( t  C_  X  /\  E. n  e.  F  n  C_  t ) ) )
163123, 159, 1623bitr4d 285 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  ( t  e.  ( ( X  FilMap  ( 2nd  |`  H )
) `  ran  ( tail `  D ) )  <->  t  e.  ( X filGen F ) ) )
164163eqrdv 2439 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) )  =  ( X filGen F ) )
165 fgfil 19446 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( X filGen F )  =  F )
166164, 165eqtr2d 2474 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  F  =  ( ( X  FilMap  ( 2nd  |`  H )
) `  ran  ( tail `  D ) ) )
16721, 166jca 532 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( ( 2nd  |`  H ) : dom  D --> X  /\  F  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) ) )
168 feq1 5540 . . . . 5  |-  ( f  =  ( 2nd  |`  H )  ->  ( f : dom  D --> X  <->  ( 2nd  |`  H ) : dom  D --> X ) )
169 oveq2 6097 . . . . . . 7  |-  ( f  =  ( 2nd  |`  H )  ->  ( X  FilMap  f )  =  ( X 
FilMap  ( 2nd  |`  H ) ) )
170169fveq1d 5691 . . . . . 6  |-  ( f  =  ( 2nd  |`  H )  ->  ( ( X 
FilMap  f ) `  ran  ( tail `  D )
)  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) )
171170eqeq2d 2452 . . . . 5  |-  ( f  =  ( 2nd  |`  H )  ->  ( F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) )  <-> 
F  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) ) )
172168, 171anbi12d 710 . . . 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 ) ) ) ) )
173172spcegv 3056 . . 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 ) ) ) ) )
17415, 167, 173sylc 60 . 2  |-  ( F  e.  ( Fil `  X
)  ->  E. f
( f : dom  D --> X  /\  F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) ) )
175 dmeq 5038 . . . . . 6  |-  ( d  =  D  ->  dom  d  =  dom  D )
176175feq2d 5545 . . . . 5  |-  ( d  =  D  ->  (
f : dom  d --> X 
<->  f : dom  D --> X ) )
177 fveq2 5689 . . . . . . . 8  |-  ( d  =  D  ->  ( tail `  d )  =  ( tail `  D
) )
178177rneqd 5065 . . . . . . 7  |-  ( d  =  D  ->  ran  ( tail `  d )  =  ran  ( tail `  D
) )
179178fveq2d 5693 . . . . . 6  |-  ( d  =  D  ->  (
( X  FilMap  f ) `
 ran  ( tail `  d ) )  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) )
180179eqeq2d 2452 . . . . 5  |-  ( d  =  D  ->  ( F  =  ( ( X  FilMap  f ) `  ran  ( tail `  d
) )  <->  F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) ) )
181176, 180anbi12d 710 . . . 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
) ) ) ) )
182181exbidv 1680 . . 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 ) ) ) ) )
183182rspcev 3071 . 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
) ) ) )
1845, 174, 183syl2anc 661 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756    =/= wne 2604   A.wral 2713   E.wrex 2714   _Vcvv 2970    C_ wss 3326   (/)c0 3635   ~Pcpw 3858   {csn 3875   <.cop 3881   U.cuni 4089   U_ciun 4169   class class class wbr 4290   {copab 4347    _I cid 4629    X. cxp 4836   dom cdm 4838   ran crn 4839    |` cres 4840   "cima 4841   Fun wfun 5410    Fn wfn 5411   -->wf 5412   -onto->wfo 5414   ` cfv 5416  (class class class)co 6089   1stc1st 6573   2ndc2nd 6574   DirRelcdir 15396   tailctail 15397   fBascfbas 17802   filGencfg 17803   Filcfil 19416    FilMap cfm 19504
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-rep 4401  ax-sep 4411  ax-nul 4419  ax-pow 4468  ax-pr 4529  ax-un 6370
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3185  df-csb 3287  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-nul 3636  df-if 3790  df-pw 3860  df-sn 3876  df-pr 3878  df-op 3882  df-uni 4090  df-iun 4171  df-br 4291  df-opab 4349  df-mpt 4350  df-id 4634  df-xp 4844  df-rel 4845  df-cnv 4846  df-co 4847  df-dm 4848  df-rn 4849  df-res 4850  df-ima 4851  df-iota 5379  df-fun 5418  df-fn 5419  df-f 5420  df-f1 5421  df-fo 5422  df-f1o 5423  df-fv 5424  df-ov 6092  df-oprab 6093  df-mpt2 6094  df-1st 6575  df-2nd 6576  df-dir 15398  df-tail 15399  df-fbas 17812  df-fg 17813  df-fil 19417  df-fm 19509
This theorem is referenced by:  filnet  28600
  Copyright terms: Public domain W3C validator