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

Theorem filnetlem4 30981
Description: Lemma for filnet 30982. (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 30980 . . . 4  |-  ( H  =  U. U. D  /\  ( F  e.  ( Fil `  X )  ->  ( H  C_  ( F  X.  X
)  /\  D  e.  DirRel ) ) )
43simpri 463 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( H  C_  ( F  X.  X
)  /\  D  e.  DirRel ) )
54simprd 464 . 2  |-  ( F  e.  ( Fil `  X
)  ->  D  e.  DirRel )
6 f2ndres 6769 . . . . 5  |-  ( 2nd  |`  ( F  X.  X
) ) : ( F  X.  X ) --> X
74simpld 460 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  H  C_  ( F  X.  X ) )
8 fssres2 5706 . . . . 5  |-  ( ( ( 2nd  |`  ( F  X.  X ) ) : ( F  X.  X ) --> X  /\  H  C_  ( F  X.  X ) )  -> 
( 2nd  |`  H ) : H --> X )
96, 7, 8sylancr 667 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H ) : H --> X )
10 filtop 20807 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  X  e.  F )
11 xpexg 6546 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  X  e.  F )  ->  ( F  X.  X )  e. 
_V )
1210, 11mpdan 672 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( F  X.  X )  e.  _V )
1312, 7ssexd 4509 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  H  e.  _V )
14 fex 6092 . . . 4  |-  ( ( ( 2nd  |`  H ) : H --> X  /\  H  e.  _V )  ->  ( 2nd  |`  H )  e.  _V )
159, 13, 14syl2anc 665 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H )  e.  _V )
16 dirdm 16418 . . . . . . . 8  |-  ( D  e.  DirRel  ->  dom  D  =  U. U. D )
175, 16syl 17 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  dom  D  = 
U. U. D )
183simpli 459 . . . . . . 7  |-  H  = 
U. U. D
1917, 18syl6reqr 2476 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  H  =  dom  D )
2019feq2d 5671 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( ( 2nd  |`  H ) : H --> X  <->  ( 2nd  |`  H ) : dom  D --> X ) )
219, 20mpbid 213 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H ) : dom  D --> X )
22 eqid 2423 . . . . . . . . . . . . . 14  |-  dom  D  =  dom  D
2322tailf 30975 . . . . . . . . . . . . 13  |-  ( D  e.  DirRel  ->  ( tail `  D
) : dom  D --> ~P dom  D )
245, 23syl 17 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  ( tail `  D ) : dom  D --> ~P dom  D )
2519feq2d 5671 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  ( ( tail `  D ) : H --> ~P dom  D  <->  (
tail `  D ) : dom  D --> ~P dom  D ) )
2624, 25mpbird 235 . . . . . . . . . . 11  |-  ( F  e.  ( Fil `  X
)  ->  ( tail `  D ) : H --> ~P dom  D )
2726adantr 466 . . . . . . . . . 10  |-  ( ( F  e.  ( Fil `  X )  /\  t  C_  X )  ->  ( tail `  D ) : H --> ~P dom  D
)
28 ffn 5684 . . . . . . . . . 10  |-  ( (
tail `  D ) : H --> ~P dom  D  ->  ( tail `  D
)  Fn  H )
29 imaeq2 5121 . . . . . . . . . . . 12  |-  ( d  =  ( ( tail `  D ) `  f
)  ->  ( ( 2nd  |`  H ) "
d )  =  ( ( 2nd  |`  H )
" ( ( tail `  D ) `  f
) ) )
3029sseq1d 3429 . . . . . . . . . . 11  |-  ( d  =  ( ( tail `  D ) `  f
)  ->  ( (
( 2nd  |`  H )
" d )  C_  t 
<->  ( ( 2nd  |`  H )
" ( ( tail `  D ) `  f
) )  C_  t
) )
3130rexrn 5978 . . . . . . . . . 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 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
) )
33 fo2nd 6767 . . . . . . . . . . . . . . 15  |-  2nd : _V -onto-> _V
34 fofn 5750 . . . . . . . . . . . . . . 15  |-  ( 2nd
: _V -onto-> _V  ->  2nd 
Fn  _V )
3533, 34ax-mp 5 . . . . . . . . . . . . . 14  |-  2nd  Fn  _V
36 ssv 3422 . . . . . . . . . . . . . 14  |-  H  C_  _V
37 fnssres 5645 . . . . . . . . . . . . . 14  |-  ( ( 2nd  Fn  _V  /\  H  C_  _V )  -> 
( 2nd  |`  H )  Fn  H )
3835, 36, 37mp2an 676 . . . . . . . . . . . . 13  |-  ( 2nd  |`  H )  Fn  H
39 fnfun 5629 . . . . . . . . . . . . 13  |-  ( ( 2nd  |`  H )  Fn  H  ->  Fun  ( 2nd  |`  H ) )
4038, 39ax-mp 5 . . . . . . . . . . . 12  |-  Fun  ( 2nd  |`  H )
4127ffvelrnda 5976 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  e.  ~P dom  D )
4241elpwid 3929 . . . . . . . . . . . . . 14  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  dom  D )
4319ad2antrr 730 . . . . . . . . . . . . . 14  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  H  =  dom  D )
4442, 43sseqtr4d 3439 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  H
)
45 fndm 5631 . . . . . . . . . . . . . 14  |-  ( ( 2nd  |`  H )  Fn  H  ->  dom  ( 2nd  |`  H )  =  H )
4638, 45ax-mp 5 . . . . . . . . . . . . 13  |-  dom  ( 2nd  |`  H )  =  H
4744, 46syl6sseqr 3449 . . . . . . . . . . . 12  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  dom  ( 2nd  |`  H )
)
48 funimass4 5871 . . . . . . . . . . . 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 667 . . . . . . . . . . 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 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  D  e.  DirRel )
51 simpr 462 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  f  e.  H )
5251, 43eleqtrd 2503 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  f  e.  dom  D )
53 vex 3020 . . . . . . . . . . . . . . . . 17  |-  d  e. 
_V
5453a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  d  e.  _V )
5522eltail 30974 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  DirRel  /\  f  e.  dom  D  /\  d  e.  _V )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  f D
d ) )
5650, 52, 54, 55syl3anc 1264 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  f D
d ) )
5751biantrurd 510 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
d  e.  H  <->  ( f  e.  H  /\  d  e.  H ) ) )
5857anbi1d 709 . . . . . . . . . . . . . . . 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 3020 . . . . . . . . . . . . . . . . 17  |-  f  e. 
_V
601, 2, 59, 53filnetlem1 30978 . . . . . . . . . . . . . . . 16  |-  ( f D d  <->  ( (
f  e.  H  /\  d  e.  H )  /\  ( 1st `  d
)  C_  ( 1st `  f ) ) )
6158, 60syl6bbr 266 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( d  e.  H  /\  ( 1st `  d
)  C_  ( 1st `  f ) )  <->  f D
d ) )
6256, 61bitr4d 259 . . . . . . . . . . . . . 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 318 . . . . . . . . . . . . 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 5834 . . . . . . . . . . . . . . . . 17  |-  ( d  e.  H  ->  (
( 2nd  |`  H ) `
 d )  =  ( 2nd `  d
) )
6564eleq1d 2485 . . . . . . . . . . . . . . . 16  |-  ( d  e.  H  ->  (
( ( 2nd  |`  H ) `
 d )  e.  t  <->  ( 2nd `  d
)  e.  t ) )
6665adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( d  e.  H  /\  ( 1st `  d ) 
C_  ( 1st `  f
) )  ->  (
( ( 2nd  |`  H ) `
 d )  e.  t  <->  ( 2nd `  d
)  e.  t ) )
6766pm5.74i 248 . . . . . . . . . . . . . 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 447 . . . . . . . . . . . . . 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 252 . . . . . . . . . . . . 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 264 . . . . . . . . . . . 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 2795 . . . . . . . . . . 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 256 . . . . . . . . . 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 2870 . . . . . . . . 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 3020 . . . . . . . . . . . . . . . . 17  |-  k  e. 
_V
75 vex 3020 . . . . . . . . . . . . . . . . 17  |-  v  e. 
_V
7674, 75op1std 6756 . . . . . . . . . . . . . . . 16  |-  ( d  =  <. k ,  v
>.  ->  ( 1st `  d
)  =  k )
7776sseq1d 3429 . . . . . . . . . . . . . . 15  |-  ( d  =  <. k ,  v
>.  ->  ( ( 1st `  d )  C_  ( 1st `  f )  <->  k  C_  ( 1st `  f ) ) )
7874, 75op2ndd 6757 . . . . . . . . . . . . . . . 16  |-  ( d  =  <. k ,  v
>.  ->  ( 2nd `  d
)  =  v )
7978eleq1d 2485 . . . . . . . . . . . . . . 15  |-  ( d  =  <. k ,  v
>.  ->  ( ( 2nd `  d )  e.  t  <-> 
v  e.  t ) )
8077, 79imbi12d 321 . . . . . . . . . . . . . 14  |-  ( d  =  <. k ,  v
>.  ->  ( ( ( 1st `  d ) 
C_  ( 1st `  f
)  ->  ( 2nd `  d )  e.  t )  <->  ( k  C_  ( 1st `  f )  ->  v  e.  t ) ) )
8180raliunxp 4931 . . . . . . . . . . . . 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 3946 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  { n }  =  { k } )
83 id 22 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  n  =  k )
8482, 83xpeq12d 4816 . . . . . . . . . . . . . . . 16  |-  ( n  =  k  ->  ( { n }  X.  n )  =  ( { k }  X.  k ) )
8584cbviunv 4276 . . . . . . . . . . . . . . 15  |-  U_ n  e.  F  ( {
n }  X.  n
)  =  U_ k  e.  F  ( {
k }  X.  k
)
861, 85eqtri 2445 . . . . . . . . . . . . . 14  |-  H  = 
U_ k  e.  F  ( { k }  X.  k )
8786raleqi 2963 . . . . . . . . . . . . 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 3392 . . . . . . . . . . . . . . . 16  |-  ( k 
C_  t  <->  A. v  e.  k  v  e.  t )
8988imbi2i 313 . . . . . . . . . . . . . . 15  |-  ( ( k  C_  ( 1st `  f )  ->  k  C_  t )  <->  ( k  C_  ( 1st `  f
)  ->  A. v  e.  k  v  e.  t ) )
90 r19.21v 2765 . . . . . . . . . . . . . . 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 255 . . . . . . . . . . . . . 14  |-  ( ( k  C_  ( 1st `  f )  ->  k  C_  t )  <->  A. v  e.  k  ( k  C_  ( 1st `  f
)  ->  v  e.  t ) )
9291ralbii 2791 . . . . . . . . . . . . 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 280 . . . . . . . . . . . 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 2861 . . . . . . . . . . 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 2964 . . . . . . . . . . 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 3020 . . . . . . . . . . . . . . . 16  |-  n  e. 
_V
97 vex 3020 . . . . . . . . . . . . . . . 16  |-  m  e. 
_V
9896, 97op1std 6756 . . . . . . . . . . . . . . 15  |-  ( f  =  <. n ,  m >.  ->  ( 1st `  f
)  =  n )
9998sseq2d 3430 . . . . . . . . . . . . . 14  |-  ( f  =  <. n ,  m >.  ->  ( k  C_  ( 1st `  f )  <-> 
k  C_  n )
)
10099imbi1d 318 . . . . . . . . . . . . 13  |-  ( f  =  <. n ,  m >.  ->  ( ( k 
C_  ( 1st `  f
)  ->  k  C_  t )  <->  ( k  C_  n  ->  k  C_  t ) ) )
101100ralbidv 2799 . . . . . . . . . . . 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 4932 . . . . . . . . . . 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 274 . . . . . . . . . 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 20802 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  n  =/=  (/) )
105104adantlr 719 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  n  e.  F )  ->  n  =/=  (/) )
106 r19.9rzv 3831 . . . . . . . . . . . . 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 17 . . . . . . . . . . . 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 3421 . . . . . . . . . . . . . . 15  |-  n  C_  n
109 sseq1 3423 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  (
k  C_  n  <->  n  C_  n
) )
110 sseq1 3423 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  (
k  C_  t  <->  n  C_  t
) )
111109, 110imbi12d 321 . . . . . . . . . . . . . . . 16  |-  ( k  =  n  ->  (
( k  C_  n  ->  k  C_  t )  <->  ( n  C_  n  ->  n 
C_  t ) ) )
112111rspcv 3116 . . . . . . . . . . . . . . 15  |-  ( n  e.  F  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  ->  ( n  C_  n  ->  n  C_  t )
) )
113108, 112mpii 44 . . . . . . . . . . . . . 14  |-  ( n  e.  F  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  ->  n  C_  t )
)
114113adantl 467 . . . . . . . . . . . . 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 3409 . . . . . . . . . . . . . . 15  |-  ( k 
C_  n  ->  (
n  C_  t  ->  k 
C_  t ) )
116115com12 32 . . . . . . . . . . . . . 14  |-  ( n 
C_  t  ->  (
k  C_  n  ->  k 
C_  t ) )
117116ralrimivw 2775 . . . . . . . . . . . . 13  |-  ( n 
C_  t  ->  A. k  e.  F  ( k  C_  n  ->  k  C_  t ) )
118114, 117impbid1 206 . . . . . . . . . . . 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 258 . . . . . . . . . . 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 2870 . . . . . . . . . 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 260 . . . . . . . . 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 282 . . . . . . . 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 645 . . . . . . 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 20814 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  F  =/=  (/) )
12596snnz 4056 . . . . . . . . . . . . . . . 16  |-  { n }  =/=  (/)
126104, 125jctil 539 . . . . . . . . . . . . . . 15  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  ( { n }  =/=  (/) 
/\  n  =/=  (/) ) )
127 neanior 2688 . . . . . . . . . . . . . . 15  |-  ( ( { n }  =/=  (/) 
/\  n  =/=  (/) )  <->  -.  ( { n }  =  (/) 
\/  n  =  (/) ) )
128126, 127sylib 199 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  -.  ( { n }  =  (/) 
\/  n  =  (/) ) )
129 ss0b 3732 . . . . . . . . . . . . . . 15  |-  ( ( { n }  X.  n )  C_  (/)  <->  ( {
n }  X.  n
)  =  (/) )
130 xpeq0 5214 . . . . . . . . . . . . . . 15  |-  ( ( { n }  X.  n )  =  (/)  <->  ( { n }  =  (/) 
\/  n  =  (/) ) )
131129, 130bitri 252 . . . . . . . . . . . . . 14  |-  ( ( { n }  X.  n )  C_  (/)  <->  ( {
n }  =  (/)  \/  n  =  (/) ) )
132128, 131sylnibr 306 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  -.  ( { n }  X.  n )  C_  (/) )
133132ralrimiva 2774 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  A. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
134 r19.2z 3826 . . . . . . . . . . . 12  |-  ( ( F  =/=  (/)  /\  A. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )  ->  E. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
135124, 133, 134syl2anc 665 . . . . . . . . . . 11  |-  ( F  e.  ( Fil `  X
)  ->  E. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
136 rexnal 2808 . . . . . . . . . . 11  |-  ( E. n  e.  F  -.  ( { n }  X.  n )  C_  (/)  <->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
137135, 136sylib 199 . . . . . . . . . 10  |-  ( F  e.  ( Fil `  X
)  ->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
1381sseq1i 3426 . . . . . . . . . . . 12  |-  ( H 
C_  (/)  <->  U_ n  e.  F  ( { n }  X.  n )  C_  (/) )
139 ss0b 3732 . . . . . . . . . . . 12  |-  ( H 
C_  (/)  <->  H  =  (/) )
140 iunss 4278 . . . . . . . . . . . 12  |-  ( U_ n  e.  F  ( { n }  X.  n )  C_  (/)  <->  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
141138, 139, 1403bitr3i 278 . . . . . . . . . . 11  |-  ( H  =  (/)  <->  A. n  e.  F  ( { n }  X.  n )  C_  (/) )
142141necon3abii 2642 . . . . . . . . . 10  |-  ( H  =/=  (/)  <->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
143137, 142sylibr 215 . . . . . . . . 9  |-  ( F  e.  ( Fil `  X
)  ->  H  =/=  (/) )
144 dmresi 5117 . . . . . . . . . . . 12  |-  dom  (  _I  |`  H )  =  H
1451, 2filnetlem2 30979 . . . . . . . . . . . . . 14  |-  ( (  _I  |`  H )  C_  D  /\  D  C_  ( H  X.  H
) )
146145simpli 459 . . . . . . . . . . . . 13  |-  (  _I  |`  H )  C_  D
147 dmss 4991 . . . . . . . . . . . . 13  |-  ( (  _I  |`  H )  C_  D  ->  dom  (  _I  |`  H )  C_  dom  D )
148146, 147ax-mp 5 . . . . . . . . . . . 12  |-  dom  (  _I  |`  H )  C_  dom  D
149144, 148eqsstr3i 3433 . . . . . . . . . . 11  |-  H  C_  dom  D
150145simpri 463 . . . . . . . . . . . . 13  |-  D  C_  ( H  X.  H
)
151 dmss 4991 . . . . . . . . . . . . 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 5011 . . . . . . . . . . . 12  |-  dom  ( H  X.  H )  =  H
154152, 153sseqtri 3434 . . . . . . . . . . 11  |-  dom  D  C_  H
155149, 154eqssi 3418 . . . . . . . . . 10  |-  H  =  dom  D
156155tailfb 30977 . . . . . . . . 9  |-  ( ( D  e.  DirRel  /\  H  =/=  (/) )  ->  ran  ( tail `  D )  e.  ( fBas `  H
) )
1575, 143, 156syl2anc 665 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  ran  ( tail `  D )  e.  (
fBas `  H )
)
158 elfm 20899 . . . . . . . 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 1264 . . . . . . 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 20800 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  F  e.  ( fBas `  X )
)
161 elfg 20823 . . . . . . . 8  |-  ( F  e.  ( fBas `  X
)  ->  ( t  e.  ( X filGen F )  <-> 
( t  C_  X  /\  E. n  e.  F  n  C_  t ) ) )
162160, 161syl 17 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  ( t  e.  ( X filGen F )  <-> 
( t  C_  X  /\  E. n  e.  F  n  C_  t ) ) )
163123, 159, 1623bitr4d 288 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  ( t  e.  ( ( X  FilMap  ( 2nd  |`  H )
) `  ran  ( tail `  D ) )  <->  t  e.  ( X filGen F ) ) )
164163eqrdv 2421 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) )  =  ( X filGen F ) )
165 fgfil 20827 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( X filGen F )  =  F )
166164, 165eqtr2d 2458 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  F  =  ( ( X  FilMap  ( 2nd  |`  H )
) `  ran  ( tail `  D ) ) )
16721, 166jca 534 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( ( 2nd  |`  H ) : dom  D --> X  /\  F  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) ) )
168 feq1 5666 . . . . 5  |-  ( f  =  ( 2nd  |`  H )  ->  ( f : dom  D --> X  <->  ( 2nd  |`  H ) : dom  D --> X ) )
169 oveq2 6252 . . . . . . 7  |-  ( f  =  ( 2nd  |`  H )  ->  ( X  FilMap  f )  =  ( X 
FilMap  ( 2nd  |`  H ) ) )
170169fveq1d 5822 . . . . . 6  |-  ( f  =  ( 2nd  |`  H )  ->  ( ( X 
FilMap  f ) `  ran  ( tail `  D )
)  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) )
171170eqeq2d 2433 . . . . 5  |-  ( f  =  ( 2nd  |`  H )  ->  ( F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) )  <-> 
F  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) ) )
172168, 171anbi12d 715 . . . 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 3105 . . 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 62 . 2  |-  ( F  e.  ( Fil `  X
)  ->  E. f
( f : dom  D --> X  /\  F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) ) )
175 dmeq 4992 . . . . . 6  |-  ( d  =  D  ->  dom  d  =  dom  D )
176175feq2d 5671 . . . . 5  |-  ( d  =  D  ->  (
f : dom  d --> X 
<->  f : dom  D --> X ) )
177 fveq2 5820 . . . . . . . 8  |-  ( d  =  D  ->  ( tail `  d )  =  ( tail `  D
) )
178177rneqd 5019 . . . . . . 7  |-  ( d  =  D  ->  ran  ( tail `  d )  =  ran  ( tail `  D
) )
179178fveq2d 5824 . . . . . 6  |-  ( d  =  D  ->  (
( X  FilMap  f ) `
 ran  ( tail `  d ) )  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) )
180179eqeq2d 2433 . . . . 5  |-  ( d  =  D  ->  ( F  =  ( ( X  FilMap  f ) `  ran  ( tail `  d
) )  <->  F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) ) )
181176, 180anbi12d 715 . . . 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 1762 . . 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 3120 . 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 665 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 187    \/ wo 369    /\ wa 370    = wceq 1437   E.wex 1657    e. wcel 1872    =/= wne 2594   A.wral 2709   E.wrex 2710   _Vcvv 3017    C_ wss 3374   (/)c0 3699   ~Pcpw 3919   {csn 3936   <.cop 3942   U.cuni 4157   U_ciun 4237   class class class wbr 4361   {copab 4419    _I cid 4701    X. cxp 4789   dom cdm 4791   ran crn 4792    |` cres 4793   "cima 4794   Fun wfun 5533    Fn wfn 5534   -->wf 5535   -onto->wfo 5537   ` cfv 5539  (class class class)co 6244   1stc1st 6744   2ndc2nd 6745   DirRelcdir 16412   tailctail 16413   fBascfbas 18896   filGencfg 18897   Filcfil 20797    FilMap cfm 20885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-rep 4474  ax-sep 4484  ax-nul 4493  ax-pow 4540  ax-pr 4598  ax-un 6536
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-mo 2276  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-nel 2597  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 3019  df-sbc 3238  df-csb 3334  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-uni 4158  df-iun 4239  df-br 4362  df-opab 4421  df-mpt 4422  df-id 4706  df-xp 4797  df-rel 4798  df-cnv 4799  df-co 4800  df-dm 4801  df-rn 4802  df-res 4803  df-ima 4804  df-iota 5503  df-fun 5541  df-fn 5542  df-f 5543  df-f1 5544  df-fo 5545  df-f1o 5546  df-fv 5547  df-ov 6247  df-oprab 6248  df-mpt2 6249  df-1st 6746  df-2nd 6747  df-dir 16414  df-tail 16415  df-fbas 18905  df-fg 18906  df-fil 20798  df-fm 20890
This theorem is referenced by:  filnet  30982
  Copyright terms: Public domain W3C validator