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

Theorem filnetlem4 29789
Description: Lemma for filnet 29790. (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 29788 . . . 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 6797 . . . . 5  |-  ( 2nd  |`  ( F  X.  X
) ) : ( F  X.  X ) --> X
74simpld 459 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  H  C_  ( F  X.  X ) )
8 fssres2 5744 . . . . 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 20084 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  X  e.  F )
11 xpexg 6702 . . . . . 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 4587 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  H  e.  _V )
14 fex 6124 . . . 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 15710 . . . . . . . 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 2520 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  H  =  dom  D )
2019feq2d 5709 . . . . 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 2460 . . . . . . . . . . . . . 14  |-  dom  D  =  dom  D
2322tailf 29783 . . . . . . . . . . . . 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 5709 . . . . . . . . . . . 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 5722 . . . . . . . . . 10  |-  ( (
tail `  D ) : H --> ~P dom  D  ->  ( tail `  D
)  Fn  H )
29 imaeq2 5324 . . . . . . . . . . . 12  |-  ( d  =  ( ( tail `  D ) `  f
)  ->  ( ( 2nd  |`  H ) "
d )  =  ( ( 2nd  |`  H )
" ( ( tail `  D ) `  f
) ) )
3029sseq1d 3524 . . . . . . . . . . 11  |-  ( d  =  ( ( tail `  D ) `  f
)  ->  ( (
( 2nd  |`  H )
" d )  C_  t 
<->  ( ( 2nd  |`  H )
" ( ( tail `  D ) `  f
) )  C_  t
) )
3130rexrn 6014 . . . . . . . . . 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 6795 . . . . . . . . . . . . . . 15  |-  2nd : _V -onto-> _V
34 fofn 5788 . . . . . . . . . . . . . . 15  |-  ( 2nd
: _V -onto-> _V  ->  2nd 
Fn  _V )
3533, 34ax-mp 5 . . . . . . . . . . . . . 14  |-  2nd  Fn  _V
36 ssv 3517 . . . . . . . . . . . . . 14  |-  H  C_  _V
37 fnssres 5685 . . . . . . . . . . . . . 14  |-  ( ( 2nd  Fn  _V  /\  H  C_  _V )  -> 
( 2nd  |`  H )  Fn  H )
3835, 36, 37mp2an 672 . . . . . . . . . . . . 13  |-  ( 2nd  |`  H )  Fn  H
39 fnfun 5669 . . . . . . . . . . . . 13  |-  ( ( 2nd  |`  H )  Fn  H  ->  Fun  ( 2nd  |`  H ) )
4038, 39ax-mp 5 . . . . . . . . . . . 12  |-  Fun  ( 2nd  |`  H )
4127ffvelrnda 6012 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  e.  ~P dom  D )
4241elpwid 4013 . . . . . . . . . . . . . 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 3534 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  H
)
45 fndm 5671 . . . . . . . . . . . . . 14  |-  ( ( 2nd  |`  H )  Fn  H  ->  dom  ( 2nd  |`  H )  =  H )
4638, 45ax-mp 5 . . . . . . . . . . . . 13  |-  dom  ( 2nd  |`  H )  =  H
4744, 46syl6sseqr 3544 . . . . . . . . . . . 12  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  dom  ( 2nd  |`  H )
)
48 funimass4 5909 . . . . . . . . . . . 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 2550 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  f  e.  dom  D )
53 vex 3109 . . . . . . . . . . . . . . . . 17  |-  d  e. 
_V
5453a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  d  e.  _V )
5522eltail 29782 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  DirRel  /\  f  e.  dom  D  /\  d  e.  _V )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  f D
d ) )
5650, 52, 54, 55syl3anc 1223 . . . . . . . . . . . . . . 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 3109 . . . . . . . . . . . . . . . . 17  |-  f  e. 
_V
601, 2, 59, 53filnetlem1 29786 . . . . . . . . . . . . . . . 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 5871 . . . . . . . . . . . . . . . . 17  |-  ( d  e.  H  ->  (
( 2nd  |`  H ) `
 d )  =  ( 2nd `  d
) )
6564eleq1d 2529 . . . . . . . . . . . . . . . 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 2892 . . . . . . . . . . 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 2963 . . . . . . . . 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 3109 . . . . . . . . . . . . . . . . 17  |-  k  e. 
_V
75 vex 3109 . . . . . . . . . . . . . . . . 17  |-  v  e. 
_V
7674, 75op1std 6784 . . . . . . . . . . . . . . . 16  |-  ( d  =  <. k ,  v
>.  ->  ( 1st `  d
)  =  k )
7776sseq1d 3524 . . . . . . . . . . . . . . 15  |-  ( d  =  <. k ,  v
>.  ->  ( ( 1st `  d )  C_  ( 1st `  f )  <->  k  C_  ( 1st `  f ) ) )
7874, 75op2ndd 6785 . . . . . . . . . . . . . . . 16  |-  ( d  =  <. k ,  v
>.  ->  ( 2nd `  d
)  =  v )
7978eleq1d 2529 . . . . . . . . . . . . . . 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 5133 . . . . . . . . . . . . 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 4030 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  { n }  =  { k } )
83 id 22 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  n  =  k )
8482, 83xpeq12d 5017 . . . . . . . . . . . . . . . 16  |-  ( n  =  k  ->  ( { n }  X.  n )  =  ( { k }  X.  k ) )
8584cbviunv 4357 . . . . . . . . . . . . . . 15  |-  U_ n  e.  F  ( {
n }  X.  n
)  =  U_ k  e.  F  ( {
k }  X.  k
)
861, 85eqtri 2489 . . . . . . . . . . . . . 14  |-  H  = 
U_ k  e.  F  ( { k }  X.  k )
8786raleqi 3055 . . . . . . . . . . . . 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 3487 . . . . . . . . . . . . . . . 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 2862 . . . . . . . . . . . . . . 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 2888 . . . . . . . . . . . . 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 2958 . . . . . . . . . . 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 3056 . . . . . . . . . . 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 3109 . . . . . . . . . . . . . . . 16  |-  n  e. 
_V
97 vex 3109 . . . . . . . . . . . . . . . 16  |-  m  e. 
_V
9896, 97op1std 6784 . . . . . . . . . . . . . . 15  |-  ( f  =  <. n ,  m >.  ->  ( 1st `  f
)  =  n )
9998sseq2d 3525 . . . . . . . . . . . . . 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 2896 . . . . . . . . . . . 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 5134 . . . . . . . . . . 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 20079 . . . . . . . . . . . . . 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 3915 . . . . . . . . . . . . 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 3516 . . . . . . . . . . . . . . 15  |-  n  C_  n
109 sseq1 3518 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  (
k  C_  n  <->  n  C_  n
) )
110 sseq1 3518 . . . . . . . . . . . . . . . . 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 3203 . . . . . . . . . . . . . . 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 3504 . . . . . . . . . . . . . . 15  |-  ( k 
C_  n  ->  (
n  C_  t  ->  k 
C_  t ) )
116115com12 31 . . . . . . . . . . . . . 14  |-  ( n 
C_  t  ->  (
k  C_  n  ->  k 
C_  t ) )
117116ralrimivw 2872 . . . . . . . . . . . . 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 2963 . . . . . . . . . 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 20091 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  F  =/=  (/) )
12596snnz 4138 . . . . . . . . . . . . . . . 16  |-  { n }  =/=  (/)
126104, 125jctil 537 . . . . . . . . . . . . . . 15  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  ( { n }  =/=  (/) 
/\  n  =/=  (/) ) )
127 neanior 2785 . . . . . . . . . . . . . . 15  |-  ( ( { n }  =/=  (/) 
/\  n  =/=  (/) )  <->  -.  ( { n }  =  (/) 
\/  n  =  (/) ) )
128126, 127sylib 196 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  -.  ( { n }  =  (/) 
\/  n  =  (/) ) )
129 ss0b 3808 . . . . . . . . . . . . . . 15  |-  ( ( { n }  X.  n )  C_  (/)  <->  ( {
n }  X.  n
)  =  (/) )
130 xpeq0 5418 . . . . . . . . . . . . . . 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 2871 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  A. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
134 r19.2z 3910 . . . . . . . . . . . 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 2905 . . . . . . . . . . 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 3521 . . . . . . . . . . . 12  |-  ( H 
C_  (/)  <->  U_ n  e.  F  ( { n }  X.  n )  C_  (/) )
139 ss0b 3808 . . . . . . . . . . . 12  |-  ( H 
C_  (/)  <->  H  =  (/) )
140 iunss 4359 . . . . . . . . . . . 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 2720 . . . . . . . . . 10  |-  ( H  =/=  (/)  <->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
143137, 142sylibr 212 . . . . . . . . 9  |-  ( F  e.  ( Fil `  X
)  ->  H  =/=  (/) )
144 dmresi 5320 . . . . . . . . . . . 12  |-  dom  (  _I  |`  H )  =  H
1451, 2filnetlem2 29787 . . . . . . . . . . . . . 14  |-  ( (  _I  |`  H )  C_  D  /\  D  C_  ( H  X.  H
) )
146145simpli 458 . . . . . . . . . . . . 13  |-  (  _I  |`  H )  C_  D
147 dmss 5193 . . . . . . . . . . . . 13  |-  ( (  _I  |`  H )  C_  D  ->  dom  (  _I  |`  H )  C_  dom  D )
148146, 147ax-mp 5 . . . . . . . . . . . 12  |-  dom  (  _I  |`  H )  C_  dom  D
149144, 148eqsstr3i 3528 . . . . . . . . . . 11  |-  H  C_  dom  D
150145simpri 462 . . . . . . . . . . . . 13  |-  D  C_  ( H  X.  H
)
151 dmss 5193 . . . . . . . . . . . . 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 5213 . . . . . . . . . . . 12  |-  dom  ( H  X.  H )  =  H
154152, 153sseqtri 3529 . . . . . . . . . . 11  |-  dom  D  C_  H
155149, 154eqssi 3513 . . . . . . . . . 10  |-  H  =  dom  D
156155tailfb 29785 . . . . . . . . 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 20176 . . . . . . . 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 1223 . . . . . . 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 20077 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  F  e.  ( fBas `  X )
)
161 elfg 20100 . . . . . . . 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 2457 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) )  =  ( X filGen F ) )
165 fgfil 20104 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( X filGen F )  =  F )
166164, 165eqtr2d 2502 . . . 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 5704 . . . . 5  |-  ( f  =  ( 2nd  |`  H )  ->  ( f : dom  D --> X  <->  ( 2nd  |`  H ) : dom  D --> X ) )
169 oveq2 6283 . . . . . . 7  |-  ( f  =  ( 2nd  |`  H )  ->  ( X  FilMap  f )  =  ( X 
FilMap  ( 2nd  |`  H ) ) )
170169fveq1d 5859 . . . . . 6  |-  ( f  =  ( 2nd  |`  H )  ->  ( ( X 
FilMap  f ) `  ran  ( tail `  D )
)  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) )
171170eqeq2d 2474 . . . . 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 3192 . . 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 5194 . . . . . 6  |-  ( d  =  D  ->  dom  d  =  dom  D )
176175feq2d 5709 . . . . 5  |-  ( d  =  D  ->  (
f : dom  d --> X 
<->  f : dom  D --> X ) )
177 fveq2 5857 . . . . . . . 8  |-  ( d  =  D  ->  ( tail `  d )  =  ( tail `  D
) )
178177rneqd 5221 . . . . . . 7  |-  ( d  =  D  ->  ran  ( tail `  d )  =  ran  ( tail `  D
) )
179178fveq2d 5861 . . . . . 6  |-  ( d  =  D  ->  (
( X  FilMap  f ) `
 ran  ( tail `  d ) )  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) )
180179eqeq2d 2474 . . . . 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 1685 . . 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 3207 . 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 1374   E.wex 1591    e. wcel 1762    =/= wne 2655   A.wral 2807   E.wrex 2808   _Vcvv 3106    C_ wss 3469   (/)c0 3778   ~Pcpw 4003   {csn 4020   <.cop 4026   U.cuni 4238   U_ciun 4318   class class class wbr 4440   {copab 4497    _I cid 4783    X. cxp 4990   dom cdm 4992   ran crn 4993    |` cres 4994   "cima 4995   Fun wfun 5573    Fn wfn 5574   -->wf 5575   -onto->wfo 5577   ` cfv 5579  (class class class)co 6275   1stc1st 6772   2ndc2nd 6773   DirRelcdir 15704   tailctail 15705   fBascfbas 18170   filGencfg 18171   Filcfil 20074    FilMap cfm 20162
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-1st 6774  df-2nd 6775  df-dir 15706  df-tail 15707  df-fbas 18180  df-fg 18181  df-fil 20075  df-fm 20167
This theorem is referenced by:  filnet  29790
  Copyright terms: Public domain W3C validator