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

Theorem neibastop2lem 26320
Description: Lemma for neibastop2 26321. (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 3260 . . . . 5  |-  { y  e.  X  |  E. f  e.  U. ran  G
( ( F `  y )  i^i  ~P f )  =/=  (/) }  C_  X
31, 2eqsstri 3210 . . . 4  |-  S  C_  X
4 neibastop1.1 . . . . 5  |-  ( ph  ->  X  e.  V )
5 elpw2g 4176 . . . . 5  |-  ( X  e.  V  ->  ( S  e.  ~P X  <->  S 
C_  X ) )
64, 5syl 15 . . . 4  |-  ( ph  ->  ( S  e.  ~P X 
<->  S  C_  X )
)
73, 6mpbiri 224 . . 3  |-  ( ph  ->  S  e.  ~P X
)
8 fveq2 5527 . . . . . . . . 9  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
98ineq1d 3371 . . . . . . . 8  |-  ( y  =  x  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  x )  i^i  ~P f ) )
109neeq1d 2461 . . . . . . 7  |-  ( y  =  x  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P f )  =/=  (/) ) )
1110rexbidv 2566 . . . . . 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 2927 . . . . 5  |-  ( x  e.  S  <->  ( x  e.  X  /\  E. f  e.  U. ran  G ( ( F `  x
)  i^i  ~P f
)  =/=  (/) ) )
13 frfnom 6449 . . . . . . . . . 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 5340 . . . . . . . . . 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 200 . . . . . . . . 9  |-  G  Fn  om
17 fnunirn 5780 . . . . . . . . 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 3466 . . . . . . . . . . 11  |-  ( ( ( F `  x
)  i^i  ~P f
)  =/=  (/)  <->  E. v 
v  e.  ( ( F `  x )  i^i  ~P f ) )
20 inss1 3391 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  x )  i^i  ~P f ) 
C_  ( F `  x )
2120sseli 3178 . . . . . . . . . . . . . . . 16  |-  ( v  e.  ( ( F `
 x )  i^i 
~P f )  -> 
v  e.  ( F `
 x ) )
22 neibastop1.6 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  E. t  e.  ( F `  x ) A. y  e.  t 
( ( F `  y )  i^i  ~P v )  =/=  (/) )
2322anassrs 629 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 460 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 696 . . . . . . . . . . . . . 14  |-  ( ( ( 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 732 . . . . . . . . . . . . . . . . 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 )  =/=  (/) ) )  ->  t  e.  ( F `  x
) )
27 fvssunirn 5553 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( F `
 x )  C_  U.
ran  F
28 neibastop1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  F : X --> ( ~P ~P X  \  { (/)
} ) )
29 frn 5397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( F : X --> ( ~P ~P X  \  { (/)
} )  ->  ran  F 
C_  ( ~P ~P X  \  { (/) } ) )
3028, 29syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ran  F  C_  ( ~P ~P X  \  { (/)
} ) )
31 difss 3305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ~P ~P X  \  { (/)
} )  C_  ~P ~P X
3230, 31syl6ss 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ran  F  C_  ~P ~P X )
33 sspwuni 3989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ran 
F  C_  ~P ~P X 
<-> 
U. ran  F  C_  ~P X )
3432, 33sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  U. ran  F  C_  ~P X )
3534ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 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 )
3627, 35syl5ss 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
( F `  x
)  C_  ~P X
)
3736sselda 3182 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 )
38 elpwi 3635 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  e.  ~P X  -> 
t  C_  X )
3937, 38syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 )
4039sselda 3182 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 )
4140adantrr 697 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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
)
42 simprlr 739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
f  e.  ( G `
 k ) )
43 rspe 2606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  e.  X  /\  v  e.  ( ( F `  x )  i^i  ~P f ) )  ->  E. x  e.  X  v  e.  ( ( F `  x )  i^i  ~P f ) )
4443ad2ant2l 726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 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 ) )
45 eliun 3911 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( v  e.  U_ x  e.  X  ( ( F `
 x )  i^i 
~P z )  <->  E. x  e.  X  v  e.  ( ( F `  x )  i^i  ~P z ) )
46 pweq 3630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  f  ->  ~P z  =  ~P f
)
4746ineq2d 3372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  f  ->  (
( F `  x
)  i^i  ~P z
)  =  ( ( F `  x )  i^i  ~P f ) )
4847eleq2d 2352 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  f  ->  (
v  e.  ( ( F `  x )  i^i  ~P z )  <-> 
v  e.  ( ( F `  x )  i^i  ~P f ) ) )
4948rexbidv 2566 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( 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 ) ) )
5045, 49syl5bb 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 ) ) )
5150rspcev 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 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 ) )
5242, 44, 51syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 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 ) )
53 eliun 3911 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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
) )
5452, 53sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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 ) )
55 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  ph )
56 simprll 738 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
k  e.  om )
57 fvssunirn 5553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( G `
 k )  C_  U.
ran  G
58 fveq2 5527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( n  =  (/)  ->  ( G `
 n )  =  ( G `  (/) ) )
5914fveq1i 5528 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( G `
 (/) )  =  ( ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) ) ,  { U } )  |`  om ) `  (/) )
60 snex 4218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  { U }  e.  _V
61 fr0g 6450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( { U }  e.  _V  ->  ( ( rec (
( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) ) ,  { U } )  |`  om ) `  (/) )  =  { U } )
6260, 61ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  ( ( F `
 x )  i^i 
~P z ) ) ,  { U }
)  |`  om ) `  (/) )  =  { U }
6359, 62eqtri 2305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( G `
 (/) )  =  { U }
6458, 63syl6eq 2333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( n  =  (/)  ->  ( G `
 n )  =  { U } )
6564sseq1d 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( n  =  (/)  ->  ( ( G `  n ) 
C_  ~P U  <->  { U }  C_  ~P U ) )
66 fveq2 5527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( n  =  k  ->  ( G `  n )  =  ( G `  k ) )
6766sseq1d 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( n  =  k  ->  (
( G `  n
)  C_  ~P U  <->  ( G `  k ) 
C_  ~P U ) )
68 fveq2 5527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( n  =  suc  k  -> 
( G `  n
)  =  ( G `
 suc  k )
)
6968sseq1d 3207 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( n  =  suc  k  -> 
( ( G `  n )  C_  ~P U 
<->  ( G `  suc  k )  C_  ~P U ) )
70 neibastop2.f . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ph  ->  U  e.  ( F `
 P ) )
71 pwidg 3639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( U  e.  ( F `  P )  ->  U  e.  ~P U )
7270, 71syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  U  e.  ~P U
)
7372snssd 3762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  { U }  C_  ~P U )
74 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  -> 
k  e.  om )
75 inss2 3392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( F `  x )  i^i  ~P z ) 
C_  ~P z
76 elpwi 3635 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( z  e.  ~P U  -> 
z  C_  U )
7776adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  z  e.  ~P U )  ->  z  C_  U )
78 sspwb 4225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( z 
C_  U  <->  ~P z  C_ 
~P U )
7977, 78sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  z  e.  ~P U )  ->  ~P z  C_  ~P U )
8075, 79syl5ss 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  z  e.  ~P U )  ->  (
( F `  x
)  i^i  ~P z
)  C_  ~P U
)
8180ralrimivw 2629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  z  e.  ~P U )  ->  A. x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
82 iunss 3945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( 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
)
8381, 82sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  z  e.  ~P U )  ->  U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
8483ralrimiva 2628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ph  ->  A. z  e.  ~P  U U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
85 ssralv 3239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ( 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 ) )
8685adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( 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 ) )
8784, 86mpan9 455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
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 )
88 iunss 3945 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( 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 )
8987, 88sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
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 )
9070adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  ->  U  e.  ( F `  P ) )
91 pwexg 4196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( U  e.  ( F `  P )  ->  ~P U  e.  _V )
9290, 91syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  ->  ~P U  e.  _V )
93 ssexg 4162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
U_ z  e.  ( G `  k )
U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U  /\  ~P U  e. 
_V )  ->  U_ z  e.  ( G `  k
) U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  e.  _V )
9489, 92, 93syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
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 )
95 iuneq1 3920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( 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 ) )
96 iuneq1 3920 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( 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 ) )
9714, 95, 96frsucmpt2 6454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( 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 ) )
9874, 94, 97syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
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 ) )
9998, 89eqsstrd 3214 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  -> 
( G `  suc  k )  C_  ~P U )
10099expr 598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  k  e.  om )  ->  ( ( G `  k )  C_ 
~P U  ->  ( G `  suc  k ) 
C_  ~P U ) )
101100expcom 424 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( k  e.  om  ->  ( ph  ->  ( ( G `
 k )  C_  ~P U  ->  ( G `
 suc  k )  C_ 
~P U ) ) )
10265, 67, 69, 73, 101finds2 4686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( n  e.  om  ->  ( ph  ->  ( G `  n )  C_  ~P U ) )
103 fvex 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( G `
 n )  e. 
_V
104103elpw 3633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( G `  n )  e.  ~P ~P U  <->  ( G `  n ) 
C_  ~P U )
105102, 104syl6ibr 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( n  e.  om  ->  ( ph  ->  ( G `  n )  e.  ~P ~P U ) )
106105com12 27 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( n  e.  om  ->  ( G `  n
)  e.  ~P ~P U ) )
107106ralrimiv 2627 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A. n  e.  om  ( G `  n )  e.  ~P ~P U
)
108 ffnfv 5687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( G : om --> ~P ~P U 
<->  ( G  Fn  om  /\ 
A. n  e.  om  ( G `  n )  e.  ~P ~P U
) )
10916, 108mpbiran 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( G : om --> ~P ~P U 
<-> 
A. n  e.  om  ( G `  n )  e.  ~P ~P U
)
110107, 109sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  G : om --> ~P ~P U )
111 frn 5397 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( G : om --> ~P ~P U  ->  ran  G  C_  ~P ~P U )
112110, 111syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ran  G  C_  ~P ~P U )
113 sspwuni 3989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ran 
G  C_  ~P ~P U 
<-> 
U. ran  G  C_  ~P U )
114112, 113sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  U. ran  G  C_  ~P U )
115114ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 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 )
11657, 115syl5ss 3192 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
( G `  k
)  C_  ~P U
)
11755, 56, 116, 98syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 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 ) )
11854, 117eleqtrrd 2362 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
v  e.  ( G `
 suc  k )
)
119 peano2 4678 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  e.  om  ->  suc  k  e.  om )
12056, 119syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  ->  suc  k  e.  om )
121 fnfvelrn 5664 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( G  Fn  om  /\  suc  k  e.  om )  ->  ( G `  suc  k )  e.  ran  G )
12216, 120, 121sylancr 644 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 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 )
123 elunii 3834 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( v  e.  ( G `
 suc  k )  /\  ( G `  suc  k )  e.  ran  G )  ->  v  e.  U.
ran  G )
124118, 122, 123syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  x  e.  X )  /\  (
( k  e.  om  /\  f  e.  ( G `
 k ) )  /\  v  e.  ( ( F `  x
)  i^i  ~P f
) ) )  -> 
v  e.  U. ran  G )
125124ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 )
126 simprr 733 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 )  =/=  (/) )
127 pweq 3630 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  =  v  ->  ~P f  =  ~P v
)
128127ineq2d 3372 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  =  v  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  y )  i^i  ~P v ) )
129128neeq1d 2461 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  v  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  y )  i^i  ~P v )  =/=  (/) ) )
130129rspcev 2886 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( v  e.  U. ran  G  /\  ( ( F `
 y )  i^i 
~P v )  =/=  (/) )  ->  E. f  e.  U. ran  G ( ( F `  y
)  i^i  ~P f
)  =/=  (/) )
131125, 126, 130syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 )  =/=  (/) )
1321rabeq2i 2787 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  S  <->  ( y  e.  X  /\  E. f  e.  U. ran  G ( ( F `  y
)  i^i  ~P f
)  =/=  (/) ) )
13341, 131, 132sylanbrc 645 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( 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
)
134133expr 598 . . . . . . . . . . . . . . . . . . . . 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 )  =/=  (/)  ->  y  e.  S ) )
135134ralimdva 2623 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) )
136135impr 602 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( 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 )
137 dfss3 3172 . . . . . . . . . . . . . . . . . . 19  |-  ( t 
C_  S  <->  A. y  e.  t  y  e.  S )
138136, 137sylibr 203 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( 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 )
139 vex 2793 . . . . . . . . . . . . . . . . . . 19  |-  t  e. 
_V
140139elpw 3633 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  ~P S  <->  t  C_  S )
141138, 140sylibr 203 . . . . . . . . . . . . . . . . 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 )  =/=  (/) ) )  ->  t  e.  ~P S )
142 inelcm 3511 . . . . . . . . . . . . . . . . 17  |-  ( ( t  e.  ( F `
 x )  /\  t  e.  ~P S
)  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) )
14326, 141, 142syl2anc 642 . . . . . . . . . . . . . . . 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 )  =/=  (/) ) )  ->  (
( F `  x
)  i^i  ~P S
)  =/=  (/) )
144143expr 598 . . . . . . . . . . . . . . 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
)  =/=  (/)  ->  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) )
145144rexlimdva 2669 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )  =/=  (/)  ->  ( ( F `
 x )  i^i 
~P S )  =/=  (/) ) )
14625, 145mpd 14 . . . . . . . . . . . . 13  |-  ( ( ( 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 )  =/=  (/) )
147146expr 598 . . . . . . . . . . . 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
)  =/=  (/) ) )
148147exlimdv 1666 . . . . . . . . . . 11  |-  ( ( ( 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 )  =/=  (/) ) )
14919, 148syl5bi 208 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  X )  /\  (
k  e.  om  /\  f  e.  ( G `  k ) ) )  ->  ( ( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
150149expr 598 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  X )  /\  k  e.  om )  ->  (
f  e.  ( G `
 k )  -> 
( ( ( F `
 x )  i^i 
~P f )  =/=  (/)  ->  ( ( F `
 x )  i^i 
~P S )  =/=  (/) ) ) )
151150rexlimdva 2669 . . . . . . . 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
)  =/=  (/) ) ) )
15218, 151syl5bi 208 . . . . . . 7  |-  ( (
ph  /\  x  e.  X )  ->  (
f  e.  U. ran  G  ->  ( ( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) ) )
153152rexlimdv 2668 . . . . . 6  |-  ( (
ph  /\  x  e.  X )  ->  ( E. f  e.  U. ran  G ( ( F `  x )  i^i  ~P f )  =/=  (/)  ->  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) )
154153expimpd 586 . . . . 5  |-  ( ph  ->  ( ( x  e.  X  /\  E. f  e.  U. ran  G ( ( F `  x
)  i^i  ~P f
)  =/=  (/) )  -> 
( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
15512, 154syl5bi 208 . . . 4  |-  ( ph  ->  ( x  e.  S  ->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
156155ralrimiv 2627 . . 3  |-  ( ph  ->  A. x  e.  S  ( ( F `  x )  i^i  ~P S )  =/=  (/) )
157 pweq 3630 . . . . . . 7  |-  ( o  =  S  ->  ~P o  =  ~P S
)
158157ineq2d 3372 . . . . . 6  |-  ( o  =  S  ->  (
( F `  x
)  i^i  ~P o
)  =  ( ( F `  x )  i^i  ~P S ) )
159158neeq1d 2461 . . . . 5  |-  ( o  =  S  ->  (
( ( F `  x )  i^i  ~P o )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
160159raleqbi1dv 2746 . . . 4  |-  ( o  =  S  ->  ( A. x  e.  o 
( ( F `  x )  i^i  ~P o )  =/=  (/)  <->  A. x  e.  S  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
161 neibastop1.4 . . . 4  |-  J  =  { o  e.  ~P X  |  A. x  e.  o  ( ( F `  x )  i^i  ~P o )  =/=  (/) }
162160, 161elrab2 2927 . . 3  |-  ( S  e.  J  <->  ( S  e.  ~P X  /\  A. x  e.  S  (
( F `  x
)  i^i  ~P S
)  =/=  (/) ) )
1637, 156, 162sylanbrc 645 . 2  |-  ( ph  ->  S  e.  J )
164 neibastop2.p . . 3  |-  ( ph  ->  P  e.  X )
165 snidg 3667 . . . . . 6  |-  ( U  e.  ( F `  P )  ->  U  e.  { U } )
16670, 165syl 15 . . . . 5  |-  ( ph  ->  U  e.  { U } )
167 peano1 4677 . . . . . . 7  |-  (/)  e.  om
168 fnfvelrn 5664 . . . . . . 7  |-  ( ( G  Fn  om  /\  (/) 
e.  om )  ->  ( G `  (/) )  e. 
ran  G )
16916, 167, 168mp2an 653 . . . . . 6  |-  ( G `
 (/) )  e.  ran  G
17063, 169eqeltrri 2356 . . . . 5  |-  { U }  e.  ran  G
171 elunii 3834 . . . . 5  |-  ( ( U  e.  { U }  /\  { U }  e.  ran  G )  ->  U  e.  U. ran  G
)
172166, 170, 171sylancl 643 . . . 4  |-  ( ph  ->  U  e.  U. ran  G )
173 inelcm 3511 . . . . 5  |-  ( ( U  e.  ( F `
 P )  /\  U  e.  ~P U
)  ->  ( ( F `  P )  i^i  ~P U )  =/=  (/) )
17470, 72, 173syl2anc 642 . . . 4  |-  ( ph  ->  ( ( F `  P )  i^i  ~P U )  =/=  (/) )
175 pweq 3630 . . . . . . 7  |-  ( f  =  U  ->  ~P f  =  ~P U
)
176175ineq2d 3372 . . . . . 6  |-  ( f  =  U  ->  (
( F `  P
)  i^i  ~P f
)  =  ( ( F `  P )  i^i  ~P U ) )
177176neeq1d 2461 . . . . 5  |-  ( f  =  U  ->  (
( ( F `  P )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P U )  =/=  (/) ) )
178177rspcev 2886 . . . 4  |-  ( ( U  e.  U. ran  G  /\  ( ( F `
 P )  i^i 
~P U )  =/=  (/) )  ->  E. f  e.  U. ran  G ( ( F `  P
)  i^i  ~P f
)  =/=  (/) )
179172, 174, 178syl2anc 642 . . 3  |-  ( ph  ->  E. f  e.  U. ran  G ( ( F `
 P )  i^i 
~P f )  =/=  (/) )
180 fveq2 5527 . . . . . . 7  |-  ( y  =  P  ->  ( F `  y )  =  ( F `  P ) )
181180ineq1d 3371 . . . . . 6  |-  ( y  =  P  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  P )  i^i  ~P f ) )
182181neeq1d 2461 . . . . 5  |-  ( y  =  P  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P f )  =/=  (/) ) )
183182rexbidv 2566 . . . 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
)  =/=  (/) ) )
184183, 1elrab2 2927 . . 3  |-  ( P  e.  S  <->  ( P  e.  X  /\  E. f  e.  U. ran  G ( ( F `  P
)  i^i  ~P f
)  =/=  (/) ) )
185164, 179, 184sylanbrc 645 . 2  |-  ( ph  ->  P  e.  S )
186 eluni2 3833 . . . . . . 7  |-  ( f  e.  U. ran  G  <->  E. z  e.  ran  G  f  e.  z )
187 eleq2 2346 . . . . . . . . . 10  |-  ( z  =  ( G `  k )  ->  (
f  e.  z  <->  f  e.  ( G `  k ) ) )
188187rexrn 5669 . . . . . . . . 9  |-  ( G  Fn  om  ->  ( E. z  e.  ran  G  f  e.  z  <->  E. k  e.  om  f  e.  ( G `  k ) ) )
18916, 188ax-mp 8 . . . . . . . 8  |-  ( E. z  e.  ran  G  f  e.  z  <->  E. k  e.  om  f  e.  ( G `  k ) )
190110adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  X )  ->  G : om --> ~P ~P U
)
191 ffvelrn 5665 . . . . . . . . . . . . . . . . 17  |-  ( ( G : om --> ~P ~P U  /\  k  e.  om )  ->  ( G `  k )  e.  ~P ~P U )
192190, 191sylan 457 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  ( G `  k )  e.  ~P ~P U )
193 elpwi 3635 . . . . . . . . . . . . . . . 16  |-  ( ( G `  k )  e.  ~P ~P U  ->  ( G `  k
)  C_  ~P U
)
194192, 193syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  ( G `  k )  C_ 
~P U )
195194sselda 3182 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  f  e.  ~P U )
196195adantrr 697 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  e.  ~P U )
197 elpwi 3635 . . . . . . . . . . . . 13  |-  ( f  e.  ~P U  -> 
f  C_  U )
198196, 197syl 15 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  C_  U )
199 neibastop2.u . . . . . . . . . . . . 13  |-  ( ph  ->  U  C_  N )
200199ad3antrrr 710 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  U  C_  N )
201198, 200sstrd 3191 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  C_  N )
202 n0 3466 . . . . . . . . . . . . 13  |-  ( ( ( F `  y
)  i^i  ~P f
)  =/=  (/)  <->  E. v 
v  e.  ( ( F `  y )  i^i  ~P f ) )
203 elin 3360 . . . . . . . . . . . . . . 15  |-  ( v  e.  ( ( F `
 y )  i^i 
~P f )  <->  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) )
204 simprrr 741 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  v  e.  ~P f )
205 elpwi 3635 . . . . . . . . . . . . . . . . . 18  |-  ( v  e.  ~P f  -> 
v  C_  f )
206204, 205syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  v  C_  f
)
207 simpllr 735 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  y  e.  X
)
208 neibastop1.5 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( x  e.  X  /\  v  e.  ( F `  x
) ) )  ->  x  e.  v )
209208expr 598 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  x  e.  X )  ->  (
v  e.  ( F `
 x )  ->  x  e.  v )
)
210209ralrimiva 2628 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A. x  e.  X  ( v  e.  ( F `  x )  ->  x  e.  v ) )
211210ad3antrrr 710 . . . . . . . . . . . . . . . . . 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 ) )
212 simprrl 740 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  v  e.  ( F `  y ) )
213 fveq2 5527 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
214213eleq2d 2352 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  (
v  e.  ( F `
 x )  <->  v  e.  ( F `  y ) ) )
215 elequ1 1689 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  (
x  e.  v  <->  y  e.  v ) )
216214, 215imbi12d 311 . . . . . . . . . . . . . . . . . . 19  |-  ( x  =  y  ->  (
( v  e.  ( F `  x )  ->  x  e.  v )  <->  ( v  e.  ( F `  y
)  ->  y  e.  v ) ) )
217216rspcv 2882 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  X  ->  ( A. x  e.  X  ( v  e.  ( F `  x )  ->  x  e.  v )  ->  ( v  e.  ( F `  y
)  ->  y  e.  v ) ) )
218207, 211, 212, 217syl3c 57 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  y  e.  v )
219206, 218sseldd 3183 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( v  e.  ( F `  y
)  /\  v  e.  ~P f ) ) )  ->  y  e.  f )
220219expr 598 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  ( (
v  e.  ( F `
 y )  /\  v  e.  ~P f
)  ->  y  e.  f ) )
221203, 220syl5bi 208 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  ( v  e.  ( ( F `  y )  i^i  ~P f )  ->  y  e.  f ) )
222221exlimdv 1666 . . . . . . . . . . . . 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 ) )
223202, 222syl5bi 208 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  f  e.  ( G `  k ) )  ->  ( (
( F `  y
)  i^i  ~P f
)  =/=  (/)  ->  y  e.  f ) )
224223impr 602 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  y  e.  f )
225201, 224sseldd 3183 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  y  e.  N )
226225exp32 588 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  ->  (
f  e.  ( G `
 k )  -> 
( ( ( F `
 y )  i^i 
~P f )  =/=  (/)  ->  y  e.  N
) ) )
227226rexlimdva 2669 . . . . . . . 8  |-  ( (
ph  /\  y  e.  X )  ->  ( E. k  e.  om  f  e.  ( G `  k )  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  ->  y  e.  N ) ) )
228189, 227syl5bi 208 . . . . . . 7  |-  ( (
ph  /\  y  e.  X )  ->  ( E. z  e.  ran  G  f  e.  z  -> 
( ( ( F `
 y )  i^i 
~P f )  =/=  (/)  ->  y  e.  N
) ) )
229186, 228syl5bi 208 . . . . . 6  |-  ( (
ph  /\  y  e.  X )  ->  (
f  e.  U. ran  G  ->  ( ( ( F `  y )  i^i  ~P f )  =/=  (/)  ->  y  e.  N ) ) )
230229rexlimdv 2668 . . . . 5  |-  ( (
ph  /\  y  e.  X )  ->  ( E. f  e.  U. ran  G ( ( F `  y )  i^i  ~P f )  =/=  (/)  ->  y  e.  N ) )
2312303impia 1148 . . . 4  |-  ( (
ph  /\  y  e.  X  /\  E. f  e. 
U. ran  G (
( F `  y
)  i^i  ~P f
)  =/=  (/) )  -> 
y  e.  N )
232231rabssdv 3255 . . 3  |-  ( ph  ->  { y  e.  X  |  E. f  e.  U. ran  G ( ( F `
 y )  i^i 
~P f )  =/=  (/) }  C_  N )
2331, 232syl5eqss 3224 . 2  |-  ( ph  ->  S  C_  N )
234 eleq2 2346 . . . 4  |-  ( u  =  S  ->  ( P  e.  u  <->  P  e.  S ) )
235 sseq1 3201 . . . 4  |-  ( u  =  S  ->  (
u  C_  N  <->  S  C_  N
) )
236234, 235anbi12d 691 . . 3  |-  ( u  =  S  ->  (
( P  e.  u  /\  u  C_  N )  <-> 
( P  e.  S  /\  S  C_  N ) ) )
237236rspcev 2886 . 2  |-  ( ( S  e.  J  /\  ( P  e.  S  /\  S  C_  N ) )  ->  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) )
238163, 185, 233, 237syl12anc 1180 1  |-  ( ph  ->  E. u  e.  J  ( P  e.  u  /\  u  C_  N ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934   E.wex 1530    = wceq 1625    e. wcel 1686    =/= wne 2448   A.wral 2545   E.wrex 2546   {crab 2549   _Vcvv 2790    \ cdif 3151    i^i cin 3153    C_ wss 3154   (/)c0 3457   ~Pcpw 3627   {csn 3642   U.cuni 3829   U_ciun 3907    e. cmpt 4079   suc csuc 4396   omcom 4658   ran crn 4692    |` cres 4693    Fn wfn 5252   -->wf 5253   ` cfv 5257   reccrdg 6424
This theorem is referenced by:  neibastop2  26321
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-recs 6390  df-rdg 6425
  Copyright terms: Public domain W3C validator