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

Theorem neibastop2lem 31016
Description: Lemma for neibastop2 31017. (Contributed by Jeff Hankins, 12-Sep-2009.)
Hypotheses
Ref Expression
neibastop1.1  |-  ( ph  ->  X  e.  V )
neibastop1.2  |-  ( ph  ->  F : X --> ( ~P ~P X  \  { (/)
} ) )
neibastop1.3  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
)  /\  w  e.  ( F `  x ) ) )  ->  (
( F `  x
)  i^i  ~P (
v  i^i  w )
)  =/=  (/) )
neibastop1.4  |-  J  =  { o  e.  ~P X  |  A. x  e.  o  ( ( F `  x )  i^i  ~P o )  =/=  (/) }
neibastop1.5  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  x  e.  v )
neibastop1.6  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  E. t  e.  ( F `  x ) A. y  e.  t 
( ( F `  y )  i^i  ~P v )  =/=  (/) )
neibastop2.p  |-  ( ph  ->  P  e.  X )
neibastop2.n  |-  ( ph  ->  N  C_  X )
neibastop2.f  |-  ( ph  ->  U  e.  ( F `
 P ) )
neibastop2.u  |-  ( ph  ->  U  C_  N )
neibastop2.g  |-  G  =  ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) ) ,  { U } )  |`  om )
neibastop2.s  |-  S  =  { y  e.  X  |  E. f  e.  U. ran  G ( ( F `
 y )  i^i 
~P f )  =/=  (/) }
Assertion
Ref Expression
neibastop2lem  |-  ( ph  ->  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) )
Distinct variable groups:    t, f,
v, y, z, G   
v, u, x, y, z, J    f, o, u, w, x, P, t, v, y, z    f, N, o, t, u, v, w, x, y, z    S, f, o, t, u, v, x, y    U, f, x, y, z    f,
a, o, t, u, v, w, x, y, z, F    ph, f, o, t, v, w, x, y, z    X, a, f, o, t, u, v, w, x, y, z
Allowed substitution hints:    ph( u, a)    P( a)    S( z, w, a)    U( w, v, u, t, o, a)    G( x, w, u, o, a)    J( w, t, f, o, a)    N( a)    V( x, y, z, w, v, u, t, f, o, a)

Proof of Theorem neibastop2lem
Dummy variables  k  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neibastop2.s . . . . 5  |-  S  =  { y  e.  X  |  E. f  e.  U. ran  G ( ( F `
 y )  i^i 
~P f )  =/=  (/) }
2 ssrab2 3514 . . . . 5  |-  { y  e.  X  |  E. f  e.  U. ran  G
( ( F `  y )  i^i  ~P f )  =/=  (/) }  C_  X
31, 2eqsstri 3462 . . . 4  |-  S  C_  X
4 neibastop1.1 . . . . 5  |-  ( ph  ->  X  e.  V )
5 elpw2g 4566 . . . . 5  |-  ( X  e.  V  ->  ( S  e.  ~P X  <->  S 
C_  X ) )
64, 5syl 17 . . . 4  |-  ( ph  ->  ( S  e.  ~P X 
<->  S  C_  X )
)
73, 6mpbiri 237 . . 3  |-  ( ph  ->  S  e.  ~P X
)
8 fveq2 5865 . . . . . . . . 9  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
98ineq1d 3633 . . . . . . . 8  |-  ( y  =  x  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  x )  i^i  ~P f ) )
109neeq1d 2683 . . . . . . 7  |-  ( y  =  x  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P f )  =/=  (/) ) )
1110rexbidv 2901 . . . . . 6  |-  ( y  =  x  ->  ( E. f  e.  U. ran  G ( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  E. f  e.  U. ran  G ( ( F `  x
)  i^i  ~P f
)  =/=  (/) ) )
1211, 1elrab2 3198 . . . . 5  |-  ( x  e.  S  <->  ( x  e.  X  /\  E. f  e.  U. ran  G ( ( F `  x
)  i^i  ~P f
)  =/=  (/) ) )
13 frfnom 7152 . . . . . . . . . 10  |-  ( rec ( ( a  e. 
_V  |->  U_ z  e.  a 
U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) ) ,  { U } )  |`  om )  Fn  om
14 neibastop2.g . . . . . . . . . . 11  |-  G  =  ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) ) ,  { U } )  |`  om )
1514fneq1i 5670 . . . . . . . . . 10  |-  ( G  Fn  om  <->  ( rec ( ( a  e. 
_V  |->  U_ z  e.  a 
U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) ) ,  { U } )  |`  om )  Fn  om )
1613, 15mpbir 213 . . . . . . . . 9  |-  G  Fn  om
17 fnunirn 6158 . . . . . . . . 9  |-  ( G  Fn  om  ->  (
f  e.  U. ran  G  <->  E. k  e.  om  f  e.  ( G `  k ) ) )
1816, 17ax-mp 5 . . . . . . . 8  |-  ( f  e.  U. ran  G  <->  E. k  e.  om  f  e.  ( G `  k
) )
19 n0 3741 . . . . . . . . . 10  |-  ( ( ( F `  x
)  i^i  ~P f
)  =/=  (/)  <->  E. v 
v  e.  ( ( F `  x )  i^i  ~P f ) )
20 inss1 3652 . . . . . . . . . . . . . . . 16  |-  ( ( F `  x )  i^i  ~P f ) 
C_  ( F `  x )
2120sseli 3428 . . . . . . . . . . . . . . 15  |-  ( v  e.  ( ( F `
 x )  i^i 
~P f )  -> 
v  e.  ( F `
 x ) )
22 neibastop1.6 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  E. t  e.  ( F `  x ) A. y  e.  t 
( ( F `  y )  i^i  ~P v )  =/=  (/) )
2322anassrs 654 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  x  e.  X )  /\  v  e.  ( F `  x
) )  ->  E. t  e.  ( F `  x
) A. y  e.  t  ( ( F `
 y )  i^i 
~P v )  =/=  (/) )
2421, 23sylan2 477 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  X )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) )  ->  E. t  e.  ( F `  x ) A. y  e.  t 
( ( F `  y )  i^i  ~P v )  =/=  (/) )
2524adantrl 722 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  E. t  e.  ( F `  x ) A. y  e.  t 
( ( F `  y )  i^i  ~P v )  =/=  (/) )
26 simprl 764 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e. 
om  /\  f  e.  ( G `  k ) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  ( t  e.  ( F `  x
)  /\  A. y  e.  t  ( ( F `  y )  i^i  ~P v )  =/=  (/) ) )  ->  t  e.  ( F `  x
) )
27 fvssunirn 5888 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F `
 x )  C_  U.
ran  F
28 neibastop1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  F : X --> ( ~P ~P X  \  { (/)
} ) )
29 frn 5735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( F : X --> ( ~P ~P X  \  { (/)
} )  ->  ran  F 
C_  ( ~P ~P X  \  { (/) } ) )
3028, 29syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ran  F  C_  ( ~P ~P X  \  { (/)
} ) )
3130difss2d 3563 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ran  F  C_  ~P ~P X )
32 sspwuni 4367 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ran 
F  C_  ~P ~P X 
<-> 
U. ran  F  C_  ~P X )
3331, 32sylib 200 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  U. ran  F  C_  ~P X )
3433ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  U. ran  F  C_  ~P X )
3527, 34syl5ss 3443 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
( F `  x
)  C_  ~P X
)
3635sselda 3432 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e. 
om  /\  f  e.  ( G `  k ) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  t  e.  ( F `  x ) )  ->  t  e.  ~P X )
3736elpwid 3961 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e. 
om  /\  f  e.  ( G `  k ) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  t  e.  ( F `  x ) )  ->  t  C_  X )
3837sselda 3432 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e.  om  /\  f  e.  ( G `  k
) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  t  e.  ( F `  x ) )  /\  y  e.  t )  ->  y  e.  X )
3938adantrr 723 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e.  om  /\  f  e.  ( G `  k
) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  t  e.  ( F `  x ) )  /\  ( y  e.  t  /\  (
( F `  y
)  i^i  ~P v
)  =/=  (/) ) )  ->  y  e.  X
)
40 simprlr 773 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
f  e.  ( G `
 k ) )
41 rspe 2845 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( x  e.  X  /\  v  e.  ( ( F `  x )  i^i  ~P f ) )  ->  E. x  e.  X  v  e.  ( ( F `  x )  i^i  ~P f ) )
4241ad2ant2l 752 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  E. x  e.  X  v  e.  ( ( F `  x )  i^i  ~P f ) )
43 eliun 4283 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( v  e.  U_ x  e.  X  ( ( F `
 x )  i^i 
~P z )  <->  E. x  e.  X  v  e.  ( ( F `  x )  i^i  ~P z ) )
44 pweq 3954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  =  f  ->  ~P z  =  ~P f
)
4544ineq2d 3634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  =  f  ->  (
( F `  x
)  i^i  ~P z
)  =  ( ( F `  x )  i^i  ~P f ) )
4645eleq2d 2514 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  f  ->  (
v  e.  ( ( F `  x )  i^i  ~P z )  <-> 
v  e.  ( ( F `  x )  i^i  ~P f ) ) )
4746rexbidv 2901 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  f  ->  ( E. x  e.  X  v  e.  ( ( F `  x )  i^i  ~P z )  <->  E. x  e.  X  v  e.  ( ( F `  x )  i^i  ~P f ) ) )
4843, 47syl5bb 261 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  f  ->  (
v  e.  U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  <->  E. x  e.  X  v  e.  ( ( F `  x )  i^i  ~P f ) ) )
4948rspcev 3150 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( f  e.  ( G `
 k )  /\  E. x  e.  X  v  e.  ( ( F `
 x )  i^i 
~P f ) )  ->  E. z  e.  ( G `  k ) v  e.  U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
5040, 42, 49syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  E. z  e.  ( G `  k )
v  e.  U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
51 eliun 4283 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( v  e.  U_ z  e.  ( G `  k
) U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  <->  E. z  e.  ( G `  k
) v  e.  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) )
5250, 51sylibr 216 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
v  e.  U_ z  e.  ( G `  k
) U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
53 simpll 760 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  ph )
54 simprll 772 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
k  e.  om )
55 fvssunirn 5888 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( G `
 k )  C_  U.
ran  G
56 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( n  =  (/)  ->  ( G `
 n )  =  ( G `  (/) ) )
5714fveq1i 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( G `
 (/) )  =  ( ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) ) ,  { U } )  |`  om ) `  (/) )
58 snex 4641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  { U }  e.  _V
59 fr0g 7153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( { U }  e.  _V  ->  ( ( rec (
( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) ) ,  { U } )  |`  om ) `  (/) )  =  { U } )
6058, 59ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  ( ( F `
 x )  i^i 
~P z ) ) ,  { U }
)  |`  om ) `  (/) )  =  { U }
6157, 60eqtri 2473 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( G `
 (/) )  =  { U }
6256, 61syl6eq 2501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  =  (/)  ->  ( G `
 n )  =  { U } )
6362sseq1d 3459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( n  =  (/)  ->  ( ( G `  n ) 
C_  ~P U  <->  { U }  C_  ~P U ) )
64 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  =  k  ->  ( G `  n )  =  ( G `  k ) )
6564sseq1d 3459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( n  =  k  ->  (
( G `  n
)  C_  ~P U  <->  ( G `  k ) 
C_  ~P U ) )
66 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  =  suc  k  -> 
( G `  n
)  =  ( G `
 suc  k )
)
6766sseq1d 3459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( n  =  suc  k  -> 
( ( G `  n )  C_  ~P U 
<->  ( G `  suc  k )  C_  ~P U ) )
68 neibastop2.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  U  e.  ( F `
 P ) )
69 pwidg 3964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( U  e.  ( F `  P )  ->  U  e.  ~P U )
7068, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  U  e.  ~P U
)
7170snssd 4117 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  { U }  C_  ~P U )
72 simprl 764 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  -> 
k  e.  om )
7368adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  ->  U  e.  ( F `  P ) )
74 pwexg 4587 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( U  e.  ( F `  P )  ->  ~P U  e.  _V )
7573, 74syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  ->  ~P U  e.  _V )
76 inss2 3653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( F `  x )  i^i  ~P z ) 
C_  ~P z
77 elpwi 3960 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( z  e.  ~P U  -> 
z  C_  U )
7877adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  z  e.  ~P U )  ->  z  C_  U )
79 sspwb 4649 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( z 
C_  U  <->  ~P z  C_ 
~P U )
8078, 79sylib 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  z  e.  ~P U )  ->  ~P z  C_  ~P U )
8176, 80syl5ss 3443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  z  e.  ~P U )  ->  (
( F `  x
)  i^i  ~P z
)  C_  ~P U
)
8281ralrimivw 2803 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  z  e.  ~P U )  ->  A. x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
83 iunss 4319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( U_ x  e.  X  (
( F `  x
)  i^i  ~P z
)  C_  ~P U  <->  A. x  e.  X  ( ( F `  x
)  i^i  ~P z
)  C_  ~P U
)
8482, 83sylibr 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  z  e.  ~P U )  ->  U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
8584ralrimiva 2802 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  A. z  e.  ~P  U U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
86 ssralv 3493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( G `  k ) 
C_  ~P U  ->  ( A. z  e.  ~P  U U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U  ->  A. z  e.  ( G `  k )
U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U ) )
8786adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( k  e.  om  /\  ( G `  k ) 
C_  ~P U )  -> 
( A. z  e. 
~P  U U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U  ->  A. z  e.  ( G `  k
) U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U ) )
8885, 87mpan9 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  ->  A. z  e.  ( G `  k ) U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
89 iunss 4319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( U_ z  e.  ( G `  k ) U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U  <->  A. z  e.  ( G `  k )
U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
9088, 89sylibr 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  ->  U_ z  e.  ( G `  k ) U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
9175, 90ssexd 4550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  ->  U_ z  e.  ( G `  k ) U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  e.  _V )
92 iuneq1 4292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( y  =  a  ->  U_ z  e.  y  U_ x  e.  X  ( ( F `
 x )  i^i 
~P z )  = 
U_ z  e.  a 
U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
93 iuneq1 4292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( y  =  ( G `  k )  ->  U_ z  e.  y  U_ x  e.  X  ( ( F `
 x )  i^i 
~P z )  = 
U_ z  e.  ( G `  k )
U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
9414, 92, 93frsucmpt2 7157 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( k  e.  om  /\  U_ z  e.  ( G `
 k ) U_ x  e.  X  (
( F `  x
)  i^i  ~P z
)  e.  _V )  ->  ( G `  suc  k )  =  U_ z  e.  ( G `  k ) U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
9572, 91, 94syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  -> 
( G `  suc  k )  =  U_ z  e.  ( G `  k ) U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
9695, 90eqsstrd 3466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  -> 
( G `  suc  k )  C_  ~P U )
9796expr 620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  k  e.  om )  ->  ( ( G `  k )  C_ 
~P U  ->  ( G `  suc  k ) 
C_  ~P U ) )
9897expcom 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  e.  om  ->  ( ph  ->  ( ( G `
 k )  C_  ~P U  ->  ( G `
 suc  k )  C_ 
~P U ) ) )
9963, 65, 67, 71, 98finds2 6721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( n  e.  om  ->  ( ph  ->  ( G `  n )  C_  ~P U ) )
100 fvex 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( G `
 n )  e. 
_V
101100elpw 3957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( G `  n )  e.  ~P ~P U  <->  ( G `  n ) 
C_  ~P U )
10299, 101syl6ibr 231 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( n  e.  om  ->  ( ph  ->  ( G `  n )  e.  ~P ~P U ) )
103102com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( n  e.  om  ->  ( G `  n
)  e.  ~P ~P U ) )
104103ralrimiv 2800 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  A. n  e.  om  ( G `  n )  e.  ~P ~P U
)
105 ffnfv 6049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( G : om --> ~P ~P U 
<->  ( G  Fn  om  /\ 
A. n  e.  om  ( G `  n )  e.  ~P ~P U
) )
10616, 105mpbiran 929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( G : om --> ~P ~P U 
<-> 
A. n  e.  om  ( G `  n )  e.  ~P ~P U
)
107104, 106sylibr 216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  G : om --> ~P ~P U )
108 frn 5735 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( G : om --> ~P ~P U  ->  ran  G  C_  ~P ~P U )
109107, 108syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ran  G  C_  ~P ~P U )
110 sspwuni 4367 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ran 
G  C_  ~P ~P U 
<-> 
U. ran  G  C_  ~P U )
111109, 110sylib 200 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  U. ran  G  C_  ~P U )
112111ad2antrr 732 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  U. ran  G  C_  ~P U )
11355, 112syl5ss 3443 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
( G `  k
)  C_  ~P U
)
11453, 54, 113, 95syl12anc 1266 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
( G `  suc  k )  =  U_ z  e.  ( G `  k ) U_ x  e.  X  ( ( F `  x )  i^i  ~P z ) )
11552, 114eleqtrrd 2532 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
v  e.  ( G `
 suc  k )
)
116 peano2 6713 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  om  ->  suc  k  e.  om )
11754, 116syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  suc  k  e.  om )
118 fnfvelrn 6019 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( G  Fn  om  /\  suc  k  e.  om )  ->  ( G `  suc  k )  e.  ran  G )
11916, 117, 118sylancr 669 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
( G `  suc  k )  e.  ran  G )
120 elunii 4203 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  ( G `
 suc  k )  /\  ( G `  suc  k )  e.  ran  G )  ->  v  e.  U.
ran  G )
121115, 119, 120syl2anc 667 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
v  e.  U. ran  G )
122121ad2antrr 732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e.  om  /\  f  e.  ( G `  k
) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  t  e.  ( F `  x ) )  /\  ( y  e.  t  /\  (
( F `  y
)  i^i  ~P v
)  =/=  (/) ) )  ->  v  e.  U. ran  G )
123 simprr 766 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e.  om  /\  f  e.  ( G `  k
) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  t  e.  ( F `  x ) )  /\  ( y  e.  t  /\  (
( F `  y
)  i^i  ~P v
)  =/=  (/) ) )  ->  ( ( F `
 y )  i^i 
~P v )  =/=  (/) )
124 pweq 3954 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  v  ->  ~P f  =  ~P v
)
125124ineq2d 3634 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  v  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  y )  i^i  ~P v ) )
126125neeq1d 2683 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  v  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  y )  i^i  ~P v )  =/=  (/) ) )
127126rspcev 3150 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( v  e.  U. ran  G  /\  ( ( F `
 y )  i^i 
~P v )  =/=  (/) )  ->  E. f  e.  U. ran  G ( ( F `  y
)  i^i  ~P f
)  =/=  (/) )
128122, 123, 127syl2anc 667 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e.  om  /\  f  e.  ( G `  k
) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  t  e.  ( F `  x ) )  /\  ( y  e.  t  /\  (
( F `  y
)  i^i  ~P v
)  =/=  (/) ) )  ->  E. f  e.  U. ran  G ( ( F `
 y )  i^i 
~P f )  =/=  (/) )
1291rabeq2i 3042 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  S  <->  ( y  e.  X  /\  E. f  e.  U. ran  G ( ( F `  y
)  i^i  ~P f
)  =/=  (/) ) )
13039, 128, 129sylanbrc 670 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e.  om  /\  f  e.  ( G `  k
) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  t  e.  ( F `  x ) )  /\  ( y  e.  t  /\  (
( F `  y
)  i^i  ~P v
)  =/=  (/) ) )  ->  y  e.  S
)
131130expr 620 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e.  om  /\  f  e.  ( G `  k
) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  t  e.  ( F `  x ) )  /\  y  e.  t )  ->  (
( ( F `  y )  i^i  ~P v )  =/=  (/)  ->  y  e.  S ) )
132131ralimdva 2796 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e. 
om  /\  f  e.  ( G `  k ) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  t  e.  ( F `  x ) )  ->  ( A. y  e.  t  (
( F `  y
)  i^i  ~P v
)  =/=  (/)  ->  A. y  e.  t  y  e.  S ) )
133132impr 625 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e. 
om  /\  f  e.  ( G `  k ) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  ( t  e.  ( F `  x
)  /\  A. y  e.  t  ( ( F `  y )  i^i  ~P v )  =/=  (/) ) )  ->  A. y  e.  t  y  e.  S )
134 dfss3 3422 . . . . . . . . . . . . . . . 16  |-  ( t 
C_  S  <->  A. y  e.  t  y  e.  S )
135133, 134sylibr 216 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e. 
om  /\  f  e.  ( G `  k ) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  ( t  e.  ( F `  x
)  /\  A. y  e.  t  ( ( F `  y )  i^i  ~P v )  =/=  (/) ) )  ->  t  C_  S )
136 selpw 3958 . . . . . . . . . . . . . . 15  |-  ( t  e.  ~P S  <->  t  C_  S )
137135, 136sylibr 216 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e. 
om  /\  f  e.  ( G `  k ) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  ( t  e.  ( F `  x
)  /\  A. y  e.  t  ( ( F `  y )  i^i  ~P v )  =/=  (/) ) )  ->  t  e.  ~P S )
138 inelcm 3819 . . . . . . . . . . . . . 14  |-  ( ( t  e.  ( F `
 x )  /\  t  e.  ~P S
)  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) )
13926, 137, 138syl2anc 667 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  x  e.  X )  /\  ( ( k  e. 
om  /\  f  e.  ( G `  k ) )  /\  v  e.  ( ( F `  x )  i^i  ~P f ) ) )  /\  ( t  e.  ( F `  x
)  /\  A. y  e.  t  ( ( F `  y )  i^i  ~P v )  =/=  (/) ) )  ->  (
( F `  x
)  i^i  ~P S
)  =/=  (/) )
14025, 139rexlimddv 2883 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
( ( F `  x )  i^i  ~P S )  =/=  (/) )
141140expr 620 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  X )  /\  (
k  e.  om  /\  f  e.  ( G `  k ) ) )  ->  ( v  e.  ( ( F `  x )  i^i  ~P f )  ->  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) )
142141exlimdv 1779 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  X )  /\  (
k  e.  om  /\  f  e.  ( G `  k ) ) )  ->  ( E. v 
v  e.  ( ( F `  x )  i^i  ~P f )  ->  ( ( F `
 x )  i^i 
~P S )  =/=  (/) ) )
14319, 142syl5bi 221 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  X )  /\  (
k  e.  om  /\  f  e.  ( G `  k ) ) )  ->  ( ( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
144143rexlimdvaa 2880 . . . . . . . 8  |-  ( (
ph  /\  x  e.  X )  ->  ( E. k  e.  om  f  e.  ( G `  k )  ->  (
( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) ) )
14518, 144syl5bi 221 . . . . . . 7  |-  ( (
ph  /\  x  e.  X )  ->  (
f  e.  U. ran  G  ->  ( ( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) ) )
146145rexlimdv 2877 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  ( E. f  e.  U. ran  G ( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) )
147146expimpd 608 . . . . 5  |-  ( ph  ->  ( ( x  e.  X  /\  E. f  e.  U. ran  G ( ( F `  x
)  i^i  ~P f
)  =/=  (/) )  -> 
( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
14812, 147syl5bi 221 . . . 4  |-  ( ph  ->  ( x  e.  S  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
149148ralrimiv 2800 . . 3  |-  ( ph  ->  A. x  e.  S  ( ( F `  x )  i^i  ~P S )  =/=  (/) )
150 pweq 3954 . . . . . . 7  |-  ( o  =  S  ->  ~P o  =  ~P S
)
151150ineq2d 3634 . . . . . 6  |-  ( o  =  S  ->  (
( F `  x
)  i^i  ~P o
)  =  ( ( F `  x )  i^i  ~P S ) )
152151neeq1d 2683 . . . . 5  |-  ( o  =  S  ->  (
( ( F `  x )  i^i  ~P o )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
153152raleqbi1dv 2995 . . . 4  |-  ( o  =  S  ->  ( A. x  e.  o 
( ( F `  x )  i^i  ~P o )  =/=  (/)  <->  A. x  e.  S  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
154 neibastop1.4 . . . 4  |-  J  =  { o  e.  ~P X  |  A. x  e.  o  ( ( F `  x )  i^i  ~P o )  =/=  (/) }
155153, 154elrab2 3198 . . 3  |-  ( S  e.  J  <->  ( S  e.  ~P X  /\  A. x  e.  S  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) )
1567, 149, 155sylanbrc 670 . 2  |-  ( ph  ->  S  e.  J )
157 neibastop2.p . . 3  |-  ( ph  ->  P  e.  X )
158 snidg 3994 . . . . . 6  |-  ( U  e.  ( F `  P )  ->  U  e.  { U } )
15968, 158syl 17 . . . . 5  |-  ( ph  ->  U  e.  { U } )
160 peano1 6712 . . . . . . 7  |-  (/)  e.  om
161 fnfvelrn 6019 . . . . . . 7  |-  ( ( G  Fn  om  /\  (/) 
e.  om )  ->  ( G `  (/) )  e. 
ran  G )
16216, 160, 161mp2an 678 . . . . . 6  |-  ( G `
 (/) )  e.  ran  G
16361, 162eqeltrri 2526 . . . . 5  |-  { U }  e.  ran  G
164 elunii 4203 . . . . 5  |-  ( ( U  e.  { U }  /\  { U }  e.  ran  G )  ->  U  e.  U. ran  G
)
165159, 163, 164sylancl 668 . . . 4  |-  ( ph  ->  U  e.  U. ran  G )
166 inelcm 3819 . . . . 5  |-  ( ( U  e.  ( F `
 P )  /\  U  e.  ~P U
)  ->  ( ( F `  P )  i^i  ~P U )  =/=  (/) )
16768, 70, 166syl2anc 667 . . . 4  |-  ( ph  ->  ( ( F `  P )  i^i  ~P U )  =/=  (/) )
168 pweq 3954 . . . . . . 7  |-  ( f  =  U  ->  ~P f  =  ~P U
)
169168ineq2d 3634 . . . . . 6  |-  ( f  =  U  ->  (
( F `  P
)  i^i  ~P f
)  =  ( ( F `  P )  i^i  ~P U ) )
170169neeq1d 2683 . . . . 5  |-  ( f  =  U  ->  (
( ( F `  P )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P U )  =/=  (/) ) )
171170rspcev 3150 . . . 4  |-  ( ( U  e.  U. ran  G  /\  ( ( F `
 P )  i^i 
~P U )  =/=  (/) )  ->  E. f  e.  U. ran  G ( ( F `  P
)  i^i  ~P f
)  =/=  (/) )
172165, 167, 171syl2anc 667 . . 3  |-  ( ph  ->  E. f  e.  U. ran  G ( ( F `
 P )  i^i 
~P f )  =/=  (/) )
173 fveq2 5865 . . . . . . 7  |-  ( y  =  P  ->  ( F `  y )  =  ( F `  P ) )
174173ineq1d 3633 . . . . . 6  |-  ( y  =  P  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  P )  i^i  ~P f ) )
175174neeq1d 2683 . . . . 5  |-  ( y  =  P  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P f )  =/=  (/) ) )
176175rexbidv 2901 . . . 4  |-  ( y  =  P  ->  ( E. f  e.  U. ran  G ( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  E. f  e.  U. ran  G ( ( F `  P
)  i^i  ~P f
)  =/=  (/) ) )
177176, 1elrab2 3198 . . 3  |-  ( P  e.  S  <->  ( P  e.  X  /\  E. f  e.  U. ran  G ( ( F `  P
)  i^i  ~P f
)  =/=  (/) ) )
178157, 172, 177sylanbrc 670 . 2  |-  ( ph  ->  P  e.  S )
179 eluni2 4202 . . . . . . 7  |-  ( f  e.  U. ran  G  <->  E. z  e.  ran  G  f  e.  z )
180 eleq2 2518 . . . . . . . . . 10  |-  ( z  =  ( G `  k )  ->  (
f  e.  z  <->  f  e.  ( G `  k ) ) )
181180rexrn 6024 . . . . . . . . 9  |-  ( G  Fn  om  ->  ( E. z  e.  ran  G  f  e.  z  <->  E. k  e.  om  f  e.  ( G `  k ) ) )
18216, 181ax-mp 5 . . . . . . . 8  |-  ( E. z  e.  ran  G  f  e.  z  <->  E. k  e.  om  f  e.  ( G `  k ) )
183107adantr 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  X )  ->  G : om --> ~P ~P U
)
184183ffvelrnda 6022 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  ( G `  k )  e.  ~P ~P U )
185184elpwid 3961 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  ( G `  k )  C_ 
~P U )
186185sselda 3432 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  f  e.  ~P U )
187186adantrr 723 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  e.  ~P U )
188187elpwid 3961 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  C_  U )
189 neibastop2.u . . . . . . . . . . . . 13  |-  ( ph  ->  U  C_  N )
190189ad3antrrr 736 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  U  C_  N )
191188, 190sstrd 3442 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  C_  N )
192 n0 3741 . . . . . . . . . . . . 13  |-  ( ( ( F `  y
)  i^i  ~P f
)  =/=  (/)  <->  E. v 
v  e.  ( ( F `  y )  i^i  ~P f ) )
193 elin 3617 . . . . . . . . . . . . . . 15  |-  ( v  e.  ( ( F `
 y )  i^i 
~P f )  <->  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) )
194 simprrr 775 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  v  e.  ~P f )
195194elpwid 3961 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  v  C_  f
)
196 simpllr 769 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  y  e.  X
)
197 neibastop1.5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  x  e.  v )
198197expr 620 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  X )  ->  (
v  e.  ( F `
 x )  ->  x  e.  v )
)
199198ralrimiva 2802 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. x  e.  X  ( v  e.  ( F `  x )  ->  x  e.  v ) )
200199ad3antrrr 736 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  A. x  e.  X  ( v  e.  ( F `  x )  ->  x  e.  v ) )
201 simprrl 774 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  v  e.  ( F `  y ) )
202 fveq2 5865 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
203202eleq2d 2514 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  (
v  e.  ( F `
 x )  <->  v  e.  ( F `  y ) ) )
204 elequ1 1894 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  (
x  e.  v  <->  y  e.  v ) )
205203, 204imbi12d 322 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
( v  e.  ( F `  x )  ->  x  e.  v )  <->  ( v  e.  ( F `  y
)  ->  y  e.  v ) ) )
206205rspcv 3146 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  X  ->  ( A. x  e.  X  ( v  e.  ( F `  x )  ->  x  e.  v )  ->  ( v  e.  ( F `  y
)  ->  y  e.  v ) ) )
207196, 200, 201, 206syl3c 63 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  y  e.  v )
208195, 207sseldd 3433 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  y  e.  f )
209208expr 620 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  ( (
v  e.  ( F `
 y )  /\  v  e.  ~P f
)  ->  y  e.  f ) )
210193, 209syl5bi 221 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  ( v  e.  ( ( F `  y )  i^i  ~P f )  ->  y  e.  f ) )
211210exlimdv 1779 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  ( E. v  v  e.  (
( F `  y
)  i^i  ~P f
)  ->  y  e.  f ) )
212192, 211syl5bi 221 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  ( (
( F `  y
)  i^i  ~P f
)  =/=  (/)  ->  y  e.  f ) )
213212impr 625 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  y  e.  f )
214191, 213sseldd 3433 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  y  e.  N )
215214exp32 610 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  (
f  e.  ( G `
 k )  -> 
( ( ( F `
 y )  i^i 
~P f )  =/=  (/)  ->  y  e.  N
) ) )
216215rexlimdva 2879 . . . . . . . 8  |-  ( (
ph  /\  y  e.  X )  ->  ( E. k  e.  om  f  e.  ( G `  k )  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  ->  y  e.  N ) ) )
217182, 216syl5bi 221 . . . . . . 7  |-  ( (
ph  /\  y  e.  X )  ->  ( E. z  e.  ran  G  f  e.  z  -> 
( ( ( F `
 y )  i^i 
~P f )  =/=  (/)  ->  y  e.  N
) ) )
218179, 217syl5bi 221 . . . . . 6  |-  ( (
ph  /\  y  e.  X )  ->  (
f  e.  U. ran  G  ->  ( ( ( F `  y )  i^i  ~P f )  =/=  (/)  ->  y  e.  N ) ) )
219218rexlimdv 2877 . . . . 5  |-  ( (
ph  /\  y  e.  X )  ->  ( E. f  e.  U. ran  G ( ( F `  y )  i^i  ~P f )  =/=  (/)  ->  y  e.  N ) )
2202193impia 1205 . . . 4  |-  ( (
ph  /\  y  e.  X  /\  E. f  e. 
U. ran  G (
( F `  y
)  i^i  ~P f
)  =/=  (/) )  -> 
y  e.  N )
221220rabssdv 3509 . . 3  |-  ( ph  ->  { y  e.  X  |  E. f  e.  U. ran  G ( ( F `
 y )  i^i 
~P f )  =/=  (/) }  C_  N )
2221, 221syl5eqss 3476 . 2  |-  ( ph  ->  S  C_  N )
223 eleq2 2518 . . . 4  |-  ( u  =  S  ->  ( P  e.  u  <->  P  e.  S ) )
224 sseq1 3453 . . . 4  |-  ( u  =  S  ->  (
u  C_  N  <->  S  C_  N
) )
225223, 224anbi12d 717 . . 3  |-  ( u  =  S  ->  (
( P  e.  u  /\  u  C_  N )  <-> 
( P  e.  S  /\  S  C_  N ) ) )
226225rspcev 3150 . 2  |-  ( ( S  e.  J  /\  ( P  e.  S  /\  S  C_  N ) )  ->  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) )
227156, 178, 222, 226syl12anc 1266 1  |-  ( ph  ->  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    /\ w3a 985    = wceq 1444   E.wex 1663    e. wcel 1887    =/= wne 2622   A.wral 2737   E.wrex 2738   {crab 2741   _Vcvv 3045    \ cdif 3401    i^i cin 3403    C_ wss 3404   (/)c0 3731   ~Pcpw 3951   {csn 3968   U.cuni 4198   U_ciun 4278    |-> cmpt 4461   ran crn 4835    |` cres 4836   suc csuc 5425    Fn wfn 5577   -->wf 5578   ` cfv 5582   omcom 6692   reccrdg 7127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-om 6693  df-wrecs 7028  df-recs 7090  df-rdg 7128
This theorem is referenced by:  neibastop2  31017
  Copyright terms: Public domain W3C validator