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

Theorem neibastop2lem 26412
Description: Lemma for neibastop2 26413. (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 3271 . . . . 5  |-  { y  e.  X  |  E. f  e.  U. ran  G
( ( F `  y )  i^i  ~P f )  =/=  (/) }  C_  X
31, 2eqsstri 3221 . . . 4  |-  S  C_  X
4 neibastop1.1 . . . . 5  |-  ( ph  ->  X  e.  V )
5 elpw2g 4190 . . . . 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 5541 . . . . . . . . 9  |-  ( y  =  x  ->  ( F `  y )  =  ( F `  x ) )
98ineq1d 3382 . . . . . . . 8  |-  ( y  =  x  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  x )  i^i  ~P f ) )
109neeq1d 2472 . . . . . . 7  |-  ( y  =  x  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P f )  =/=  (/) ) )
1110rexbidv 2577 . . . . . 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 2938 . . . . 5  |-  ( x  e.  S  <->  ( x  e.  X  /\  E. f  e.  U. ran  G ( ( F `  x
)  i^i  ~P f
)  =/=  (/) ) )
13 frfnom 6463 . . . . . . . . . 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 5354 . . . . . . . . . 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 5794 . . . . . . . . 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 3477 . . . . . . . . . . 11  |-  ( ( ( F `  x
)  i^i  ~P f
)  =/=  (/)  <->  E. v 
v  e.  ( ( F `  x )  i^i  ~P f ) )
20 inss1 3402 . . . . . . . . . . . . . . . . 17  |-  ( ( F `  x )  i^i  ~P f ) 
C_  ( F `  x )
2120sseli 3189 . . . . . . . . . . . . . . . 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 5567 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( F `
 x )  C_  U.
ran  F
28 neibastop1.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  F : X --> ( ~P ~P X  \  { (/)
} ) )
29 frn 5411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ~P ~P X  \  { (/)
} )  C_  ~P ~P X
3230, 31syl6ss 3204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ran  F  C_  ~P ~P X )
33 sspwuni 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3203 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3193 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3646 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3193 . . . . . . . . . . . . . . . . . . . . . . . 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 2617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3925 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( z  =  f  ->  ~P z  =  ~P f
)
4746ineq2d 3383 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( z  =  f  ->  (
( F `  x
)  i^i  ~P z
)  =  ( ( F `  x )  i^i  ~P f ) )
4847eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( z  =  f  ->  (
v  e.  ( ( F `  x )  i^i  ~P z )  <-> 
v  e.  ( ( F `  x )  i^i  ~P f ) ) )
4948rexbidv 2577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2897 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3925 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( G `
 k )  C_  U.
ran  G
58 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( n  =  (/)  ->  ( G `
 n )  =  ( G `  (/) ) )
5914fveq1i 5542 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( G `
 (/) )  =  ( ( rec ( ( a  e.  _V  |->  U_ z  e.  a  U_ x  e.  X  (
( F `  x
)  i^i  ~P z
) ) ,  { U } )  |`  om ) `  (/) )
60 snex 4232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  { U }  e.  _V
61 fr0g 6464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( G `
 (/) )  =  { U }
6458, 63syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( n  =  (/)  ->  ( G `
 n )  =  { U } )
6564sseq1d 3218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( n  =  (/)  ->  ( ( G `  n ) 
C_  ~P U  <->  { U }  C_  ~P U ) )
66 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( n  =  k  ->  ( G `  n )  =  ( G `  k ) )
6766sseq1d 3218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( n  =  k  ->  (
( G `  n
)  C_  ~P U  <->  ( G `  k ) 
C_  ~P U ) )
68 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( n  =  suc  k  -> 
( G `  n
)  =  ( G `
 suc  k )
)
6968sseq1d 3218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3650 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( U  e.  ( F `  P )  ->  U  e.  ~P U )
7270, 71syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  U  e.  ~P U
)
7372snssd 3776 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  { U }  C_  ~P U )
74 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  ( k  e.  om  /\  ( G `
 k )  C_  ~P U ) )  -> 
k  e.  om )
75 inss2 3403 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( ( F `  x )  i^i  ~P z ) 
C_  ~P z
76 elpwi 3646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  ( z  e.  ~P U  -> 
z  C_  U )
7776adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  z  e.  ~P U )  ->  z  C_  U )
78 sspwb 4239 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  z  e.  ~P U )  ->  (
( F `  x
)  i^i  ~P z
)  C_  ~P U
)
8180ralrimivw 2640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  z  e.  ~P U )  ->  A. x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
82 iunss 3959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2639 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ph  ->  A. z  e.  ~P  U U_ x  e.  X  ( ( F `  x )  i^i  ~P z )  C_  ~P U )
85 ssralv 3250 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3959 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( n  e.  om  ->  ( ph  ->  ( G `  n )  C_  ~P U ) )
103 fvex 5555 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( G `
 n )  e. 
_V
104103elpw 3644 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2638 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  A. n  e.  om  ( G `  n )  e.  ~P ~P U
)
108 ffnfv 5701 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5411 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3203 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2373 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4692 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5678 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3848 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3641 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( f  =  v  ->  ~P f  =  ~P v
)
128127ineq2d 3383 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  =  v  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  y )  i^i  ~P v ) )
129128neeq1d 2472 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( f  =  v  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  y )  i^i  ~P v )  =/=  (/) ) )
130129rspcev 2897 . . . . . . . . . . . . . . . . . . . . . . . 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 2798 . . . . . . . . . . . . . . . . . . . . . . 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 2634 . . . . . . . . . . . . . . . . . . . 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 3183 . . . . . . . . . . . . . . . . . . 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 2804 . . . . . . . . . . . . . . . . . . 19  |-  t  e. 
_V
140139elpw 3644 . . . . . . . . . . . . . . . . . 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 3522 . . . . . . . . . . . . . . . . 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 2680 . . . . . . . . . . . . . 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 1626 . . . . . . . . . . 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 2680 . . . . . . . 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 2679 . . . . . 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 2638 . . 3  |-  ( ph  ->  A. x  e.  S  ( ( F `  x )  i^i  ~P S )  =/=  (/) )
157 pweq 3641 . . . . . . 7  |-  ( o  =  S  ->  ~P o  =  ~P S
)
158157ineq2d 3383 . . . . . 6  |-  ( o  =  S  ->  (
( F `  x
)  i^i  ~P o
)  =  ( ( F `  x )  i^i  ~P S ) )
159158neeq1d 2472 . . . . 5  |-  ( o  =  S  ->  (
( ( F `  x )  i^i  ~P o )  =/=  (/)  <->  ( ( F `  x )  i^i  ~P S )  =/=  (/) ) )
160159raleqbi1dv 2757 . . . 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 2938 . . 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 3678 . . . . . 6  |-  ( U  e.  ( F `  P )  ->  U  e.  { U } )
16670, 165syl 15 . . . . 5  |-  ( ph  ->  U  e.  { U } )
167 peano1 4691 . . . . . . 7  |-  (/)  e.  om
168 fnfvelrn 5678 . . . . . . 7  |-  ( ( G  Fn  om  /\  (/) 
e.  om )  ->  ( G `  (/) )  e. 
ran  G )
16916, 167, 168mp2an 653 . . . . . 6  |-  ( G `
 (/) )  e.  ran  G
17063, 169eqeltrri 2367 . . . . 5  |-  { U }  e.  ran  G
171 elunii 3848 . . . . 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 3522 . . . . 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 3641 . . . . . . 7  |-  ( f  =  U  ->  ~P f  =  ~P U
)
176175ineq2d 3383 . . . . . 6  |-  ( f  =  U  ->  (
( F `  P
)  i^i  ~P f
)  =  ( ( F `  P )  i^i  ~P U ) )
177176neeq1d 2472 . . . . 5  |-  ( f  =  U  ->  (
( ( F `  P )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P U )  =/=  (/) ) )
178177rspcev 2897 . . . 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 5541 . . . . . . 7  |-  ( y  =  P  ->  ( F `  y )  =  ( F `  P ) )
181180ineq1d 3382 . . . . . 6  |-  ( y  =  P  ->  (
( F `  y
)  i^i  ~P f
)  =  ( ( F `  P )  i^i  ~P f ) )
182181neeq1d 2472 . . . . 5  |-  ( y  =  P  ->  (
( ( F `  y )  i^i  ~P f )  =/=  (/)  <->  ( ( F `  P )  i^i  ~P f )  =/=  (/) ) )
183182rexbidv 2577 . . . 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 2938 . . 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 3847 . . . . . . 7  |-  ( f  e.  U. ran  G  <->  E. z  e.  ran  G  f  e.  z )
187 eleq2 2357 . . . . . . . . . 10  |-  ( z  =  ( G `  k )  ->  (
f  e.  z  <->  f  e.  ( G `  k ) ) )
188187rexrn 5683 . . . . . . . . 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 5679 . . . . . . . . . . . . . . . . 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 3646 . . . . . . . . . . . . . . . 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 3193 . . . . . . . . . . . . . 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 3646 . . . . . . . . . . . . 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 3202 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  y  e.  X )  /\  k  e.  om )  /\  ( f  e.  ( G `  k
)  /\  ( ( F `  y )  i^i  ~P f )  =/=  (/) ) )  ->  f  C_  N )
202 n0 3477 . . . . . . . . . . . . 13  |-  ( ( ( F `  y
)  i^i  ~P f
)  =/=  (/)  <->  E. v 
v  e.  ( ( F `  y )  i^i  ~P f ) )
203 elin 3371 . . . . . . . . . . . . . . 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 3646 . . . . . . . . . . . . . . . . . 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 2639 . . . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  y  ->  ( F `  x )  =  ( F `  y ) )
214213eleq2d 2363 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  y  ->  (
v  e.  ( F `
 x )  <->  v  e.  ( F `  y ) ) )
215 elequ1 1699 . . . . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . . . 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 3194 . . . . . . . . . . . . . . . 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 1626 . . . . . . . . . . . . 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 3194 . . . . . . . . . 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 2680 . . . . . . . 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 2679 . . . . 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 3266 . . 3  |-  ( ph  ->  { y  e.  X  |  E. f  e.  U. ran  G ( ( F `
 y )  i^i 
~P f )  =/=  (/) }  C_  N )
2331, 232syl5eqss 3235 . 2  |-  ( ph  ->  S  C_  N )
234 eleq2 2357 . . . 4  |-  ( u  =  S  ->  ( P  e.  u  <->  P  e.  S ) )
235 sseq1 3212 . . . 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 2897 . 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 1531    = wceq 1632    e. wcel 1696    =/= wne 2459   A.wral 2556   E.wrex 2557   {crab 2560   _Vcvv 2801    \ cdif 3162    i^i cin 3164    C_ wss 3165   (/)c0 3468   ~Pcpw 3638   {csn 3653   U.cuni 3843   U_ciun 3921    e. cmpt 4093   suc csuc 4410   omcom 4672   ran crn 4706    |` cres 4707    Fn wfn 5266   -->wf 5267   ` cfv 5271   reccrdg 6438
This theorem is referenced by:  neibastop2  26413
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
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 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-recs 6404  df-rdg 6439
  Copyright terms: Public domain W3C validator