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

Theorem suplocexprlemlub 7723
Description: Lemma for suplocexpr 7724. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
Hypotheses
Ref Expression
suplocexpr.m  |-  ( ph  ->  E. x  x  e.  A )
suplocexpr.ub  |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
<P  x )
suplocexpr.loc  |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  (
x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )
suplocexpr.b  |-  B  = 
<. U. ( 1st " A
) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A
) w  <Q  u } >.
Assertion
Ref Expression
suplocexprlemlub  |-  ( ph  ->  ( y  <P  B  ->  E. z  e.  A  y  <P  z ) )
Distinct variable groups:    y, A, z   
x, A, y    z, B    ph, y, z    ph, x
Allowed substitution hints:    ph( w, u)    A( w, u)    B( x, y, w, u)

Proof of Theorem suplocexprlemlub
Dummy variable  s is distinct from all other variables.
StepHypRef Expression
1 simpr 110 . . . 4  |-  ( (
ph  /\  y  <P  B )  ->  y  <P  B )
2 ltrelpr 7504 . . . . . . . 8  |-  <P  C_  ( P.  X.  P. )
32brel 4679 . . . . . . 7  |-  ( y 
<P  B  ->  ( y  e.  P.  /\  B  e.  P. ) )
43simpld 112 . . . . . 6  |-  ( y 
<P  B  ->  y  e. 
P. )
54adantl 277 . . . . 5  |-  ( (
ph  /\  y  <P  B )  ->  y  e.  P. )
63simprd 114 . . . . . 6  |-  ( y 
<P  B  ->  B  e. 
P. )
76adantl 277 . . . . 5  |-  ( (
ph  /\  y  <P  B )  ->  B  e.  P. )
8 ltdfpr 7505 . . . . 5  |-  ( ( y  e.  P.  /\  B  e.  P. )  ->  ( y  <P  B  <->  E. s  e.  Q.  ( s  e.  ( 2nd `  y
)  /\  s  e.  ( 1st `  B ) ) ) )
95, 7, 8syl2anc 411 . . . 4  |-  ( (
ph  /\  y  <P  B )  ->  ( y  <P  B  <->  E. s  e.  Q.  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )
101, 9mpbid 147 . . 3  |-  ( (
ph  /\  y  <P  B )  ->  E. s  e.  Q.  ( s  e.  ( 2nd `  y
)  /\  s  e.  ( 1st `  B ) ) )
11 simprrr 540 . . . . . 6  |-  ( ( ( ph  /\  y  <P  B )  /\  (
s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  -> 
s  e.  ( 1st `  B ) )
12 suplocexpr.b . . . . . . . . . 10  |-  B  = 
<. U. ( 1st " A
) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A
) w  <Q  u } >.
1312fveq2i 5519 . . . . . . . . 9  |-  ( 1st `  B )  =  ( 1st `  <. U. ( 1st " A ) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w  <Q  u } >. )
14 npex 7472 . . . . . . . . . . . . 13  |-  P.  e.  _V
1514a1i 9 . . . . . . . . . . . 12  |-  ( ph  ->  P.  e.  _V )
16 suplocexpr.m . . . . . . . . . . . . 13  |-  ( ph  ->  E. x  x  e.  A )
17 suplocexpr.ub . . . . . . . . . . . . 13  |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
<P  x )
18 suplocexpr.loc . . . . . . . . . . . . 13  |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  (
x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )
1916, 17, 18suplocexprlemss 7714 . . . . . . . . . . . 12  |-  ( ph  ->  A  C_  P. )
2015, 19ssexd 4144 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  _V )
21 fo1st 6158 . . . . . . . . . . . . 13  |-  1st : _V -onto-> _V
22 fofun 5440 . . . . . . . . . . . . 13  |-  ( 1st
: _V -onto-> _V  ->  Fun 
1st )
2321, 22ax-mp 5 . . . . . . . . . . . 12  |-  Fun  1st
24 funimaexg 5301 . . . . . . . . . . . 12  |-  ( ( Fun  1st  /\  A  e. 
_V )  ->  ( 1st " A )  e. 
_V )
2523, 24mpan 424 . . . . . . . . . . 11  |-  ( A  e.  _V  ->  ( 1st " A )  e. 
_V )
26 uniexg 4440 . . . . . . . . . . 11  |-  ( ( 1st " A )  e.  _V  ->  U. ( 1st " A )  e. 
_V )
2720, 25, 263syl 17 . . . . . . . . . 10  |-  ( ph  ->  U. ( 1st " A
)  e.  _V )
28 nqex 7362 . . . . . . . . . . 11  |-  Q.  e.  _V
2928rabex 4148 . . . . . . . . . 10  |-  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A
) w  <Q  u }  e.  _V
30 op1stg 6151 . . . . . . . . . 10  |-  ( ( U. ( 1st " A
)  e.  _V  /\  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w 
<Q  u }  e.  _V )  ->  ( 1st `  <. U. ( 1st " A
) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A
) w  <Q  u } >. )  =  U. ( 1st " A ) )
3127, 29, 30sylancl 413 . . . . . . . . 9  |-  ( ph  ->  ( 1st `  <. U. ( 1st " A
) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A
) w  <Q  u } >. )  =  U. ( 1st " A ) )
3213, 31eqtrid 2222 . . . . . . . 8  |-  ( ph  ->  ( 1st `  B
)  =  U. ( 1st " A ) )
3332eleq2d 2247 . . . . . . 7  |-  ( ph  ->  ( s  e.  ( 1st `  B )  <-> 
s  e.  U. ( 1st " A ) ) )
3433ad2antrr 488 . . . . . 6  |-  ( ( ( ph  /\  y  <P  B )  /\  (
s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  -> 
( s  e.  ( 1st `  B )  <-> 
s  e.  U. ( 1st " A ) ) )
3511, 34mpbid 147 . . . . 5  |-  ( ( ( ph  /\  y  <P  B )  /\  (
s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  -> 
s  e.  U. ( 1st " A ) )
36 suplocexprlemell 7712 . . . . 5  |-  ( s  e.  U. ( 1st " A )  <->  E. z  e.  A  s  e.  ( 1st `  z ) )
3735, 36sylib 122 . . . 4  |-  ( ( ( ph  /\  y  <P  B )  /\  (
s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  ->  E. z  e.  A  s  e.  ( 1st `  z ) )
38 simprl 529 . . . . . . . . 9  |-  ( ( ( ph  /\  y  <P  B )  /\  (
s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  -> 
s  e.  Q. )
3938ad2antrr 488 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  /\  s  e.  ( 1st `  z ) )  ->  s  e.  Q. )
40 simprrl 539 . . . . . . . . 9  |-  ( ( ( ph  /\  y  <P  B )  /\  (
s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  -> 
s  e.  ( 2nd `  y ) )
4140ad2antrr 488 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  /\  s  e.  ( 1st `  z ) )  ->  s  e.  ( 2nd `  y ) )
42 simpr 110 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  /\  s  e.  ( 1st `  z ) )  ->  s  e.  ( 1st `  z ) )
43 rspe 2526 . . . . . . . 8  |-  ( ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  z ) ) )  ->  E. s  e.  Q.  ( s  e.  ( 2nd `  y
)  /\  s  e.  ( 1st `  z ) ) )
4439, 41, 42, 43syl12anc 1236 . . . . . . 7  |-  ( ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  /\  s  e.  ( 1st `  z ) )  ->  E. s  e.  Q.  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  z ) ) )
454ad4antlr 495 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  /\  s  e.  ( 1st `  z ) )  ->  y  e.  P. )
4619ad4antr 494 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  /\  s  e.  ( 1st `  z ) )  ->  A  C_  P. )
47 simplr 528 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  /\  s  e.  ( 1st `  z ) )  ->  z  e.  A
)
4846, 47sseldd 3157 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  /\  s  e.  ( 1st `  z ) )  ->  z  e.  P. )
49 ltdfpr 7505 . . . . . . . 8  |-  ( ( y  e.  P.  /\  z  e.  P. )  ->  ( y  <P  z  <->  E. s  e.  Q.  (
s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  z
) ) ) )
5045, 48, 49syl2anc 411 . . . . . . 7  |-  ( ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  /\  s  e.  ( 1st `  z ) )  ->  ( y  <P 
z  <->  E. s  e.  Q.  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  z ) ) ) )
5144, 50mpbird 167 . . . . . 6  |-  ( ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  /\  s  e.  ( 1st `  z ) )  ->  y  <P  z
)
5251ex 115 . . . . 5  |-  ( ( ( ( ph  /\  y  <P  B )  /\  ( s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  /\  z  e.  A )  ->  ( s  e.  ( 1st `  z )  ->  y  <P  z
) )
5352reximdva 2579 . . . 4  |-  ( ( ( ph  /\  y  <P  B )  /\  (
s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  -> 
( E. z  e.  A  s  e.  ( 1st `  z )  ->  E. z  e.  A  y  <P  z ) )
5437, 53mpd 13 . . 3  |-  ( ( ( ph  /\  y  <P  B )  /\  (
s  e.  Q.  /\  ( s  e.  ( 2nd `  y )  /\  s  e.  ( 1st `  B ) ) ) )  ->  E. z  e.  A  y  <P  z )
5510, 54rexlimddv 2599 . 2  |-  ( (
ph  /\  y  <P  B )  ->  E. z  e.  A  y  <P  z )
5655ex 115 1  |-  ( ph  ->  ( y  <P  B  ->  E. z  e.  A  y  <P  z ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    <-> wb 105    \/ wo 708    = wceq 1353   E.wex 1492    e. wcel 2148   A.wral 2455   E.wrex 2456   {crab 2459   _Vcvv 2738    C_ wss 3130   <.cop 3596   U.cuni 3810   |^|cint 3845   class class class wbr 4004   "cima 4630   Fun wfun 5211   -onto->wfo 5215   ` cfv 5217   1stc1st 6139   2ndc2nd 6140   Q.cnq 7279    <Q cltq 7284   P.cnp 7290    <P cltp 7294
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-iinf 4588
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-iom 4591  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-1st 6141  df-qs 6541  df-ni 7303  df-nqqs 7347  df-inp 7465  df-iltp 7469
This theorem is referenced by:  suplocexpr  7724
  Copyright terms: Public domain W3C validator