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

Theorem neibastop2lem 31015
Description: Lemma for neibastop2 31016. (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 3547 . . . . 5  |-  { y  e.  X  |  E. f  e.  U. ran  G
( ( F `  y )  i^i  ~P f )  =/=  (/) }  C_  X
31, 2eqsstri 3495 . . . 4  |-  S  C_  X
4 neibastop1.1 . . . . 5  |-  ( ph  ->  X  e.  V )
5 elpw2g 4585 . . . . 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 5879 . . . . . . . . 9  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
98ineq1d 3664 . . . . . . . 8  |-  ( y  =  x  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  x )  i^i  ~P f ) )
109neeq1d 2702 . . . . . . 7  |-  ( y  =  x  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P f )  =/=  (/) ) )
1110rexbidv 2940 . . . . . 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 3232 . . . . 5  |-  ( x  e.  S  <->  ( x  e.  X  /\  E. f  e.  U. ran  G ( ( F `  x
)  i^i  ~P f
)  =/=  (/) ) )
13 frfnom 7158 . . . . . . . . . 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 5686 . . . . . . . . . 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 6171 . . . . . . . . 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 3772 . . . . . . . . . 10  |-  ( ( ( F `  x
)  i^i  ~P f
)  =/=  (/)  <->  E. v 
v  e.  ( ( F `  x )  i^i  ~P f ) )
20 inss1 3683 . . . . . . . . . . . . . . . 16  |-  ( ( F `  x )  i^i  ~P f ) 
C_  ( F `  x )
2120sseli 3461 . . . . . . . . . . . . . . 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 653 . . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . 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 763 . . . . . . . . . . . . . 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 5902 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F `
 x )  C_  U.
ran  F
28 neibastop1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  F : X --> ( ~P ~P X  \  { (/)
} ) )
29 frn 5750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( F : X --> ( ~P ~P X  \  { (/)
} )  ->  ran  F 
C_  ( ~P ~P X  \  { (/) } ) )
3028, 29syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ran  F  C_  ( ~P ~P X  \  { (/)
} ) )
3130difss2d 3596 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ran  F  C_  ~P ~P X )
32 sspwuni 4386 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . 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 3476 . . . . . . . . . . . . . . . . . . . . . . . 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 3465 . . . . . . . . . . . . . . . . . . . . . . 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 3990 . . . . . . . . . . . . . . . . . . . . . 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 3465 . . . . . . . . . . . . . . . . . . . . 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 722 . . . . . . . . . . . . . . . . . . . 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 772 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2884 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 751 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4302 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  =  f  ->  ~P z  =  ~P f
)
4544ineq2d 3665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  =  f  ->  (
( F `  x
)  i^i  ~P z
)  =  ( ( F `  x )  i^i  ~P f ) )
4645eleq2d 2493 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  f  ->  (
v  e.  ( ( F `  x )  i^i  ~P z )  <-> 
v  e.  ( ( F `  x )  i^i  ~P f ) ) )
4746rexbidv 2940 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3183 . . . . . . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . . . . . . 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 4302 . . . . . . . . . . . . . . . . . . . . . . . . 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 759 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  ph )
54 simprll 771 . . . . . . . . . . . . . . . . . . . . . . . . 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 5902 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( G `
 k )  C_  U.
ran  G
56 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( n  =  (/)  ->  ( G `
 n )  =  ( G `  (/) ) )
5714fveq1i 5880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( G `
 (/) )  =  ( ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) ) ,  { U } )  |`  om ) `  (/) )
58 snex 4660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  { U }  e.  _V
59 fr0g 7159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( G `
 (/) )  =  { U }
6256, 61syl6eq 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  =  (/)  ->  ( G `
 n )  =  { U } )
6362sseq1d 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( n  =  (/)  ->  ( ( G `  n ) 
C_  ~P U  <->  { U }  C_  ~P U ) )
64 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  =  k  ->  ( G `  n )  =  ( G `  k ) )
6564sseq1d 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( n  =  k  ->  (
( G `  n
)  C_  ~P U  <->  ( G `  k ) 
C_  ~P U ) )
66 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  =  suc  k  -> 
( G `  n
)  =  ( G `
 suc  k )
)
6766sseq1d 3492 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3993 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( U  e.  ( F `  P )  ->  U  e.  ~P U )
7068, 69syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  U  e.  ~P U
)
7170snssd 4143 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  { U }  C_  ~P U )
72 simprl 763 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( F `  x )  i^i  ~P z ) 
C_  ~P z
77 elpwi 3989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( z  e.  ~P U  -> 
z  C_  U )
7877adantl 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  z  e.  ~P U )  ->  z  C_  U )
79 sspwb 4668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3476 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  z  e.  ~P U )  ->  (
( F `  x
)  i^i  ~P z
)  C_  ~P U
)
8281ralrimivw 2841 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  z  e.  ~P U )  ->  A. x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
83 iunss 4338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  A. z  e.  ~P  U U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
86 ssralv 3526 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4569 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7163 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3499 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  -> 
( G `  suc  k )  C_  ~P U )
9796expr 619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( n  e.  om  ->  ( ph  ->  ( G `  n )  C_  ~P U ) )
100 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( G `
 n )  e. 
_V
101100elpw 3986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 33 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( n  e.  om  ->  ( G `  n
)  e.  ~P ~P U ) )
104103ralrimiv 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  A. n  e.  om  ( G `  n )  e.  ~P ~P U
)
105 ffnfv 6062 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( G : om --> ~P ~P U 
<->  ( G  Fn  om  /\ 
A. n  e.  om  ( G `  n )  e.  ~P ~P U
) )
10616, 105mpbiran 927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4386 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3476 . . . . . . . . . . . . . . . . . . . . . . . . 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 1263 . . . . . . . . . . . . . . . . . . . . . . . 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 2514 . . . . . . . . . . . . . . . . . . . . . . 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 6725 . . . . . . . . . . . . . . . . . . . . . . . . 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 6032 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( G  Fn  om  /\  suc  k  e.  om )  ->  ( G `  suc  k )  e.  ran  G )
11916, 117, 118sylancr 668 . . . . . . . . . . . . . . . . . . . . . . 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 4222 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  ( G `
 suc  k )  /\  ( G `  suc  k )  e.  ran  G )  ->  v  e.  U.
ran  G )
121115, 119, 120syl2anc 666 . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . 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 765 . . . . . . . . . . . . . . . . . . . . 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 3983 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  v  ->  ~P f  =  ~P v
)
125124ineq2d 3665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  v  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  y )  i^i  ~P v ) )
126125neeq1d 2702 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  v  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  y )  i^i  ~P v )  =/=  (/) ) )
127126rspcev 3183 . . . . . . . . . . . . . . . . . . . . 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 666 . . . . . . . . . . . . . . . . . . . 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 3079 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  S  <->  ( y  e.  X  /\  E. f  e.  U. ran  G ( ( F `  y
)  i^i  ~P f
)  =/=  (/) ) )
13039, 128, 129sylanbrc 669 . . . . . . . . . . . . . . . . . . 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 619 . . . . . . . . . . . . . . . . . 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 2834 . . . . . . . . . . . . . . . . 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 624 . . . . . . . . . . . . . . . 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 3455 . . . . . . . . . . . . . . . 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 3987 . . . . . . . . . . . . . . 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 3848 . . . . . . . . . . . . . 14  |-  ( ( t  e.  ( F `
 x )  /\  t  e.  ~P S
)  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) )
13926, 137, 138syl2anc 666 . . . . . . . . . . . . 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 2922 . . . . . . . . . . . 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 619 . . . . . . . . . . 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 1769 . . . . . . . . . 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 2919 . . . . . . . 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 2916 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  ( E. f  e.  U. ran  G ( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) )
147146expimpd 607 . . . . 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 2838 . . 3  |-  ( ph  ->  A. x  e.  S  ( ( F `  x )  i^i  ~P S )  =/=  (/) )
150 pweq 3983 . . . . . . 7  |-  ( o  =  S  ->  ~P o  =  ~P S
)
151150ineq2d 3665 . . . . . 6  |-  ( o  =  S  ->  (
( F `  x
)  i^i  ~P o
)  =  ( ( F `  x )  i^i  ~P S ) )
152151neeq1d 2702 . . . . 5  |-  ( o  =  S  ->  (
( ( F `  x )  i^i  ~P o )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
153152raleqbi1dv 3034 . . . 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 3232 . . 3  |-  ( S  e.  J  <->  ( S  e.  ~P X  /\  A. x  e.  S  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) )
1567, 149, 155sylanbrc 669 . 2  |-  ( ph  ->  S  e.  J )
157 neibastop2.p . . 3  |-  ( ph  ->  P  e.  X )
158 snidg 4023 . . . . . 6  |-  ( U  e.  ( F `  P )  ->  U  e.  { U } )
15968, 158syl 17 . . . . 5  |-  ( ph  ->  U  e.  { U } )
160 peano1 6724 . . . . . . 7  |-  (/)  e.  om
161 fnfvelrn 6032 . . . . . . 7  |-  ( ( G  Fn  om  /\  (/) 
e.  om )  ->  ( G `  (/) )  e. 
ran  G )
16216, 160, 161mp2an 677 . . . . . 6  |-  ( G `
 (/) )  e.  ran  G
16361, 162eqeltrri 2508 . . . . 5  |-  { U }  e.  ran  G
164 elunii 4222 . . . . 5  |-  ( ( U  e.  { U }  /\  { U }  e.  ran  G )  ->  U  e.  U. ran  G
)
165159, 163, 164sylancl 667 . . . 4  |-  ( ph  ->  U  e.  U. ran  G )
166 inelcm 3848 . . . . 5  |-  ( ( U  e.  ( F `
 P )  /\  U  e.  ~P U
)  ->  ( ( F `  P )  i^i  ~P U )  =/=  (/) )
16768, 70, 166syl2anc 666 . . . 4  |-  ( ph  ->  ( ( F `  P )  i^i  ~P U )  =/=  (/) )
168 pweq 3983 . . . . . . 7  |-  ( f  =  U  ->  ~P f  =  ~P U
)
169168ineq2d 3665 . . . . . 6  |-  ( f  =  U  ->  (
( F `  P
)  i^i  ~P f
)  =  ( ( F `  P )  i^i  ~P U ) )
170169neeq1d 2702 . . . . 5  |-  ( f  =  U  ->  (
( ( F `  P )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P U )  =/=  (/) ) )
171170rspcev 3183 . . . 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 666 . . 3  |-  ( ph  ->  E. f  e.  U. ran  G ( ( F `
 P )  i^i 
~P f )  =/=  (/) )
173 fveq2 5879 . . . . . . 7  |-  ( y  =  P  ->  ( F `  y )  =  ( F `  P ) )
174173ineq1d 3664 . . . . . 6  |-  ( y  =  P  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  P )  i^i  ~P f ) )
175174neeq1d 2702 . . . . 5  |-  ( y  =  P  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P f )  =/=  (/) ) )
176175rexbidv 2940 . . . 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 3232 . . 3  |-  ( P  e.  S  <->  ( P  e.  X  /\  E. f  e.  U. ran  G ( ( F `  P
)  i^i  ~P f
)  =/=  (/) ) )
178157, 172, 177sylanbrc 669 . 2  |-  ( ph  ->  P  e.  S )
179 eluni2 4221 . . . . . . 7  |-  ( f  e.  U. ran  G  <->  E. z  e.  ran  G  f  e.  z )
180 eleq2 2496 . . . . . . . . . 10  |-  ( z  =  ( G `  k )  ->  (
f  e.  z  <->  f  e.  ( G `  k ) ) )
181180rexrn 6037 . . . . . . . . 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 6035 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  ( G `  k )  e.  ~P ~P U )
185184elpwid 3990 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  ( G `  k )  C_ 
~P U )
186185sselda 3465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  f  e.  ~P U )
187186adantrr 722 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  e.  ~P U )
188187elpwid 3990 . . . . . . . . . . . 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 735 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  U  C_  N )
191188, 190sstrd 3475 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  C_  N )
192 n0 3772 . . . . . . . . . . . . 13  |-  ( ( ( F `  y
)  i^i  ~P f
)  =/=  (/)  <->  E. v 
v  e.  ( ( F `  y )  i^i  ~P f ) )
193 elin 3650 . . . . . . . . . . . . . . 15  |-  ( v  e.  ( ( F `
 y )  i^i 
~P f )  <->  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) )
194 simprrr 774 . . . . . . . . . . . . . . . . . 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 3990 . . . . . . . . . . . . . . . . 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 768 . . . . . . . . . . . . . . . . . 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 619 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  X )  ->  (
v  e.  ( F `
 x )  ->  x  e.  v )
)
199198ralrimiva 2840 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. x  e.  X  ( v  e.  ( F `  x )  ->  x  e.  v ) )
200199ad3antrrr 735 . . . . . . . . . . . . . . . . . 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 773 . . . . . . . . . . . . . . . . . 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 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
203202eleq2d 2493 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  (
v  e.  ( F `
 x )  <->  v  e.  ( F `  y ) ) )
204 elequ1 1872 . . . . . . . . . . . . . . . . . . . 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 3179 . . . . . . . . . . . . . . . . . 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 64 . . . . . . . . . . . . . . . . 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 3466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  y  e.  f )
209208expr 619 . . . . . . . . . . . . . . 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 1769 . . . . . . . . . . . . 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 624 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  y  e.  f )
214191, 213sseldd 3466 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  y  e.  N )
215214exp32 609 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  (
f  e.  ( G `
 k )  -> 
( ( ( F `
 y )  i^i 
~P f )  =/=  (/)  ->  y  e.  N
) ) )
216215rexlimdva 2918 . . . . . . . 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 2916 . . . . 5  |-  ( (
ph  /\  y  e.  X )  ->  ( E. f  e.  U. ran  G ( ( F `  y )  i^i  ~P f )  =/=  (/)  ->  y  e.  N ) )
2202193impia 1203 . . . 4  |-  ( (
ph  /\  y  e.  X  /\  E. f  e. 
U. ran  G (
( F `  y
)  i^i  ~P f
)  =/=  (/) )  -> 
y  e.  N )
221220rabssdv 3542 . . 3  |-  ( ph  ->  { y  e.  X  |  E. f  e.  U. ran  G ( ( F `
 y )  i^i 
~P f )  =/=  (/) }  C_  N )
2221, 221syl5eqss 3509 . 2  |-  ( ph  ->  S  C_  N )
223 eleq2 2496 . . . 4  |-  ( u  =  S  ->  ( P  e.  u  <->  P  e.  S ) )
224 sseq1 3486 . . . 4  |-  ( u  =  S  ->  (
u  C_  N  <->  S  C_  N
) )
225223, 224anbi12d 716 . . 3  |-  ( u  =  S  ->  (
( P  e.  u  /\  u  C_  N )  <-> 
( P  e.  S  /\  S  C_  N ) ) )
226225rspcev 3183 . 2  |-  ( ( S  e.  J  /\  ( P  e.  S  /\  S  C_  N ) )  ->  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) )
227156, 178, 222, 226syl12anc 1263 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 983    = wceq 1438   E.wex 1660    e. wcel 1869    =/= wne 2619   A.wral 2776   E.wrex 2777   {crab 2780   _Vcvv 3082    \ cdif 3434    i^i cin 3436    C_ wss 3437   (/)c0 3762   ~Pcpw 3980   {csn 3997   U.cuni 4217   U_ciun 4297    |-> cmpt 4480   ran crn 4852    |` cres 4853   suc csuc 5442    Fn wfn 5594   -->wf 5595   ` cfv 5599   omcom 6704   reccrdg 7133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658  ax-un 6595
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 984  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-reu 2783  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-pss 3453  df-nul 3763  df-if 3911  df-pw 3982  df-sn 3998  df-pr 4000  df-tp 4002  df-op 4004  df-uni 4218  df-iun 4299  df-br 4422  df-opab 4481  df-mpt 4482  df-tr 4517  df-eprel 4762  df-id 4766  df-po 4772  df-so 4773  df-fr 4810  df-we 4812  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-pred 5397  df-ord 5443  df-on 5444  df-lim 5445  df-suc 5446  df-iota 5563  df-fun 5601  df-fn 5602  df-f 5603  df-f1 5604  df-fo 5605  df-f1o 5606  df-fv 5607  df-om 6705  df-wrecs 7034  df-recs 7096  df-rdg 7134
This theorem is referenced by:  neibastop2  31016
  Copyright terms: Public domain W3C validator