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

Theorem caucvgprprlemval 6767
Description: Lemma for caucvgprpr 6791. 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 6403 . . . . 5  |-  <N  C_  ( N.  X.  N. )
21brel 4379 . . . 4  |-  ( A 
<N  B  ->  ( A  e.  N.  /\  B  e.  N. ) )
32adantl 262 . . 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 6766 . . . 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 261 . . 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 103 . . 3  |-  ( (
ph  /\  A  <N  B )  ->  A  <N  B )
9 breq1 3764 . . . . 5  |-  ( a  =  A  ->  (
a  <N  b  <->  A  <N  b ) )
10 fveq2 5165 . . . . . . 7  |-  ( a  =  A  ->  ( F `  a )  =  ( F `  A ) )
11 opeq1 3546 . . . . . . . . . . . . 13  |-  ( a  =  A  ->  <. a ,  1o >.  =  <. A ,  1o >. )
1211eceq1d 6129 . . . . . . . . . . . 12  |-  ( a  =  A  ->  [ <. a ,  1o >. ]  ~Q  =  [ <. A ,  1o >. ]  ~Q  )
1312fveq2d 5169 . . . . . . . . . . 11  |-  ( a  =  A  ->  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  =  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) )
1413breq2d 3773 . . . . . . . . . 10  |-  ( a  =  A  ->  (
l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <->  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) ) )
1514abbidv 2155 . . . . . . . . 9  |-  ( a  =  A  ->  { l  |  l  <Q  ( *Q `  [ <. a ,  1o >. ]  ~Q  ) }  =  { l  |  l  <Q  ( *Q
`  [ <. A ,  1o >. ]  ~Q  ) } )
1613breq1d 3771 . . . . . . . . . 10  |-  ( a  =  A  ->  (
( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u  <->  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u ) )
1716abbidv 2155 . . . . . . . . 9  |-  ( a  =  A  ->  { u  |  ( *Q `  [ <. a ,  1o >. ]  ~Q  )  <Q  u }  =  {
u  |  ( *Q
`  [ <. A ,  1o >. ]  ~Q  )  <Q  u } )
1815, 17opeq12d 3554 . . . . . . . 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 5515 . . . . . . 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 3774 . . . . . 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 5517 . . . . . . 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 3773 . . . . . 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 442 . . . . 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 223 . . . 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 3765 . . . . 5  |-  ( b  =  B  ->  ( A  <N  b  <->  A  <N  B ) )
26 fveq2 5165 . . . . . . . 8  |-  ( b  =  B  ->  ( F `  b )  =  ( F `  B ) )
2726oveq1d 5514 . . . . . . 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 3773 . . . . . 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 3771 . . . . . 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 442 . . . . 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 223 . . . 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 2659 . . 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 57 . 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 3764 . . . . . . 7  |-  ( l  =  p  ->  (
l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <->  p  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) ) )
3534cbvabv 2161 . . . . . 6  |-  { l  |  l  <Q  ( *Q `  [ <. A ,  1o >. ]  ~Q  ) }  =  { p  |  p  <Q  ( *Q
`  [ <. A ,  1o >. ]  ~Q  ) }
36 breq2 3765 . . . . . . 7  |-  ( u  =  q  ->  (
( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u  <->  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  q ) )
3736cbvabv 2161 . . . . . 6  |-  { u  |  ( *Q `  [ <. A ,  1o >. ]  ~Q  )  <Q  u }  =  {
q  |  ( *Q
`  [ <. A ,  1o >. ]  ~Q  )  <Q  q }
3835, 37opeq12i 3551 . . . . 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 5510 . . . 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 3769 . . 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 5510 . . . 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 3769 . . 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 433 . 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 127 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 97    = wceq 1243    e. wcel 1393   {cab 2026   A.wral 2303   <.cop 3375   class class class wbr 3761   -->wf 4885   ` cfv 4889  (class class class)co 5499   1oc1o 5981   [cec 6091   N.cnpi 6351    <N clti 6354    ~Q ceq 6358   *Qcrq 6363    <Q cltq 6364   P.cnp 6370    +P. cpp 6372    <P cltp 6374
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3872  ax-pow 3924  ax-pr 3941
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2308  df-rex 2309  df-v 2556  df-un 2919  df-in 2921  df-ss 2928  df-pw 3358  df-sn 3378  df-pr 3379  df-op 3381  df-uni 3578  df-br 3762  df-opab 3816  df-xp 4338  df-cnv 4340  df-dm 4342  df-rn 4343  df-res 4344  df-ima 4345  df-iota 4854  df-fv 4897  df-ov 5502  df-ec 6095  df-lti 6386
This theorem is referenced by:  caucvgprprlemnkltj  6768  caucvgprprlemnjltk  6770  caucvgprprlemnbj  6772
  Copyright terms: Public domain W3C validator