Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-pre-suploc Unicode version

Axiom ax-pre-suploc 7748
 Description: An inhabited, bounded-above, located set of reals has a supremum. Locatedness here means that given , either there is an element of the set greater than , or is an upper bound. Although this and ax-caucvg 7747 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7747. (Contributed by Jim Kingdon, 23-Jan-2024.)
Assertion
Ref Expression
ax-pre-suploc
Distinct variable group:   ,,,

Detailed syntax breakdown of Axiom ax-pre-suploc
StepHypRef Expression
1 cA . . . . 5
2 cr 7626 . . . . 5
31, 2wss 3071 . . . 4
4 vx . . . . . . 7
54cv 1330 . . . . . 6
65, 1wcel 1480 . . . . 5
76, 4wex 1468 . . . 4
83, 7wa 103 . . 3
9 vy . . . . . . . 8
109cv 1330 . . . . . . 7
11 cltrr 7631 . . . . . . 7
1210, 5, 11wbr 3929 . . . . . 6
1312, 9, 1wral 2416 . . . . 5
1413, 4, 2wrex 2417 . . . 4
155, 10, 11wbr 3929 . . . . . . 7
16 vz . . . . . . . . . . 11
1716cv 1330 . . . . . . . . . 10
185, 17, 11wbr 3929 . . . . . . . . 9
1918, 16, 1wrex 2417 . . . . . . . 8
2017, 10, 11wbr 3929 . . . . . . . . 9
2120, 16, 1wral 2416 . . . . . . . 8
2219, 21wo 697 . . . . . . 7
2315, 22wi 4 . . . . . 6
2423, 9, 2wral 2416 . . . . 5
2524, 4, 2wral 2416 . . . 4
2614, 25wa 103 . . 3
278, 26wa 103 . 2
2815wn 3 . . . . 5
2928, 9, 1wral 2416 . . . 4
3010, 17, 11wbr 3929 . . . . . . 7
3130, 16, 1wrex 2417 . . . . . 6
3212, 31wi 4 . . . . 5
3332, 9, 2wral 2416 . . . 4
3429, 33wa 103 . . 3
3534, 4, 2wrex 2417 . 2
3627, 35wi 4 1
 Colors of variables: wff set class This axiom is referenced by:  axsuploc  7844
 Copyright terms: Public domain W3C validator