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

Theorem suplocexprlemex 7636
 Description: Lemma for suplocexpr 7639. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.)
Hypotheses
Ref Expression
suplocexpr.m
suplocexpr.ub
suplocexpr.loc
suplocexpr.b
Assertion
Ref Expression
suplocexprlemex
Distinct variable groups:   ,,,   ,,,,   ,   ,,,   ,,
Allowed substitution hints:   (,,,)

Proof of Theorem suplocexprlemex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suplocexpr.b . . 3
2 suplocexpr.m . . . . . 6
3 suplocexpr.ub . . . . . 6
4 suplocexpr.loc . . . . . 6
52, 3, 4suplocexprlemss 7629 . . . . 5
61suplocexprlem2b 7628 . . . . 5
75, 6syl 14 . . . 4
87opeq2d 3748 . . 3
91, 8eqtr4id 2209 . 2
10 suplocexprlemell 7627 . . . . . . . . 9
1110biimpi 119 . . . . . . . 8
1211adantl 275 . . . . . . 7
135ad2antrr 480 . . . . . . . . . 10
14 simprl 521 . . . . . . . . . 10
1513, 14sseldd 3129 . . . . . . . . 9
16 prop 7389 . . . . . . . . 9
1715, 16syl 14 . . . . . . . 8
18 simprr 522 . . . . . . . 8
19 elprnql 7395 . . . . . . . 8
2017, 18, 19syl2anc 409 . . . . . . 7
2112, 20rexlimddv 2579 . . . . . 6
2221ex 114 . . . . 5
2322ssrdv 3134 . . . 4
24 ssrab2 3213 . . . . 5
257, 24eqsstrdi 3180 . . . 4
262, 3, 4suplocexprlemml 7630 . . . . 5
272, 3, 4, 1suplocexprlemmu 7632 . . . . 5
2826, 27jca 304 . . . 4
2923, 25, 28jca31 307 . . 3
302, 3, 4suplocexprlemrl 7631 . . . . 5
312, 3, 4, 1suplocexprlemru 7633 . . . . 5
3230, 31jca 304 . . . 4
332, 3, 4, 1suplocexprlemdisj 7634 . . . 4
342, 3, 4, 1suplocexprlemloc 7635 . . . 4
3532, 33, 343jca 1162 . . 3
36 elinp 7388 . . 3
3729, 35, 36sylanbrc 414 . 2
389, 37eqeltrd 2234 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wb 104   wo 698   w3a 963   wceq 1335  wex 1472   wcel 2128  wral 2435  wrex 2436  crab 2439   wss 3102  cop 3563  cuni 3772  cint 3807   class class class wbr 3965  cima 4588  cfv 5169  c1st 6083  c2nd 6084  cnq 7194   cltq 7199  cnp 7205   cltp 7209 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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4079  ax-sep 4082  ax-nul 4090  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4495  ax-iinf 4546 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-ral 2440  df-rex 2441  df-reu 2442  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-iun 3851  df-br 3966  df-opab 4026  df-mpt 4027  df-tr 4063  df-eprel 4249  df-id 4253  df-po 4256  df-iso 4257  df-iord 4326  df-on 4328  df-suc 4331  df-iom 4549  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-rn 4596  df-res 4597  df-ima 4598  df-iota 5134  df-fun 5171  df-fn 5172  df-f 5173  df-f1 5174  df-fo 5175  df-f1o 5176  df-fv 5177  df-ov 5824  df-oprab 5825  df-mpo 5826  df-1st 6085  df-2nd 6086  df-recs 6249  df-irdg 6314  df-1o 6360  df-2o 6361  df-oadd 6364  df-omul 6365  df-er 6477  df-ec 6479  df-qs 6483  df-ni 7218  df-pli 7219  df-mi 7220  df-lti 7221  df-plpq 7258  df-mpq 7259  df-enq 7261  df-nqqs 7262  df-plqqs 7263  df-mqqs 7264  df-1nqqs 7265  df-rq 7266  df-ltnqqs 7267  df-enq0 7338  df-nq0 7339  df-0nq0 7340  df-plq0 7341  df-mq0 7342  df-inp 7380  df-iltp 7384 This theorem is referenced by:  suplocexprlemub  7637  suplocexpr  7639
 Copyright terms: Public domain W3C validator