ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  caucvgprprlemval Unicode version

Theorem caucvgprprlemval 7168
Description: Lemma for caucvgprpr 7192. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.)
Hypotheses
Ref Expression
caucvgprpr.f  |-  ( ph  ->  F : N. --> P. )
caucvgprpr.cau  |-  ( ph  ->  A. n  e.  N.  A. k  e.  N.  (
n  <N  k  ->  (
( F `  n
)  <P  ( ( F `
 k )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  k
)  <P  ( ( F `
 n )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >. )
) ) )
Assertion
Ref Expression
caucvgprprlemval  |-  ( (
ph  /\  A  <N  B )  ->  ( ( F `  A )  <P  ( ( F `  B )  +P.  <. { p  |  p  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q 
q } >. )  /\  ( F `  B
)  <P  ( ( F `
 A )  +P. 
<. { p  |  p 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  q } >. ) ) )
Distinct variable groups:    A, l    u, A    A, p, l    A, q, u    k, F, n   
k, l, n    u, k, n
Allowed substitution hints:    ph( u, k, n, q, p, l)    A( k, n)    B( u, k, n, q, p, l)    F( u, q, p, l)

Proof of Theorem caucvgprprlemval
Dummy variables  a  b are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltrelpi 6804 . . . . 5  |-  <N  C_  ( N.  X.  N. )
21brel 4451 . . . 4  |-  ( A 
<N  B  ->  ( A  e.  N.  /\  B  e.  N. ) )
32adantl 271 . . 3  |-  ( (
ph  /\  A  <N  B )  ->  ( A  e.  N.  /\  B  e. 
N. ) )
4 caucvgprpr.f . . . . 5  |-  ( ph  ->  F : N. --> P. )
5 caucvgprpr.cau . . . . 5  |-  ( ph  ->  A. n  e.  N.  A. k  e.  N.  (
n  <N  k  ->  (
( F `  n
)  <P  ( ( F `
 k )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  k
)  <P  ( ( F `
 n )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. n ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. n ,  1o >. ]  ~Q  )  <Q  u } >. )
) ) )
64, 5caucvgprprlemcbv 7167 . . . 4  |-  ( ph  ->  A. a  e.  N.  A. b  e.  N.  (
a  <N  b  ->  (
( F `  a
)  <P  ( ( F `
 b )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  b
)  <P  ( ( F `
 a )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )
) ) )
76adantr 270 . . 3  |-  ( (
ph  /\  A  <N  B )  ->  A. a  e.  N.  A. b  e. 
N.  ( a  <N 
b  ->  ( ( F `  a )  <P  ( ( F `  b )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  b
)  <P  ( ( F `
 a )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )
) ) )
8 simpr 108 . . 3  |-  ( (
ph  /\  A  <N  B )  ->  A  <N  B )
9 breq1 3817 . . . . 5  |-  ( a  =  A  ->  (
a  <N  b  <->  A  <N  b ) )
10 fveq2 5256 . . . . . . 7  |-  ( a  =  A  ->  ( F `  a )  =  ( F `  A ) )
11 opeq1 3599 . . . . . . . . . . . . 13  |-  ( a  =  A  ->  <. a ,  1o >.  =  <. A ,  1o >. )
1211eceq1d 6261 . . . . . . . . . . . 12  |-  ( a  =  A  ->  [ <. a ,  1o >. ]  ~Q  =  [ <. A ,  1o >. ]  ~Q  )
1312fveq2d 5260 . . . . . . . . . . 11  |-  ( a  =  A  ->  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  =  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) )
1413breq2d 3826 . . . . . . . . . 10  |-  ( a  =  A  ->  (
l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <->  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) ) )
1514abbidv 2202 . . . . . . . . 9  |-  ( a  =  A  ->  { l  |  l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) }  =  { l  |  l  <Q  ( *Q
`  [ <. A ,  1o >. ]  ~Q  ) } )
1613breq1d 3824 . . . . . . . . . 10  |-  ( a  =  A  ->  (
( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u  <->  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u ) )
1716abbidv 2202 . . . . . . . . 9  |-  ( a  =  A  ->  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u }  =  {
u  |  ( *Q
`  [ <. A ,  1o >. ]  ~Q  )  <Q  u } )
1815, 17opeq12d 3607 . . . . . . . 8  |-  ( a  =  A  ->  <. { l  |  l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >.  =  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
1918oveq2d 5610 . . . . . . 7  |-  ( a  =  A  ->  (
( F `  b
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )  =  ( ( F `  b
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. ) )
2010, 19breq12d 3827 . . . . . 6  |-  ( a  =  A  ->  (
( F `  a
)  <P  ( ( F `
 b )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )  <->  ( F `  A ) 
<P  ( ( F `  b )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) )
2110, 18oveq12d 5612 . . . . . . 7  |-  ( a  =  A  ->  (
( F `  a
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )  =  ( ( F `  A
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. ) )
2221breq2d 3826 . . . . . 6  |-  ( a  =  A  ->  (
( F `  b
)  <P  ( ( F `
 a )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )  <->  ( F `  b ) 
<P  ( ( F `  A )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) )
2320, 22anbi12d 457 . . . . 5  |-  ( a  =  A  ->  (
( ( F `  a )  <P  (
( F `  b
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  b )  <P  ( ( F `  a )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )
)  <->  ( ( F `
 A )  <P 
( ( F `  b )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  b
)  <P  ( ( F `
 A )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) ) )
249, 23imbi12d 232 . . . 4  |-  ( a  =  A  ->  (
( a  <N  b  ->  ( ( F `  a )  <P  (
( F `  b
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  b )  <P  ( ( F `  a )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )
) )  <->  ( A  <N  b  ->  ( ( F `  A )  <P  ( ( F `  b )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  b
)  <P  ( ( F `
 A )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) ) ) )
25 breq2 3818 . . . . 5  |-  ( b  =  B  ->  ( A  <N  b  <->  A  <N  B ) )
26 fveq2 5256 . . . . . . . 8  |-  ( b  =  B  ->  ( F `  b )  =  ( F `  B ) )
2726oveq1d 5609 . . . . . . 7  |-  ( b  =  B  ->  (
( F `  b
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  =  ( ( F `  B
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. ) )
2827breq2d 3826 . . . . . 6  |-  ( b  =  B  ->  (
( F `  A
)  <P  ( ( F `
 b )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  <->  ( F `  A ) 
<P  ( ( F `  B )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) )
2926breq1d 3824 . . . . . 6  |-  ( b  =  B  ->  (
( F `  b
)  <P  ( ( F `
 A )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  <->  ( F `  B ) 
<P  ( ( F `  A )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) )
3028, 29anbi12d 457 . . . . 5  |-  ( b  =  B  ->  (
( ( F `  A )  <P  (
( F `  b
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  b )  <P  ( ( F `  A )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
)  <->  ( ( F `
 A )  <P 
( ( F `  B )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  B
)  <P  ( ( F `
 A )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) ) )
3125, 30imbi12d 232 . . . 4  |-  ( b  =  B  ->  (
( A  <N  b  ->  ( ( F `  A )  <P  (
( F `  b
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  b )  <P  ( ( F `  A )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) )  <->  ( A  <N  B  ->  ( ( F `  A )  <P  ( ( F `  B )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  B
)  <P  ( ( F `
 A )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) ) ) )
3224, 31rspc2v 2725 . . 3  |-  ( ( A  e.  N.  /\  B  e.  N. )  ->  ( A. a  e. 
N.  A. b  e.  N.  ( a  <N  b  ->  ( ( F `  a )  <P  (
( F `  b
)  +P.  <. { l  |  l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  b )  <P  ( ( F `  a )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. a ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u } >. )
) )  ->  ( A  <N  B  ->  (
( F `  A
)  <P  ( ( F `
 B )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  B
)  <P  ( ( F `
 A )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) ) ) )
333, 7, 8, 32syl3c 62 . 2  |-  ( (
ph  /\  A  <N  B )  ->  ( ( F `  A )  <P  ( ( F `  B )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  B
)  <P  ( ( F `
 A )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
) )
34 breq1 3817 . . . . . . 7  |-  ( l  =  p  ->  (
l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <->  p  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) ) )
3534cbvabv 2208 . . . . . 6  |-  { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) }  =  { p  |  p  <Q  ( *Q
`  [ <. A ,  1o >. ]  ~Q  ) }
36 breq2 3818 . . . . . . 7  |-  ( u  =  q  ->  (
( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u  <->  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  q ) )
3736cbvabv 2208 . . . . . 6  |-  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u }  =  {
q  |  ( *Q
`  [ <. A ,  1o >. ]  ~Q  )  <Q  q }
3835, 37opeq12i 3604 . . . . 5  |-  <. { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >.  =  <. { p  |  p  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q 
q } >.
3938oveq2i 5605 . . . 4  |-  ( ( F `  B )  +P.  <. { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  =  ( ( F `  B
)  +P.  <. { p  |  p  <Q  ( *Q
`  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q 
q } >. )
4039breq2i 3822 . . 3  |-  ( ( F `  A ) 
<P  ( ( F `  B )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  <->  ( F `  A ) 
<P  ( ( F `  B )  +P.  <. { p  |  p  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q 
q } >. )
)
4138oveq2i 5605 . . . 4  |-  ( ( F `  A )  +P.  <. { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  =  ( ( F `  A
)  +P.  <. { p  |  p  <Q  ( *Q
`  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q 
q } >. )
4241breq2i 3822 . . 3  |-  ( ( F `  B ) 
<P  ( ( F `  A )  +P.  <. { l  |  l  <Q 
( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  <->  ( F `  B ) 
<P  ( ( F `  A )  +P.  <. { p  |  p  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q 
q } >. )
)
4340, 42anbi12i 448 . 2  |-  ( ( ( F `  A
)  <P  ( ( F `
 B )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )  /\  ( F `  B
)  <P  ( ( F `
 A )  +P. 
<. { l  |  l 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u } >. )
)  <->  ( ( F `
 A )  <P 
( ( F `  B )  +P.  <. { p  |  p  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q 
q } >. )  /\  ( F `  B
)  <P  ( ( F `
 A )  +P. 
<. { p  |  p 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  q } >. ) ) )
4433, 43sylib 120 1  |-  ( (
ph  /\  A  <N  B )  ->  ( ( F `  A )  <P  ( ( F `  B )  +P.  <. { p  |  p  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q 
q } >. )  /\  ( F `  B
)  <P  ( ( F `
 A )  +P. 
<. { p  |  p 
<Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  q } >. ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    = wceq 1287    e. wcel 1436   {cab 2071   A.wral 2355   <.cop 3428   class class class wbr 3814   -->wf 4968   ` cfv 4972  (class class class)co 5594   1oc1o 6109   [cec 6223   N.cnpi 6752    <N clti 6755    ~Q ceq 6759   *Qcrq 6764    <Q cltq 6765   P.cnp 6771    +P. cpp 6773    <P cltp 6775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3925  ax-pow 3977  ax-pr 4003
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ral 2360  df-rex 2361  df-v 2616  df-un 2990  df-in 2992  df-ss 2999  df-pw 3411  df-sn 3431  df-pr 3432  df-op 3434  df-uni 3631  df-br 3815  df-opab 3869  df-xp 4410  df-cnv 4412  df-dm 4414  df-rn 4415  df-res 4416  df-ima 4417  df-iota 4937  df-fv 4980  df-ov 5597  df-ec 6227  df-lti 6787
This theorem is referenced by:  caucvgprprlemnkltj  7169  caucvgprprlemnjltk  7171  caucvgprprlemnbj  7173
  Copyright terms: Public domain W3C validator