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

Theorem caucvgprprlemval 7245
Description: Lemma for caucvgprpr 7269. 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 6881 . . . . 5  |-  <N  C_  ( N.  X.  N. )
21brel 4490 . . . 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 7244 . . . 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 3848 . . . . 5  |-  ( a  =  A  ->  (
a  <N  b  <->  A  <N  b ) )
10 fveq2 5305 . . . . . . 7  |-  ( a  =  A  ->  ( F `  a )  =  ( F `  A ) )
11 opeq1 3622 . . . . . . . . . . . . 13  |-  ( a  =  A  ->  <. a ,  1o >.  =  <. A ,  1o >. )
1211eceq1d 6326 . . . . . . . . . . . 12  |-  ( a  =  A  ->  [ <. a ,  1o >. ]  ~Q  =  [ <. A ,  1o >. ]  ~Q  )
1312fveq2d 5309 . . . . . . . . . . 11  |-  ( a  =  A  ->  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  =  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) )
1413breq2d 3857 . . . . . . . . . 10  |-  ( a  =  A  ->  (
l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <->  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) ) )
1514abbidv 2205 . . . . . . . . 9  |-  ( a  =  A  ->  { l  |  l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) }  =  { l  |  l  <Q  ( *Q
`  [ <. A ,  1o >. ]  ~Q  ) } )
1613breq1d 3855 . . . . . . . . . 10  |-  ( a  =  A  ->  (
( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u  <->  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u ) )
1716abbidv 2205 . . . . . . . . 9  |-  ( a  =  A  ->  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u }  =  {
u  |  ( *Q
`  [ <. A ,  1o >. ]  ~Q  )  <Q  u } )
1815, 17opeq12d 3630 . . . . . . . 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 5668 . . . . . . 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 3858 . . . . . 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 5670 . . . . . . 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 3857 . . . . . 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 3849 . . . . 5  |-  ( b  =  B  ->  ( A  <N  b  <->  A  <N  B ) )
26 fveq2 5305 . . . . . . . 8  |-  ( b  =  B  ->  ( F `  b )  =  ( F `  B ) )
2726oveq1d 5667 . . . . . . 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 3857 . . . . . 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 3855 . . . . . 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 2734 . . 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 3848 . . . . . . 7  |-  ( l  =  p  ->  (
l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <->  p  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) ) )
3534cbvabv 2211 . . . . . 6  |-  { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) }  =  { p  |  p  <Q  ( *Q
`  [ <. A ,  1o >. ]  ~Q  ) }
36 breq2 3849 . . . . . . 7  |-  ( u  =  q  ->  (
( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u  <->  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  q ) )
3736cbvabv 2211 . . . . . 6  |-  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u }  =  {
q  |  ( *Q
`  [ <. A ,  1o >. ]  ~Q  )  <Q  q }
3835, 37opeq12i 3627 . . . . 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 5663 . . . 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 3853 . . 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 5663 . . . 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 3853 . . 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 1289    e. wcel 1438   {cab 2074   A.wral 2359   <.cop 3449   class class class wbr 3845   -->wf 5011   ` cfv 5015  (class class class)co 5652   1oc1o 6174   [cec 6288   N.cnpi 6829    <N clti 6832    ~Q ceq 6836   *Qcrq 6841    <Q cltq 6842   P.cnp 6848    +P. cpp 6850    <P cltp 6852
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 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-pow 4009  ax-pr 4036
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-un 3003  df-in 3005  df-ss 3012  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-br 3846  df-opab 3900  df-xp 4444  df-cnv 4446  df-dm 4448  df-rn 4449  df-res 4450  df-ima 4451  df-iota 4980  df-fv 5023  df-ov 5655  df-ec 6292  df-lti 6864
This theorem is referenced by:  caucvgprprlemnkltj  7246  caucvgprprlemnjltk  7248  caucvgprprlemnbj  7250
  Copyright terms: Public domain W3C validator