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

Theorem neibastop2lem 26080
Description: Lemma for neibastop2 26081. (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 3371 . . . . 5  |-  { y  e.  X  |  E. f  e.  U. ran  G
( ( F `  y )  i^i  ~P f )  =/=  (/) }  C_  X
31, 2eqsstri 3321 . . . 4  |-  S  C_  X
4 neibastop1.1 . . . . 5  |-  ( ph  ->  X  e.  V )
5 elpw2g 4304 . . . . 5  |-  ( X  e.  V  ->  ( S  e.  ~P X  <->  S 
C_  X ) )
64, 5syl 16 . . . 4  |-  ( ph  ->  ( S  e.  ~P X 
<->  S  C_  X )
)
73, 6mpbiri 225 . . 3  |-  ( ph  ->  S  e.  ~P X
)
8 fveq2 5668 . . . . . . . . 9  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
98ineq1d 3484 . . . . . . . 8  |-  ( y  =  x  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  x )  i^i  ~P f ) )
109neeq1d 2563 . . . . . . 7  |-  ( y  =  x  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P f )  =/=  (/) ) )
1110rexbidv 2670 . . . . . 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 3037 . . . . 5  |-  ( x  e.  S  <->  ( x  e.  X  /\  E. f  e.  U. ran  G ( ( F `  x
)  i^i  ~P f
)  =/=  (/) ) )
13 frfnom 6628 . . . . . . . . . 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 5479 . . . . . . . . . 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 201 . . . . . . . . 9  |-  G  Fn  om
17 fnunirn 5938 . . . . . . . . 9  |-  ( G  Fn  om  ->  (
f  e.  U. ran  G  <->  E. k  e.  om  f  e.  ( G `  k ) ) )
1816, 17ax-mp 8 . . . . . . . 8  |-  ( f  e.  U. ran  G  <->  E. k  e.  om  f  e.  ( G `  k
) )
19 n0 3580 . . . . . . . . . 10  |-  ( ( ( F `  x
)  i^i  ~P f
)  =/=  (/)  <->  E. v 
v  e.  ( ( F `  x )  i^i  ~P f ) )
20 inss1 3504 . . . . . . . . . . . . . . . 16  |-  ( ( F `  x )  i^i  ~P f ) 
C_  ( F `  x )
2120sseli 3287 . . . . . . . . . . . . . . 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 630 . . . . . . . . . . . . . . 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 461 . . . . . . . . . . . . . 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 697 . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . 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 5694 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( F `
 x )  C_  U.
ran  F
28 neibastop1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  F : X --> ( ~P ~P X  \  { (/)
} ) )
29 frn 5537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( F : X --> ( ~P ~P X  \  { (/)
} )  ->  ran  F 
C_  ( ~P ~P X  \  { (/) } ) )
3028, 29syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ran  F  C_  ( ~P ~P X  \  { (/)
} ) )
3130difss2d 3420 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ran  F  C_  ~P ~P X )
32 sspwuni 4117 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ran 
F  C_  ~P ~P X 
<-> 
U. ran  F  C_  ~P X )
3331, 32sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  U. ran  F  C_  ~P X )
3433ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 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 3302 . . . . . . . . . . . . . . . . . . . . . . . 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 3291 . . . . . . . . . . . . . . . . . . . . . . 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 3751 . . . . . . . . . . . . . . . . . . . . . 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 3291 . . . . . . . . . . . . . . . . . . . . 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 698 . . . . . . . . . . . . . . . . . . . 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 740 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2710 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 727 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4039 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3745 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( z  =  f  ->  ~P z  =  ~P f
)
4544ineq2d 3485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( z  =  f  ->  (
( F `  x
)  i^i  ~P z
)  =  ( ( F `  x )  i^i  ~P f ) )
4645eleq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  f  ->  (
v  e.  ( ( F `  x )  i^i  ~P z )  <-> 
v  e.  ( ( F `  x )  i^i  ~P f ) ) )
4746rexbidv 2670 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 249 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2995 . . . . . . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . . . . . . 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 4039 . . . . . . . . . . . . . . . . . . . . . . . . 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 204 . . . . . . . . . . . . . . . . . . . . . . . 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 731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  ph )
54 simprll 739 . . . . . . . . . . . . . . . . . . . . . . . . 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 5694 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( G `
 k )  C_  U.
ran  G
56 fveq2 5668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( n  =  (/)  ->  ( G `
 n )  =  ( G `  (/) ) )
5714fveq1i 5669 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( G `
 (/) )  =  ( ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) ) ,  { U } )  |`  om ) `  (/) )
58 snex 4346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  { U }  e.  _V
59 fr0g 6629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  ( ( F `
 x )  i^i 
~P z ) ) ,  { U }
)  |`  om ) `  (/) )  =  { U }
6157, 60eqtri 2407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( G `
 (/) )  =  { U }
6256, 61syl6eq 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  =  (/)  ->  ( G `
 n )  =  { U } )
6362sseq1d 3318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( n  =  (/)  ->  ( ( G `  n ) 
C_  ~P U  <->  { U }  C_  ~P U ) )
64 fveq2 5668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  =  k  ->  ( G `  n )  =  ( G `  k ) )
6564sseq1d 3318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( n  =  k  ->  (
( G `  n
)  C_  ~P U  <->  ( G `  k ) 
C_  ~P U ) )
66 fveq2 5668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  =  suc  k  -> 
( G `  n
)  =  ( G `
 suc  k )
)
6766sseq1d 3318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( U  e.  ( F `  P )  ->  U  e.  ~P U )
7068, 69syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  U  e.  ~P U
)
7170snssd 3886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  { U }  C_  ~P U )
72 simprl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  -> 
k  e.  om )
7368adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  ->  U  e.  ( F `  P ) )
74 pwexg 4324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( U  e.  ( F `  P )  ->  ~P U  e.  _V )
7573, 74syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  ->  ~P U  e.  _V )
76 inss2 3505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( F `  x )  i^i  ~P z ) 
C_  ~P z
77 elpwi 3750 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( z  e.  ~P U  -> 
z  C_  U )
7877adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  z  e.  ~P U )  ->  z  C_  U )
79 sspwb 4354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( z 
C_  U  <->  ~P z  C_ 
~P U )
8078, 79sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  z  e.  ~P U )  ->  ~P z  C_  ~P U )
8176, 80syl5ss 3302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  z  e.  ~P U )  ->  (
( F `  x
)  i^i  ~P z
)  C_  ~P U
)
8281ralrimivw 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  z  e.  ~P U )  ->  A. x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
83 iunss 4073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  z  e.  ~P U )  ->  U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
8584ralrimiva 2732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  A. z  e.  ~P  U U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
86 ssralv 3350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3325 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  -> 
( G `  suc  k )  C_  ~P U )
9796expr 599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  k  e.  om )  ->  ( ( G `  k )  C_ 
~P U  ->  ( G `  suc  k ) 
C_  ~P U ) )
9897expcom 425 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  e.  om  ->  ( ph  ->  ( ( G `
 k )  C_  ~P U  ->  ( G `
 suc  k )  C_ 
~P U ) ) )
9963, 65, 67, 71, 98finds2 4813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( n  e.  om  ->  ( ph  ->  ( G `  n )  C_  ~P U ) )
100 fvex 5682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( G `
 n )  e. 
_V
101100elpw 3748 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( G `  n )  e.  ~P ~P U  <->  ( G `  n ) 
C_  ~P U )
10299, 101syl6ibr 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( n  e.  om  ->  ( ph  ->  ( G `  n )  e.  ~P ~P U ) )
103102com12 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( n  e.  om  ->  ( G `  n
)  e.  ~P ~P U ) )
104103ralrimiv 2731 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  A. n  e.  om  ( G `  n )  e.  ~P ~P U
)
105 ffnfv 5833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( G : om --> ~P ~P U 
<->  ( G  Fn  om  /\ 
A. n  e.  om  ( G `  n )  e.  ~P ~P U
) )
10616, 105mpbiran 885 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( G : om --> ~P ~P U 
<-> 
A. n  e.  om  ( G `  n )  e.  ~P ~P U
)
107104, 106sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  G : om --> ~P ~P U )
108 frn 5537 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( G : om --> ~P ~P U  ->  ran  G  C_  ~P ~P U )
109107, 108syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ran  G  C_  ~P ~P U )
110 sspwuni 4117 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ran 
G  C_  ~P ~P U 
<-> 
U. ran  G  C_  ~P U )
111109, 110sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  U. ran  G  C_  ~P U )
112111ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3302 . . . . . . . . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . . . . . . 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 4805 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  om  ->  suc  k  e.  om )
11754, 116syl 16 . . . . . . . . . . . . . . . . . . . . . . . 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 5806 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( G  Fn  om  /\  suc  k  e.  om )  ->  ( G `  suc  k )  e.  ran  G )
11916, 117, 118sylancr 645 . . . . . . . . . . . . . . . . . . . . . . 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 3962 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( v  e.  ( G `
 suc  k )  /\  ( G `  suc  k )  e.  ran  G )  ->  v  e.  U.
ran  G )
121115, 119, 120syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . . . . 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 3745 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  v  ->  ~P f  =  ~P v
)
125124ineq2d 3485 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( f  =  v  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  y )  i^i  ~P v ) )
126125neeq1d 2563 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( f  =  v  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  y )  i^i  ~P v )  =/=  (/) ) )
127126rspcev 2995 . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . 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 2896 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  S  <->  ( y  e.  X  /\  E. f  e.  U. ran  G ( ( F `  y
)  i^i  ~P f
)  =/=  (/) ) )
13039, 128, 129sylanbrc 646 . . . . . . . . . . . . . . . . . . 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 599 . . . . . . . . . . . . . . . . . 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 2727 . . . . . . . . . . . . . . . . 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 603 . . . . . . . . . . . . . . . 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 3281 . . . . . . . . . . . . . . . 16  |-  ( t 
C_  S  <->  A. y  e.  t  y  e.  S )
135133, 134sylibr 204 . . . . . . . . . . . . . . 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 vex 2902 . . . . . . . . . . . . . . . 16  |-  t  e. 
_V
137136elpw 3748 . . . . . . . . . . . . . . 15  |-  ( t  e.  ~P S  <->  t  C_  S )
138135, 137sylibr 204 . . . . . . . . . . . . . 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 )
139 inelcm 3625 . . . . . . . . . . . . . 14  |-  ( ( t  e.  ( F `
 x )  /\  t  e.  ~P S
)  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) )
14026, 138, 139syl2anc 643 . . . . . . . . . . . . 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
)  =/=  (/) )
14125, 140rexlimddv 2777 . . . . . . . . . . . 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 )  =/=  (/) )
142141expr 599 . . . . . . . . . . 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
)  =/=  (/) ) )
143142exlimdv 1643 . . . . . . . . . 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 )  =/=  (/) ) )
14419, 143syl5bi 209 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  X )  /\  (
k  e.  om  /\  f  e.  ( G `  k ) ) )  ->  ( ( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
145144rexlimdvaa 2774 . . . . . . . 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
)  =/=  (/) ) ) )
14618, 145syl5bi 209 . . . . . . 7  |-  ( (
ph  /\  x  e.  X )  ->  (
f  e.  U. ran  G  ->  ( ( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) ) )
147146rexlimdv 2772 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  ( E. f  e.  U. ran  G ( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) )
148147expimpd 587 . . . . 5  |-  ( ph  ->  ( ( x  e.  X  /\  E. f  e.  U. ran  G ( ( F `  x
)  i^i  ~P f
)  =/=  (/) )  -> 
( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
14912, 148syl5bi 209 . . . 4  |-  ( ph  ->  ( x  e.  S  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
150149ralrimiv 2731 . . 3  |-  ( ph  ->  A. x  e.  S  ( ( F `  x )  i^i  ~P S )  =/=  (/) )
151 pweq 3745 . . . . . . 7  |-  ( o  =  S  ->  ~P o  =  ~P S
)
152151ineq2d 3485 . . . . . 6  |-  ( o  =  S  ->  (
( F `  x
)  i^i  ~P o
)  =  ( ( F `  x )  i^i  ~P S ) )
153152neeq1d 2563 . . . . 5  |-  ( o  =  S  ->  (
( ( F `  x )  i^i  ~P o )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
154153raleqbi1dv 2855 . . . 4  |-  ( o  =  S  ->  ( A. x  e.  o 
( ( F `  x )  i^i  ~P o )  =/=  (/)  <->  A. x  e.  S  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
155 neibastop1.4 . . . 4  |-  J  =  { o  e.  ~P X  |  A. x  e.  o  ( ( F `  x )  i^i  ~P o )  =/=  (/) }
156154, 155elrab2 3037 . . 3  |-  ( S  e.  J  <->  ( S  e.  ~P X  /\  A. x  e.  S  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) )
1577, 150, 156sylanbrc 646 . 2  |-  ( ph  ->  S  e.  J )
158 neibastop2.p . . 3  |-  ( ph  ->  P  e.  X )
159 snidg 3782 . . . . . 6  |-  ( U  e.  ( F `  P )  ->  U  e.  { U } )
16068, 159syl 16 . . . . 5  |-  ( ph  ->  U  e.  { U } )
161 peano1 4804 . . . . . . 7  |-  (/)  e.  om
162 fnfvelrn 5806 . . . . . . 7  |-  ( ( G  Fn  om  /\  (/) 
e.  om )  ->  ( G `  (/) )  e. 
ran  G )
16316, 161, 162mp2an 654 . . . . . 6  |-  ( G `
 (/) )  e.  ran  G
16461, 163eqeltrri 2458 . . . . 5  |-  { U }  e.  ran  G
165 elunii 3962 . . . . 5  |-  ( ( U  e.  { U }  /\  { U }  e.  ran  G )  ->  U  e.  U. ran  G
)
166160, 164, 165sylancl 644 . . . 4  |-  ( ph  ->  U  e.  U. ran  G )
167 inelcm 3625 . . . . 5  |-  ( ( U  e.  ( F `
 P )  /\  U  e.  ~P U
)  ->  ( ( F `  P )  i^i  ~P U )  =/=  (/) )
16868, 70, 167syl2anc 643 . . . 4  |-  ( ph  ->  ( ( F `  P )  i^i  ~P U )  =/=  (/) )
169 pweq 3745 . . . . . . 7  |-  ( f  =  U  ->  ~P f  =  ~P U
)
170169ineq2d 3485 . . . . . 6  |-  ( f  =  U  ->  (
( F `  P
)  i^i  ~P f
)  =  ( ( F `  P )  i^i  ~P U ) )
171170neeq1d 2563 . . . . 5  |-  ( f  =  U  ->  (
( ( F `  P )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P U )  =/=  (/) ) )
172171rspcev 2995 . . . 4  |-  ( ( U  e.  U. ran  G  /\  ( ( F `
 P )  i^i 
~P U )  =/=  (/) )  ->  E. f  e.  U. ran  G ( ( F `  P
)  i^i  ~P f
)  =/=  (/) )
173166, 168, 172syl2anc 643 . . 3  |-  ( ph  ->  E. f  e.  U. ran  G ( ( F `
 P )  i^i 
~P f )  =/=  (/) )
174 fveq2 5668 . . . . . . 7  |-  ( y  =  P  ->  ( F `  y )  =  ( F `  P ) )
175174ineq1d 3484 . . . . . 6  |-  ( y  =  P  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  P )  i^i  ~P f ) )
176175neeq1d 2563 . . . . 5  |-  ( y  =  P  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P f )  =/=  (/) ) )
177176rexbidv 2670 . . . 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
)  =/=  (/) ) )
178177, 1elrab2 3037 . . 3  |-  ( P  e.  S  <->  ( P  e.  X  /\  E. f  e.  U. ran  G ( ( F `  P
)  i^i  ~P f
)  =/=  (/) ) )
179158, 173, 178sylanbrc 646 . 2  |-  ( ph  ->  P  e.  S )
180 eluni2 3961 . . . . . . 7  |-  ( f  e.  U. ran  G  <->  E. z  e.  ran  G  f  e.  z )
181 eleq2 2448 . . . . . . . . . 10  |-  ( z  =  ( G `  k )  ->  (
f  e.  z  <->  f  e.  ( G `  k ) ) )
182181rexrn 5811 . . . . . . . . 9  |-  ( G  Fn  om  ->  ( E. z  e.  ran  G  f  e.  z  <->  E. k  e.  om  f  e.  ( G `  k ) ) )
18316, 182ax-mp 8 . . . . . . . 8  |-  ( E. z  e.  ran  G  f  e.  z  <->  E. k  e.  om  f  e.  ( G `  k ) )
184107adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  X )  ->  G : om --> ~P ~P U
)
185184ffvelrnda 5809 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  ( G `  k )  e.  ~P ~P U )
186185elpwid 3751 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  ( G `  k )  C_ 
~P U )
187186sselda 3291 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  f  e.  ~P U )
188187adantrr 698 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  e.  ~P U )
189188elpwid 3751 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  C_  U )
190 neibastop2.u . . . . . . . . . . . . 13  |-  ( ph  ->  U  C_  N )
191190ad3antrrr 711 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  U  C_  N )
192189, 191sstrd 3301 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  C_  N )
193 n0 3580 . . . . . . . . . . . . 13  |-  ( ( ( F `  y
)  i^i  ~P f
)  =/=  (/)  <->  E. v 
v  e.  ( ( F `  y )  i^i  ~P f ) )
194 elin 3473 . . . . . . . . . . . . . . 15  |-  ( v  e.  ( ( F `
 y )  i^i 
~P f )  <->  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) )
195 simprrr 742 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  v  e.  ~P f )
196195elpwid 3751 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  v  C_  f
)
197 simpllr 736 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  y  e.  X
)
198 neibastop1.5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  x  e.  v )
199198expr 599 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  X )  ->  (
v  e.  ( F `
 x )  ->  x  e.  v )
)
200199ralrimiva 2732 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. x  e.  X  ( v  e.  ( F `  x )  ->  x  e.  v ) )
201200ad3antrrr 711 . . . . . . . . . . . . . . . . . 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 ) )
202 simprrl 741 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  v  e.  ( F `  y ) )
203 fveq2 5668 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
204203eleq2d 2454 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  (
v  e.  ( F `
 x )  <->  v  e.  ( F `  y ) ) )
205 elequ1 1720 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  (
x  e.  v  <->  y  e.  v ) )
206204, 205imbi12d 312 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
( v  e.  ( F `  x )  ->  x  e.  v )  <->  ( v  e.  ( F `  y
)  ->  y  e.  v ) ) )
207206rspcv 2991 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  X  ->  ( A. x  e.  X  ( v  e.  ( F `  x )  ->  x  e.  v )  ->  ( v  e.  ( F `  y
)  ->  y  e.  v ) ) )
208197, 201, 202, 207syl3c 59 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  y  e.  v )
209196, 208sseldd 3292 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  y  e.  f )
210209expr 599 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  ( (
v  e.  ( F `
 y )  /\  v  e.  ~P f
)  ->  y  e.  f ) )
211194, 210syl5bi 209 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  ( v  e.  ( ( F `  y )  i^i  ~P f )  ->  y  e.  f ) )
212211exlimdv 1643 . . . . . . . . . . . . 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 ) )
213193, 212syl5bi 209 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  ( (
( F `  y
)  i^i  ~P f
)  =/=  (/)  ->  y  e.  f ) )
214213impr 603 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  y  e.  f )
215192, 214sseldd 3292 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  y  e.  N )
216215exp32 589 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  (
f  e.  ( G `
 k )  -> 
( ( ( F `
 y )  i^i 
~P f )  =/=  (/)  ->  y  e.  N
) ) )
217216rexlimdva 2773 . . . . . . . 8  |-  ( (
ph  /\  y  e.  X )  ->  ( E. k  e.  om  f  e.  ( G `  k )  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  ->  y  e.  N ) ) )
218183, 217syl5bi 209 . . . . . . 7  |-  ( (
ph  /\  y  e.  X )  ->  ( E. z  e.  ran  G  f  e.  z  -> 
( ( ( F `
 y )  i^i 
~P f )  =/=  (/)  ->  y  e.  N
) ) )
219180, 218syl5bi 209 . . . . . 6  |-  ( (
ph  /\  y  e.  X )  ->  (
f  e.  U. ran  G  ->  ( ( ( F `  y )  i^i  ~P f )  =/=  (/)  ->  y  e.  N ) ) )
220219rexlimdv 2772 . . . . 5  |-  ( (
ph  /\  y  e.  X )  ->  ( E. f  e.  U. ran  G ( ( F `  y )  i^i  ~P f )  =/=  (/)  ->  y  e.  N ) )
2212203impia 1150 . . . 4  |-  ( (
ph  /\  y  e.  X  /\  E. f  e. 
U. ran  G (
( F `  y
)  i^i  ~P f
)  =/=  (/) )  -> 
y  e.  N )
222221rabssdv 3366 . . 3  |-  ( ph  ->  { y  e.  X  |  E. f  e.  U. ran  G ( ( F `
 y )  i^i 
~P f )  =/=  (/) }  C_  N )
2231, 222syl5eqss 3335 . 2  |-  ( ph  ->  S  C_  N )
224 eleq2 2448 . . . 4  |-  ( u  =  S  ->  ( P  e.  u  <->  P  e.  S ) )
225 sseq1 3312 . . . 4  |-  ( u  =  S  ->  (
u  C_  N  <->  S  C_  N
) )
226224, 225anbi12d 692 . . 3  |-  ( u  =  S  ->  (
( P  e.  u  /\  u  C_  N )  <-> 
( P  e.  S  /\  S  C_  N ) ) )
227226rspcev 2995 . 2  |-  ( ( S  e.  J  /\  ( P  e.  S  /\  S  C_  N ) )  ->  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) )
228157, 179, 223, 227syl12anc 1182 1  |-  ( ph  ->  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    /\ w3a 936   E.wex 1547    = wceq 1649    e. wcel 1717    =/= wne 2550   A.wral 2649   E.wrex 2650   {crab 2653   _Vcvv 2899    \ cdif 3260    i^i cin 3262    C_ wss 3263   (/)c0 3571   ~Pcpw 3742   {csn 3757   U.cuni 3957   U_ciun 4035    e. cmpt 4207   suc csuc 4524   omcom 4785   ran crn 4819    |` cres 4820    Fn wfn 5389   -->wf 5390   ` cfv 5394   reccrdg 6603
This theorem is referenced by:  neibastop2  26081
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-reu 2656  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-pss 3279  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-tp 3765  df-op 3766  df-uni 3958  df-iun 4037  df-br 4154  df-opab 4208  df-mpt 4209  df-tr 4244  df-eprel 4435  df-id 4439  df-po 4444  df-so 4445  df-fr 4482  df-we 4484  df-ord 4525  df-on 4526  df-lim 4527  df-suc 4528  df-om 4786  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-recs 6569  df-rdg 6604
  Copyright terms: Public domain W3C validator