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

Theorem suplociccex 12782
 Description: An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7844 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.)
Hypotheses
Ref Expression
suplocicc.1
suplocicc.2
suplocicc.bc
suplocicc.3
suplocicc.m
suplocicc.l
Assertion
Ref Expression
suplociccex
Distinct variable groups:   ,,,   ,,,   ,,,   ,,,

Proof of Theorem suplociccex
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 suplocicc.1 . . 3
2 suplocicc.2 . . 3
3 suplocicc.bc . . 3
4 suplocicc.3 . . 3
5 suplocicc.m . . 3
6 suplocicc.l . . 3
71, 2, 3, 4, 5, 6suplociccreex 12781 . 2
8 simprl 520 . . . 4
9 eleq1w 2200 . . . . . . . 8
109cbvexv 1890 . . . . . . 7
115, 10sylib 121 . . . . . 6
1211adantr 274 . . . . 5
131ad2antrr 479 . . . . . 6
14 iccssre 9745 . . . . . . . . . 10
151, 2, 14syl2anc 408 . . . . . . . . 9
164, 15sstrd 3107 . . . . . . . 8
1716ad2antrr 479 . . . . . . 7
18 simpr 109 . . . . . . 7
1917, 18sseldd 3098 . . . . . 6
208adantr 274 . . . . . 6
2113rexrd 7822 . . . . . . 7
222rexrd 7822 . . . . . . . 8
2322ad2antrr 479 . . . . . . 7
244ad2antrr 479 . . . . . . . 8
2524, 18sseldd 3098 . . . . . . 7
26 iccgelb 9722 . . . . . . 7
2721, 23, 25, 26syl3anc 1216 . . . . . 6
28 breq2 3933 . . . . . . . . 9
2928notbid 656 . . . . . . . 8
30 simprrl 528 . . . . . . . . 9
3130adantr 274 . . . . . . . 8
3229, 31, 18rspcdva 2794 . . . . . . 7
3319, 20, 32nltled 7890 . . . . . 6
3413, 19, 20, 27, 33letrd 7893 . . . . 5
3512, 34exlimddv 1870 . . . 4
36 simpl 108 . . . . . 6
37 simprrr 529 . . . . . . 7
388, 30, 373jca 1161 . . . . . 6
39 lttri3 7851 . . . . . . . 8
4039adantl 275 . . . . . . 7
4140eqsupti 6883 . . . . . 6
4236, 38, 41sylc 62 . . . . 5
431rexrd 7822 . . . . . . . . . 10
4443adantr 274 . . . . . . . . 9
4522adantr 274 . . . . . . . . 9
464sselda 3097 . . . . . . . . 9
47 iccleub 9721 . . . . . . . . 9
4844, 45, 46, 47syl3anc 1216 . . . . . . . 8
4948ralrimiva 2505 . . . . . . 7
507, 16, 2suprleubex 8719 . . . . . . 7
5149, 50mpbird 166 . . . . . 6
5251adantr 274 . . . . 5
5342, 52eqbrtrrd 3952 . . . 4
548, 35, 533jca 1161 . . 3
55 elicc2 9728 . . . . 5
561, 2, 55syl2anc 408 . . . 4