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

Theorem suplocsrlemb 7739
Description: Lemma for suplocsr 7742. The set  B is located. (Contributed by Jim Kingdon, 18-Jan-2024.)
Hypotheses
Ref Expression
suplocsrlem.b  |-  B  =  { w  e.  P.  |  ( C  +R  [
<. w ,  1P >. ]  ~R  )  e.  A }
suplocsrlem.ss  |-  ( ph  ->  A  C_  R. )
suplocsrlem.c  |-  ( ph  ->  C  e.  A )
suplocsrlem.ub  |-  ( ph  ->  E. x  e.  R.  A. y  e.  A  y 
<R  x )
suplocsrlem.loc  |-  ( ph  ->  A. x  e.  R.  A. y  e.  R.  (
x  <R  y  ->  ( E. z  e.  A  x  <R  z  \/  A. z  e.  A  z  <R  y ) ) )
Assertion
Ref Expression
suplocsrlemb  |-  ( ph  ->  A. u  e.  P.  A. v  e.  P.  (
u  <P  v  ->  ( E. q  e.  B  u  <P  q  \/  A. q  e.  B  q  <P  v ) ) )
Distinct variable groups:    A, q, w   
x, A, y, z   
z, B    C, q, w    x, C, y, z    ph, q, u, v, z   
x, u, y    y,
v
Allowed substitution hints:    ph( x, y, w)    A( v, u)    B( x, y, w, v, u, q)    C( v, u)

Proof of Theorem suplocsrlemb
StepHypRef Expression
1 simpr 109 . . . . . 6  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  u  <P  v )
2 simplrl 525 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  u  e.  P. )
3 simplrr 526 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  v  e.  P. )
4 suplocsrlem.ss . . . . . . . . 9  |-  ( ph  ->  A  C_  R. )
5 suplocsrlem.c . . . . . . . . 9  |-  ( ph  ->  C  e.  A )
64, 5sseldd 3139 . . . . . . . 8  |-  ( ph  ->  C  e.  R. )
76ad2antrr 480 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  C  e.  R. )
8 ltpsrprg 7736 . . . . . . 7  |-  ( ( u  e.  P.  /\  v  e.  P.  /\  C  e.  R. )  ->  (
( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  )  <->  u 
<P  v ) )
92, 3, 7, 8syl3anc 1227 . . . . . 6  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  ( ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  )  <->  u  <P  v ) )
101, 9mpbird 166 . . . . 5  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R 
( C  +R  [ <. v ,  1P >. ]  ~R  ) )
11 breq2 3981 . . . . . . 7  |-  ( y  =  ( C  +R  [
<. v ,  1P >. ]  ~R  )  ->  (
( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  y  <->  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  ( C  +R  [
<. v ,  1P >. ]  ~R  ) ) )
12 breq2 3981 . . . . . . . . 9  |-  ( y  =  ( C  +R  [
<. v ,  1P >. ]  ~R  )  ->  (
z  <R  y  <->  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) ) )
1312ralbidv 2464 . . . . . . . 8  |-  ( y  =  ( C  +R  [
<. v ,  1P >. ]  ~R  )  ->  ( A. z  e.  A  z  <R  y  <->  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) ) )
1413orbi2d 780 . . . . . . 7  |-  ( y  =  ( C  +R  [
<. v ,  1P >. ]  ~R  )  ->  (
( E. z  e.  A  ( C  +R  [
<. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  y )  <->  ( E. z  e.  A  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) ) ) )
1511, 14imbi12d 233 . . . . . 6  |-  ( y  =  ( C  +R  [
<. v ,  1P >. ]  ~R  )  ->  (
( ( C  +R  [
<. u ,  1P >. ]  ~R  )  <R  y  ->  ( E. z  e.  A  ( C  +R  [
<. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  y ) )  <-> 
( ( C  +R  [
<. u ,  1P >. ]  ~R  )  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  )  ->  ( E. z  e.  A  ( C  +R  [
<. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  ( C  +R  [
<. v ,  1P >. ]  ~R  ) ) ) ) )
16 breq1 3980 . . . . . . . . 9  |-  ( x  =  ( C  +R  [
<. u ,  1P >. ]  ~R  )  ->  (
x  <R  y  <->  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R 
y ) )
17 breq1 3980 . . . . . . . . . . 11  |-  ( x  =  ( C  +R  [
<. u ,  1P >. ]  ~R  )  ->  (
x  <R  z  <->  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R 
z ) )
1817rexbidv 2465 . . . . . . . . . 10  |-  ( x  =  ( C  +R  [
<. u ,  1P >. ]  ~R  )  ->  ( E. z  e.  A  x  <R  z  <->  E. z  e.  A  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R 
z ) )
1918orbi1d 781 . . . . . . . . 9  |-  ( x  =  ( C  +R  [
<. u ,  1P >. ]  ~R  )  ->  (
( E. z  e.  A  x  <R  z  \/  A. z  e.  A  z  <R  y )  <->  ( E. z  e.  A  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  y ) ) )
2016, 19imbi12d 233 . . . . . . . 8  |-  ( x  =  ( C  +R  [
<. u ,  1P >. ]  ~R  )  ->  (
( x  <R  y  ->  ( E. z  e.  A  x  <R  z  \/  A. z  e.  A  z  <R  y ) )  <-> 
( ( C  +R  [
<. u ,  1P >. ]  ~R  )  <R  y  ->  ( E. z  e.  A  ( C  +R  [
<. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  y ) ) ) )
2120ralbidv 2464 . . . . . . 7  |-  ( x  =  ( C  +R  [
<. u ,  1P >. ]  ~R  )  ->  ( A. y  e.  R.  ( x  <R  y  -> 
( E. z  e.  A  x  <R  z  \/  A. z  e.  A  z  <R  y ) )  <->  A. y  e.  R.  ( ( C  +R  [
<. u ,  1P >. ]  ~R  )  <R  y  ->  ( E. z  e.  A  ( C  +R  [
<. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  y ) ) ) )
22 suplocsrlem.loc . . . . . . . 8  |-  ( ph  ->  A. x  e.  R.  A. y  e.  R.  (
x  <R  y  ->  ( E. z  e.  A  x  <R  z  \/  A. z  e.  A  z  <R  y ) ) )
2322ad2antrr 480 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  A. x  e.  R.  A. y  e. 
R.  ( x  <R  y  ->  ( E. z  e.  A  x  <R  z  \/  A. z  e.  A  z  <R  y
) ) )
24 1pr 7487 . . . . . . . . . . . 12  |-  1P  e.  P.
2524a1i 9 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  1P  e.  P. )
262, 25opelxpd 4632 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  <. u ,  1P >.  e.  ( P.  X.  P. ) )
27 enrex 7670 . . . . . . . . . . 11  |-  ~R  e.  _V
2827ecelqsi 6547 . . . . . . . . . 10  |-  ( <.
u ,  1P >.  e.  ( P.  X.  P. )  ->  [ <. u ,  1P >. ]  ~R  e.  ( ( P.  X.  P. ) /.  ~R  )
)
2926, 28syl 14 . . . . . . . . 9  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  [ <. u ,  1P >. ]  ~R  e.  ( ( P.  X.  P. ) /.  ~R  )
)
30 df-nr 7660 . . . . . . . . 9  |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )
3129, 30eleqtrrdi 2258 . . . . . . . 8  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  [ <. u ,  1P >. ]  ~R  e.  R. )
32 addclsr 7686 . . . . . . . 8  |-  ( ( C  e.  R.  /\  [
<. u ,  1P >. ]  ~R  e.  R. )  ->  ( C  +R  [ <. u ,  1P >. ]  ~R  )  e.  R. )
337, 31, 32syl2anc 409 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  ( C  +R  [ <. u ,  1P >. ]  ~R  )  e. 
R. )
3421, 23, 33rspcdva 2831 . . . . . 6  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  A. y  e.  R.  ( ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  y  ->  ( E. z  e.  A  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  y ) ) )
353, 25opelxpd 4632 . . . . . . . 8  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  <. v ,  1P >.  e.  ( P.  X.  P. ) )
3627ecelqsi 6547 . . . . . . . . 9  |-  ( <.
v ,  1P >.  e.  ( P.  X.  P. )  ->  [ <. v ,  1P >. ]  ~R  e.  ( ( P.  X.  P. ) /.  ~R  )
)
3736, 30eleqtrrdi 2258 . . . . . . . 8  |-  ( <.
v ,  1P >.  e.  ( P.  X.  P. )  ->  [ <. v ,  1P >. ]  ~R  e.  R. )
3835, 37syl 14 . . . . . . 7  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  [ <. v ,  1P >. ]  ~R  e.  R. )
39 addclsr 7686 . . . . . . 7  |-  ( ( C  e.  R.  /\  [
<. v ,  1P >. ]  ~R  e.  R. )  ->  ( C  +R  [ <. v ,  1P >. ]  ~R  )  e.  R. )
407, 38, 39syl2anc 409 . . . . . 6  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  ( C  +R  [ <. v ,  1P >. ]  ~R  )  e. 
R. )
4115, 34, 40rspcdva 2831 . . . . 5  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  ( ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  )  ->  ( E. z  e.  A  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) ) ) )
4210, 41mpd 13 . . . 4  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  ( E. z  e.  A  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) ) )
432ad2antrr 480 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  u  e.  P. )
447ad2antrr 480 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  C  e.  R. )
45 mappsrprg 7737 . . . . . . . . . . 11  |-  ( ( u  e.  P.  /\  C  e.  R. )  ->  ( C  +R  -1R )  <R  ( C  +R  [
<. u ,  1P >. ]  ~R  ) )
4643, 44, 45syl2anc 409 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  ( C  +R  -1R )  <R 
( C  +R  [ <. u ,  1P >. ]  ~R  ) )
47 simpr 109 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )
48 ltsosr 7697 . . . . . . . . . . 11  |-  <R  Or  R.
49 ltrelsr 7671 . . . . . . . . . . 11  |-  <R  C_  ( R.  X.  R. )
5048, 49sotri 4994 . . . . . . . . . 10  |-  ( ( ( C  +R  -1R )  <R  ( C  +R  [
<. u ,  1P >. ]  ~R  )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  ( C  +R  -1R )  <R 
z )
5146, 47, 50syl2anc 409 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  ( C  +R  -1R )  <R 
z )
52 map2psrprg 7738 . . . . . . . . . 10  |-  ( C  e.  R.  ->  (
( C  +R  -1R )  <R  z  <->  E. q  e.  P.  ( C  +R  [
<. q ,  1P >. ]  ~R  )  =  z ) )
5344, 52syl 14 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  (
( C  +R  -1R )  <R  z  <->  E. q  e.  P.  ( C  +R  [
<. q ,  1P >. ]  ~R  )  =  z ) )
5451, 53mpbid 146 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  E. q  e.  P.  ( C  +R  [
<. q ,  1P >. ]  ~R  )  =  z )
55 simpr 109 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  -> 
( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )
56 simp-4r 532 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  -> 
z  e.  A )
5755, 56eqeltrd 2241 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  -> 
( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A
)
58 simpllr 524 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  -> 
( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z
)
5958, 55breqtrrd 4005 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  -> 
( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  ( C  +R  [ <. q ,  1P >. ]  ~R  )
)
602ad4antr 486 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  ->  u  e.  P. )
61 simplr 520 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  -> 
q  e.  P. )
6244ad2antrr 480 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  ->  C  e.  R. )
63 ltpsrprg 7736 . . . . . . . . . . . . 13  |-  ( ( u  e.  P.  /\  q  e.  P.  /\  C  e.  R. )  ->  (
( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  ( C  +R  [ <. q ,  1P >. ]  ~R  )  <->  u 
<P  q ) )
6460, 61, 62, 63syl3anc 1227 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  -> 
( ( C  +R  [
<. u ,  1P >. ]  ~R  )  <R  ( C  +R  [ <. q ,  1P >. ]  ~R  )  <->  u 
<P  q ) )
6559, 64mpbid 146 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  ->  u  <P  q )
6657, 65jca 304 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  /\  q  e.  P. )  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z )  -> 
( ( C  +R  [
<. q ,  1P >. ]  ~R  )  e.  A  /\  u  <P  q ) )
6766ex 114 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  ( u  e.  P.  /\  v  e. 
P. ) )  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z
)  /\  q  e.  P. )  ->  ( ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z  ->  ( ( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A  /\  u  <P  q ) ) )
6867reximdva 2566 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  ( E. q  e.  P.  ( C  +R  [ <. q ,  1P >. ]  ~R  )  =  z  ->  E. q  e.  P.  (
( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A  /\  u  <P  q ) ) )
6954, 68mpd 13 . . . . . . 7  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  E. q  e.  P.  ( ( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A  /\  u  <P  q ) )
70 opeq1 3753 . . . . . . . . . . . . . 14  |-  ( w  =  q  ->  <. w ,  1P >.  =  <. q ,  1P >. )
7170eceq1d 6529 . . . . . . . . . . . . 13  |-  ( w  =  q  ->  [ <. w ,  1P >. ]  ~R  =  [ <. q ,  1P >. ]  ~R  )
7271oveq2d 5853 . . . . . . . . . . . 12  |-  ( w  =  q  ->  ( C  +R  [ <. w ,  1P >. ]  ~R  )  =  ( C  +R  [
<. q ,  1P >. ]  ~R  ) )
7372eleq1d 2233 . . . . . . . . . . 11  |-  ( w  =  q  ->  (
( C  +R  [ <. w ,  1P >. ]  ~R  )  e.  A  <->  ( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A )
)
74 suplocsrlem.b . . . . . . . . . . 11  |-  B  =  { w  e.  P.  |  ( C  +R  [
<. w ,  1P >. ]  ~R  )  e.  A }
7573, 74elrab2 2881 . . . . . . . . . 10  |-  ( q  e.  B  <->  ( q  e.  P.  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A ) )
7675anbi1i 454 . . . . . . . . 9  |-  ( ( q  e.  B  /\  u  <P  q )  <->  ( (
q  e.  P.  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A )  /\  u  <P  q ) )
77 anass 399 . . . . . . . . 9  |-  ( ( ( q  e.  P.  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A
)  /\  u  <P  q )  <->  ( q  e. 
P.  /\  ( ( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A  /\  u  <P  q ) ) )
7876, 77bitri 183 . . . . . . . 8  |-  ( ( q  e.  B  /\  u  <P  q )  <->  ( q  e.  P.  /\  ( ( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A  /\  u  <P  q ) ) )
7978rexbii2 2475 . . . . . . 7  |-  ( E. q  e.  B  u 
<P  q  <->  E. q  e.  P.  ( ( C  +R  [
<. q ,  1P >. ]  ~R  )  e.  A  /\  u  <P  q ) )
8069, 79sylibr 133 . . . . . 6  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  z  e.  A )  /\  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z )  ->  E. q  e.  B  u  <P  q )
8180rexlimdva2 2584 . . . . 5  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  ( E. z  e.  A  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z  ->  E. q  e.  B  u  <P  q ) )
82 breq1 3980 . . . . . . . . 9  |-  ( z  =  ( C  +R  [
<. q ,  1P >. ]  ~R  )  ->  (
z  <R  ( C  +R  [
<. v ,  1P >. ]  ~R  )  <->  ( C  +R  [ <. q ,  1P >. ]  ~R  )  <R 
( C  +R  [ <. v ,  1P >. ]  ~R  ) ) )
83 simplr 520 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  /\  q  e.  B )  ->  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )
84 simpr 109 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  /\  q  e.  B )  ->  q  e.  B )
8584, 75sylib 121 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  /\  q  e.  B )  ->  (
q  e.  P.  /\  ( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A )
)
8685simprd 113 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  /\  q  e.  B )  ->  ( C  +R  [ <. q ,  1P >. ]  ~R  )  e.  A )
8782, 83, 86rspcdva 2831 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  /\  q  e.  B )  ->  ( C  +R  [ <. q ,  1P >. ]  ~R  )  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )
8885simpld 111 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  /\  q  e.  B )  ->  q  e.  P. )
893ad2antrr 480 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  /\  q  e.  B )  ->  v  e.  P. )
907ad2antrr 480 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  /\  q  e.  B )  ->  C  e.  R. )
91 ltpsrprg 7736 . . . . . . . . 9  |-  ( ( q  e.  P.  /\  v  e.  P.  /\  C  e.  R. )  ->  (
( C  +R  [ <. q ,  1P >. ]  ~R  )  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  )  <->  q 
<P  v ) )
9288, 89, 90, 91syl3anc 1227 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  /\  q  e.  B )  ->  (
( C  +R  [ <. q ,  1P >. ]  ~R  )  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  )  <->  q 
<P  v ) )
9387, 92mpbid 146 . . . . . . 7  |-  ( ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  /\  q  e.  B )  ->  q  <P  v )
9493ralrimiva 2537 . . . . . 6  |-  ( ( ( ( ph  /\  ( u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  /\  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  ->  A. q  e.  B  q  <P  v )
9594ex 114 . . . . 5  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  ( A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  )  ->  A. q  e.  B  q  <P  v ) )
9681, 95orim12d 776 . . . 4  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  ( ( E. z  e.  A  ( C  +R  [ <. u ,  1P >. ]  ~R  )  <R  z  \/  A. z  e.  A  z  <R  ( C  +R  [ <. v ,  1P >. ]  ~R  ) )  -> 
( E. q  e.  B  u  <P  q  \/  A. q  e.  B  q  <P  v ) ) )
9742, 96mpd 13 . . 3  |-  ( ( ( ph  /\  (
u  e.  P.  /\  v  e.  P. )
)  /\  u  <P  v )  ->  ( E. q  e.  B  u  <P  q  \/  A. q  e.  B  q  <P  v ) )
9897ex 114 . 2  |-  ( (
ph  /\  ( u  e.  P.  /\  v  e. 
P. ) )  -> 
( u  <P  v  ->  ( E. q  e.  B  u  <P  q  \/  A. q  e.  B  q  <P  v ) ) )
9998ralrimivva 2546 1  |-  ( ph  ->  A. u  e.  P.  A. v  e.  P.  (
u  <P  v  ->  ( E. q  e.  B  u  <P  q  \/  A. q  e.  B  q  <P  v ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 698    = wceq 1342    e. wcel 2135   A.wral 2442   E.wrex 2443   {crab 2446    C_ wss 3112   <.cop 3574   class class class wbr 3977    X. cxp 4597  (class class class)co 5837   [cec 6491   /.cqs 6492   P.cnp 7224   1Pc1p 7225    <P cltp 7228    ~R cer 7229   R.cnr 7230   -1Rcm1r 7233    +R cplr 7234    <R cltr 7236
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-coll 4092  ax-sep 4095  ax-nul 4103  ax-pow 4148  ax-pr 4182  ax-un 4406  ax-setind 4509  ax-iinf 4560
This theorem depends on definitions:  df-bi 116  df-dc 825  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2724  df-sbc 2948  df-csb 3042  df-dif 3114  df-un 3116  df-in 3118  df-ss 3125  df-nul 3406  df-pw 3556  df-sn 3577  df-pr 3578  df-op 3580  df-uni 3785  df-int 3820  df-iun 3863  df-br 3978  df-opab 4039  df-mpt 4040  df-tr 4076  df-eprel 4262  df-id 4266  df-po 4269  df-iso 4270  df-iord 4339  df-on 4341  df-suc 4344  df-iom 4563  df-xp 4605  df-rel 4606  df-cnv 4607  df-co 4608  df-dm 4609  df-rn 4610  df-res 4611  df-ima 4612  df-iota 5148  df-fun 5185  df-fn 5186  df-f 5187  df-f1 5188  df-fo 5189  df-f1o 5190  df-fv 5191  df-ov 5840  df-oprab 5841  df-mpo 5842  df-1st 6101  df-2nd 6102  df-recs 6265  df-irdg 6330  df-1o 6376  df-2o 6377  df-oadd 6380  df-omul 6381  df-er 6493  df-ec 6495  df-qs 6499  df-ni 7237  df-pli 7238  df-mi 7239  df-lti 7240  df-plpq 7277  df-mpq 7278  df-enq 7280  df-nqqs 7281  df-plqqs 7282  df-mqqs 7283  df-1nqqs 7284  df-rq 7285  df-ltnqqs 7286  df-enq0 7357  df-nq0 7358  df-0nq0 7359  df-plq0 7360  df-mq0 7361  df-inp 7399  df-i1p 7400  df-iplp 7401  df-imp 7402  df-iltp 7403  df-enr 7659  df-nr 7660  df-plr 7661  df-mr 7662  df-ltr 7663  df-0r 7664  df-1r 7665  df-m1r 7666
This theorem is referenced by:  suplocsrlempr  7740
  Copyright terms: Public domain W3C validator