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

Theorem filnetlem4 26411
Description: Lemma for filnet 26412. (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 26410 . . . 4  |-  ( H  =  U. U. D  /\  ( F  e.  ( Fil `  X )  ->  ( H  C_  ( F  X.  X
)  /\  D  e.  DirRel ) ) )
43simpri 450 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( H  C_  ( F  X.  X
)  /\  D  e.  DirRel ) )
54simprd 451 . 2  |-  ( F  e.  ( Fil `  X
)  ->  D  e.  DirRel )
6 f2ndres 6370 . . . . 5  |-  ( 2nd  |`  ( F  X.  X
) ) : ( F  X.  X ) --> X
74simpld 447 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  H  C_  ( F  X.  X ) )
8 fssres2 5612 . . . . 5  |-  ( ( ( 2nd  |`  ( F  X.  X ) ) : ( F  X.  X ) --> X  /\  H  C_  ( F  X.  X ) )  -> 
( 2nd  |`  H ) : H --> X )
96, 7, 8sylancr 646 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H ) : H --> X )
10 filtop 17888 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  X  e.  F )
11 xpexg 4990 . . . . . 6  |-  ( ( F  e.  ( Fil `  X )  /\  X  e.  F )  ->  ( F  X.  X )  e. 
_V )
1210, 11mpdan 651 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( F  X.  X )  e.  _V )
1312, 7ssexd 4351 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  H  e.  _V )
14 fex 5970 . . . 4  |-  ( ( ( 2nd  |`  H ) : H --> X  /\  H  e.  _V )  ->  ( 2nd  |`  H )  e.  _V )
159, 13, 14syl2anc 644 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H )  e.  _V )
16 dirdm 14680 . . . . . . . 8  |-  ( D  e.  DirRel  ->  dom  D  =  U. U. D )
175, 16syl 16 . . . . . . 7  |-  ( F  e.  ( Fil `  X
)  ->  dom  D  = 
U. U. D )
183simpli 446 . . . . . . 7  |-  H  = 
U. U. D
1917, 18syl6reqr 2488 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  H  =  dom  D )
2019feq2d 5582 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( ( 2nd  |`  H ) : H --> X  <->  ( 2nd  |`  H ) : dom  D --> X ) )
219, 20mpbid 203 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  ( 2nd  |`  H ) : dom  D --> X )
22 eqid 2437 . . . . . . . . . . . . . 14  |-  dom  D  =  dom  D
2322tailf 26405 . . . . . . . . . . . . 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 5582 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  ( ( tail `  D ) : H --> ~P dom  D  <->  (
tail `  D ) : dom  D --> ~P dom  D ) )
2624, 25mpbird 225 . . . . . . . . . . 11  |-  ( F  e.  ( Fil `  X
)  ->  ( tail `  D ) : H --> ~P dom  D )
2726adantr 453 . . . . . . . . . 10  |-  ( ( F  e.  ( Fil `  X )  /\  t  C_  X )  ->  ( tail `  D ) : H --> ~P dom  D
)
28 ffn 5592 . . . . . . . . . 10  |-  ( (
tail `  D ) : H --> ~P dom  D  ->  ( tail `  D
)  Fn  H )
29 imaeq2 5200 . . . . . . . . . . . 12  |-  ( d  =  ( ( tail `  D ) `  f
)  ->  ( ( 2nd  |`  H ) "
d )  =  ( ( 2nd  |`  H )
" ( ( tail `  D ) `  f
) ) )
3029sseq1d 3376 . . . . . . . . . . 11  |-  ( d  =  ( ( tail `  D ) `  f
)  ->  ( (
( 2nd  |`  H )
" d )  C_  t 
<->  ( ( 2nd  |`  H )
" ( ( tail `  D ) `  f
) )  C_  t
) )
3130rexrn 5873 . . . . . . . . . 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 19 . . . . . . . . 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 6368 . . . . . . . . . . . . . . 15  |-  2nd : _V -onto-> _V
34 fofn 5656 . . . . . . . . . . . . . . 15  |-  ( 2nd
: _V -onto-> _V  ->  2nd 
Fn  _V )
3533, 34ax-mp 8 . . . . . . . . . . . . . 14  |-  2nd  Fn  _V
36 ssv 3369 . . . . . . . . . . . . . 14  |-  H  C_  _V
37 fnssres 5559 . . . . . . . . . . . . . 14  |-  ( ( 2nd  Fn  _V  /\  H  C_  _V )  -> 
( 2nd  |`  H )  Fn  H )
3835, 36, 37mp2an 655 . . . . . . . . . . . . 13  |-  ( 2nd  |`  H )  Fn  H
39 fnfun 5543 . . . . . . . . . . . . 13  |-  ( ( 2nd  |`  H )  Fn  H  ->  Fun  ( 2nd  |`  H ) )
4038, 39ax-mp 8 . . . . . . . . . . . 12  |-  Fun  ( 2nd  |`  H )
4127ffvelrnda 5871 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  e.  ~P dom  D )
4241elpwid 3809 . . . . . . . . . . . . . 14  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  dom  D )
4319ad2antrr 708 . . . . . . . . . . . . . 14  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  H  =  dom  D )
4442, 43sseqtr4d 3386 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  H
)
45 fndm 5545 . . . . . . . . . . . . . 14  |-  ( ( 2nd  |`  H )  Fn  H  ->  dom  ( 2nd  |`  H )  =  H )
4638, 45ax-mp 8 . . . . . . . . . . . . 13  |-  dom  ( 2nd  |`  H )  =  H
4744, 46syl6sseqr 3396 . . . . . . . . . . . 12  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( tail `  D ) `  f )  C_  dom  ( 2nd  |`  H )
)
48 funimass4 5778 . . . . . . . . . . . 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 646 . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  D  e.  DirRel )
51 simpr 449 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  f  e.  H )
5251, 43eleqtrd 2513 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  f  e.  dom  D )
53 vex 2960 . . . . . . . . . . . . . . . . 17  |-  d  e. 
_V
5453a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  d  e.  _V )
5522eltail 26404 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  DirRel  /\  f  e.  dom  D  /\  d  e.  _V )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  f D
d ) )
5650, 52, 54, 55syl3anc 1185 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
d  e.  ( (
tail `  D ) `  f )  <->  f D
d ) )
5751biantrurd 496 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
d  e.  H  <->  ( f  e.  H  /\  d  e.  H ) ) )
5857anbi1d 687 . . . . . . . . . . . . . . . 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 2960 . . . . . . . . . . . . . . . . 17  |-  f  e. 
_V
601, 2, 59, 53filnetlem1 26408 . . . . . . . . . . . . . . . 16  |-  ( f D d  <->  ( (
f  e.  H  /\  d  e.  H )  /\  ( 1st `  d
)  C_  ( 1st `  f ) ) )
6158, 60syl6bbr 256 . . . . . . . . . . . . . . 15  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  f  e.  H )  ->  (
( d  e.  H  /\  ( 1st `  d
)  C_  ( 1st `  f ) )  <->  f D
d ) )
6256, 61bitr4d 249 . . . . . . . . . . . . . 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 310 . . . . . . . . . . . . 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 5746 . . . . . . . . . . . . . . . . 17  |-  ( d  e.  H  ->  (
( 2nd  |`  H ) `
 d )  =  ( 2nd `  d
) )
6564eleq1d 2503 . . . . . . . . . . . . . . . 16  |-  ( d  e.  H  ->  (
( ( 2nd  |`  H ) `
 d )  e.  t  <->  ( 2nd `  d
)  e.  t ) )
6665adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( d  e.  H  /\  ( 1st `  d ) 
C_  ( 1st `  f
) )  ->  (
( ( 2nd  |`  H ) `
 d )  e.  t  <->  ( 2nd `  d
)  e.  t ) )
6766pm5.74i 238 . . . . . . . . . . . . . 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 435 . . . . . . . . . . . . . 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 242 . . . . . . . . . . . . 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 254 . . . . . . . . . . . 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 2728 . . . . . . . . . . 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 246 . . . . . . . . . 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 2723 . . . . . . . . 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 2960 . . . . . . . . . . . . . . . . 17  |-  k  e. 
_V
75 vex 2960 . . . . . . . . . . . . . . . . 17  |-  v  e. 
_V
7674, 75op1std 6358 . . . . . . . . . . . . . . . 16  |-  ( d  =  <. k ,  v
>.  ->  ( 1st `  d
)  =  k )
7776sseq1d 3376 . . . . . . . . . . . . . . 15  |-  ( d  =  <. k ,  v
>.  ->  ( ( 1st `  d )  C_  ( 1st `  f )  <->  k  C_  ( 1st `  f ) ) )
7874, 75op2ndd 6359 . . . . . . . . . . . . . . . 16  |-  ( d  =  <. k ,  v
>.  ->  ( 2nd `  d
)  =  v )
7978eleq1d 2503 . . . . . . . . . . . . . . 15  |-  ( d  =  <. k ,  v
>.  ->  ( ( 2nd `  d )  e.  t  <-> 
v  e.  t ) )
8077, 79imbi12d 313 . . . . . . . . . . . . . 14  |-  ( d  =  <. k ,  v
>.  ->  ( ( ( 1st `  d ) 
C_  ( 1st `  f
)  ->  ( 2nd `  d )  e.  t )  <->  ( k  C_  ( 1st `  f )  ->  v  e.  t ) ) )
8180raliunxp 5015 . . . . . . . . . . . . 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 3826 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  { n }  =  { k } )
83 id 21 . . . . . . . . . . . . . . . . 17  |-  ( n  =  k  ->  n  =  k )
8482, 83xpeq12d 4904 . . . . . . . . . . . . . . . 16  |-  ( n  =  k  ->  ( { n }  X.  n )  =  ( { k }  X.  k ) )
8584cbviunv 4131 . . . . . . . . . . . . . . 15  |-  U_ n  e.  F  ( {
n }  X.  n
)  =  U_ k  e.  F  ( {
k }  X.  k
)
861, 85eqtri 2457 . . . . . . . . . . . . . 14  |-  H  = 
U_ k  e.  F  ( { k }  X.  k )
8786raleqi 2909 . . . . . . . . . . . . 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 3339 . . . . . . . . . . . . . . . 16  |-  ( k 
C_  t  <->  A. v  e.  k  v  e.  t )
8988imbi2i 305 . . . . . . . . . . . . . . 15  |-  ( ( k  C_  ( 1st `  f )  ->  k  C_  t )  <->  ( k  C_  ( 1st `  f
)  ->  A. v  e.  k  v  e.  t ) )
90 r19.21v 2794 . . . . . . . . . . . . . . 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 245 . . . . . . . . . . . . . 14  |-  ( ( k  C_  ( 1st `  f )  ->  k  C_  t )  <->  A. v  e.  k  ( k  C_  ( 1st `  f
)  ->  v  e.  t ) )
9291ralbii 2730 . . . . . . . . . . . . 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 270 . . . . . . . . . . . 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 2731 . . . . . . . . . . 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 2910 . . . . . . . . . . 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 2960 . . . . . . . . . . . . . . . 16  |-  n  e. 
_V
97 vex 2960 . . . . . . . . . . . . . . . 16  |-  m  e. 
_V
9896, 97op1std 6358 . . . . . . . . . . . . . . 15  |-  ( f  =  <. n ,  m >.  ->  ( 1st `  f
)  =  n )
9998sseq2d 3377 . . . . . . . . . . . . . 14  |-  ( f  =  <. n ,  m >.  ->  ( k  C_  ( 1st `  f )  <-> 
k  C_  n )
)
10099imbi1d 310 . . . . . . . . . . . . 13  |-  ( f  =  <. n ,  m >.  ->  ( ( k 
C_  ( 1st `  f
)  ->  k  C_  t )  <->  ( k  C_  n  ->  k  C_  t ) ) )
101100ralbidv 2726 . . . . . . . . . . . 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 5016 . . . . . . . . . . 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 264 . . . . . . . . . 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 17883 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  n  =/=  (/) )
105104adantlr 697 . . . . . . . . . . . . 13  |-  ( ( ( F  e.  ( Fil `  X )  /\  t  C_  X
)  /\  n  e.  F )  ->  n  =/=  (/) )
106 r19.9rzv 3723 . . . . . . . . . . . . 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 3368 . . . . . . . . . . . . . . 15  |-  n  C_  n
109 sseq1 3370 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  (
k  C_  n  <->  n  C_  n
) )
110 sseq1 3370 . . . . . . . . . . . . . . . . 17  |-  ( k  =  n  ->  (
k  C_  t  <->  n  C_  t
) )
111109, 110imbi12d 313 . . . . . . . . . . . . . . . 16  |-  ( k  =  n  ->  (
( k  C_  n  ->  k  C_  t )  <->  ( n  C_  n  ->  n 
C_  t ) ) )
112111rspcv 3049 . . . . . . . . . . . . . . 15  |-  ( n  e.  F  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  ->  ( n  C_  n  ->  n  C_  t )
) )
113108, 112mpii 42 . . . . . . . . . . . . . 14  |-  ( n  e.  F  ->  ( A. k  e.  F  ( k  C_  n  ->  k  C_  t )  ->  n  C_  t )
)
114113adantl 454 . . . . . . . . . . . . 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 3356 . . . . . . . . . . . . . . 15  |-  ( k 
C_  n  ->  (
n  C_  t  ->  k 
C_  t ) )
116115com12 30 . . . . . . . . . . . . . 14  |-  ( n 
C_  t  ->  (
k  C_  n  ->  k 
C_  t ) )
117116ralrimivw 2791 . . . . . . . . . . . . 13  |-  ( n 
C_  t  ->  A. k  e.  F  ( k  C_  n  ->  k  C_  t ) )
118114, 117impbid1 196 . . . . . . . . . . . 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 248 . . . . . . . . . . 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 2723 . . . . . . . . . 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 250 . . . . . . . . 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 272 . . . . . . . 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 624 . . . . . . 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 17895 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  F  =/=  (/) )
12596snnz 3923 . . . . . . . . . . . . . . . 16  |-  { n }  =/=  (/)
126104, 125jctil 525 . . . . . . . . . . . . . . 15  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  ( { n }  =/=  (/) 
/\  n  =/=  (/) ) )
127 neanior 2690 . . . . . . . . . . . . . . 15  |-  ( ( { n }  =/=  (/) 
/\  n  =/=  (/) )  <->  -.  ( { n }  =  (/) 
\/  n  =  (/) ) )
128126, 127sylib 190 . . . . . . . . . . . . . 14  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  -.  ( { n }  =  (/) 
\/  n  =  (/) ) )
129 ss0b 3658 . . . . . . . . . . . . . . 15  |-  ( ( { n }  X.  n )  C_  (/)  <->  ( {
n }  X.  n
)  =  (/) )
130 xpeq0 5294 . . . . . . . . . . . . . . 15  |-  ( ( { n }  X.  n )  =  (/)  <->  ( { n }  =  (/) 
\/  n  =  (/) ) )
131129, 130bitri 242 . . . . . . . . . . . . . 14  |-  ( ( { n }  X.  n )  C_  (/)  <->  ( {
n }  =  (/)  \/  n  =  (/) ) )
132128, 131sylnibr 298 . . . . . . . . . . . . 13  |-  ( ( F  e.  ( Fil `  X )  /\  n  e.  F )  ->  -.  ( { n }  X.  n )  C_  (/) )
133132ralrimiva 2790 . . . . . . . . . . . 12  |-  ( F  e.  ( Fil `  X
)  ->  A. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
134 r19.2z 3718 . . . . . . . . . . . 12  |-  ( ( F  =/=  (/)  /\  A. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )  ->  E. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
135124, 133, 134syl2anc 644 . . . . . . . . . . 11  |-  ( F  e.  ( Fil `  X
)  ->  E. n  e.  F  -.  ( { n }  X.  n )  C_  (/) )
136 rexnal 2717 . . . . . . . . . . 11  |-  ( E. n  e.  F  -.  ( { n }  X.  n )  C_  (/)  <->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
137135, 136sylib 190 . . . . . . . . . 10  |-  ( F  e.  ( Fil `  X
)  ->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
1381sseq1i 3373 . . . . . . . . . . . 12  |-  ( H 
C_  (/)  <->  U_ n  e.  F  ( { n }  X.  n )  C_  (/) )
139 ss0b 3658 . . . . . . . . . . . 12  |-  ( H 
C_  (/)  <->  H  =  (/) )
140 iunss 4133 . . . . . . . . . . . 12  |-  ( U_ n  e.  F  ( { n }  X.  n )  C_  (/)  <->  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
141138, 139, 1403bitr3i 268 . . . . . . . . . . 11  |-  ( H  =  (/)  <->  A. n  e.  F  ( { n }  X.  n )  C_  (/) )
142141necon3abii 2632 . . . . . . . . . 10  |-  ( H  =/=  (/)  <->  -.  A. n  e.  F  ( {
n }  X.  n
)  C_  (/) )
143137, 142sylibr 205 . . . . . . . . 9  |-  ( F  e.  ( Fil `  X
)  ->  H  =/=  (/) )
144 dmresi 5197 . . . . . . . . . . . 12  |-  dom  (  _I  |`  H )  =  H
1451, 2filnetlem2 26409 . . . . . . . . . . . . . 14  |-  ( (  _I  |`  H )  C_  D  /\  D  C_  ( H  X.  H
) )
146145simpli 446 . . . . . . . . . . . . 13  |-  (  _I  |`  H )  C_  D
147 dmss 5070 . . . . . . . . . . . . 13  |-  ( (  _I  |`  H )  C_  D  ->  dom  (  _I  |`  H )  C_  dom  D )
148146, 147ax-mp 8 . . . . . . . . . . . 12  |-  dom  (  _I  |`  H )  C_  dom  D
149144, 148eqsstr3i 3380 . . . . . . . . . . 11  |-  H  C_  dom  D
150145simpri 450 . . . . . . . . . . . . 13  |-  D  C_  ( H  X.  H
)
151 dmss 5070 . . . . . . . . . . . . 13  |-  ( D 
C_  ( H  X.  H )  ->  dom  D 
C_  dom  ( H  X.  H ) )
152150, 151ax-mp 8 . . . . . . . . . . . 12  |-  dom  D  C_ 
dom  ( H  X.  H )
153 dmxpid 5090 . . . . . . . . . . . 12  |-  dom  ( H  X.  H )  =  H
154152, 153sseqtri 3381 . . . . . . . . . . 11  |-  dom  D  C_  H
155149, 154eqssi 3365 . . . . . . . . . 10  |-  H  =  dom  D
156155tailfb 26407 . . . . . . . . 9  |-  ( ( D  e.  DirRel  /\  H  =/=  (/) )  ->  ran  ( tail `  D )  e.  ( fBas `  H
) )
1575, 143, 156syl2anc 644 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  ran  ( tail `  D )  e.  (
fBas `  H )
)
158 elfm 17980 . . . . . . . 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 1185 . . . . . . 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 17881 . . . . . . . 8  |-  ( F  e.  ( Fil `  X
)  ->  F  e.  ( fBas `  X )
)
161 elfg 17904 . . . . . . . 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 278 . . . . . 6  |-  ( F  e.  ( Fil `  X
)  ->  ( t  e.  ( ( X  FilMap  ( 2nd  |`  H )
) `  ran  ( tail `  D ) )  <->  t  e.  ( X filGen F ) ) )
164163eqrdv 2435 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) )  =  ( X filGen F ) )
165 fgfil 17908 . . . . 5  |-  ( F  e.  ( Fil `  X
)  ->  ( X filGen F )  =  F )
166164, 165eqtr2d 2470 . . . 4  |-  ( F  e.  ( Fil `  X
)  ->  F  =  ( ( X  FilMap  ( 2nd  |`  H )
) `  ran  ( tail `  D ) ) )
16721, 166jca 520 . . 3  |-  ( F  e.  ( Fil `  X
)  ->  ( ( 2nd  |`  H ) : dom  D --> X  /\  F  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) ) )
168 feq1 5577 . . . . 5  |-  ( f  =  ( 2nd  |`  H )  ->  ( f : dom  D --> X  <->  ( 2nd  |`  H ) : dom  D --> X ) )
169 oveq2 6090 . . . . . . 7  |-  ( f  =  ( 2nd  |`  H )  ->  ( X  FilMap  f )  =  ( X 
FilMap  ( 2nd  |`  H ) ) )
170169fveq1d 5731 . . . . . 6  |-  ( f  =  ( 2nd  |`  H )  ->  ( ( X 
FilMap  f ) `  ran  ( tail `  D )
)  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) )
171170eqeq2d 2448 . . . . 5  |-  ( f  =  ( 2nd  |`  H )  ->  ( F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) )  <-> 
F  =  ( ( X  FilMap  ( 2nd  |`  H ) ) `  ran  ( tail `  D ) ) ) )
172168, 171anbi12d 693 . . . 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 3038 . . 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 59 . 2  |-  ( F  e.  ( Fil `  X
)  ->  E. f
( f : dom  D --> X  /\  F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) ) )
175 dmeq 5071 . . . . . 6  |-  ( d  =  D  ->  dom  d  =  dom  D )
176175feq2d 5582 . . . . 5  |-  ( d  =  D  ->  (
f : dom  d --> X 
<->  f : dom  D --> X ) )
177 fveq2 5729 . . . . . . . 8  |-  ( d  =  D  ->  ( tail `  d )  =  ( tail `  D
) )
178177rneqd 5098 . . . . . . 7  |-  ( d  =  D  ->  ran  ( tail `  d )  =  ran  ( tail `  D
) )
179178fveq2d 5733 . . . . . 6  |-  ( d  =  D  ->  (
( X  FilMap  f ) `
 ran  ( tail `  d ) )  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) )
180179eqeq2d 2448 . . . . 5  |-  ( d  =  D  ->  ( F  =  ( ( X  FilMap  f ) `  ran  ( tail `  d
) )  <->  F  =  ( ( X  FilMap  f ) `  ran  ( tail `  D ) ) ) )
181176, 180anbi12d 693 . . . 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 1637 . . 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 3053 . 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 644 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 178    \/ wo 359    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1726    =/= wne 2600   A.wral 2706   E.wrex 2707   _Vcvv 2957    C_ wss 3321   (/)c0 3629   ~Pcpw 3800   {csn 3815   <.cop 3818   U.cuni 4016   U_ciun 4094   class class class wbr 4213   {copab 4266    _I cid 4494    X. cxp 4877   dom cdm 4879   ran crn 4880    |` cres 4881   "cima 4882   Fun wfun 5449    Fn wfn 5450   -->wf 5451   -onto->wfo 5453   ` cfv 5455  (class class class)co 6082   1stc1st 6348   2ndc2nd 6349   DirRelcdir 14674   tailctail 14675   fBascfbas 16690   filGencfg 16691   Filcfil 17878    FilMap cfm 17966
This theorem is referenced by:  filnet  26412
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-op 3824  df-uni 4017  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-id 4499  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-1st 6350  df-2nd 6351  df-dir 14676  df-tail 14677  df-fbas 16700  df-fg 16701  df-fil 17879  df-fm 17971
  Copyright terms: Public domain W3C validator