Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  ax-ddkcomp Unicode version

Axiom ax-ddkcomp 13176
Description: Axiom of Dedekind completeness for Dedekind real numbers: every inhabited upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then the axiom ax-ddkcomp 13176 should be used in place of construction specific results. In particular, axcaucvg 7701 should be proved from it. (Contributed by BJ, 24-Oct-2021.)
Assertion
Ref Expression
ax-ddkcomp  |-  ( ( ( A  C_  RR  /\ 
E. x  x  e.  A )  /\  E. x  e.  RR  A. y  e.  A  y  <  x  /\  A. x  e.  RR  A. y  e.  RR  ( x  < 
y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )  ->  E. x  e.  RR  ( A. y  e.  A  y  <_  x  /\  (
( B  e.  R  /\  A. y  e.  A  y  <_  B )  ->  x  <_  B ) ) )

Detailed syntax breakdown of Axiom ax-ddkcomp
StepHypRef Expression
1 cA . . . . 5  class  A
2 cr 7612 . . . . 5  class  RR
31, 2wss 3066 . . . 4  wff  A  C_  RR
4 vx . . . . . . 7  setvar  x
54cv 1330 . . . . . 6  class  x
65, 1wcel 1480 . . . . 5  wff  x  e.  A
76, 4wex 1468 . . . 4  wff  E. x  x  e.  A
83, 7wa 103 . . 3  wff  ( A 
C_  RR  /\  E. x  x  e.  A )
9 vy . . . . . . 7  setvar  y
109cv 1330 . . . . . 6  class  y
11 clt 7793 . . . . . 6  class  <
1210, 5, 11wbr 3924 . . . . 5  wff  y  < 
x
1312, 9, 1wral 2414 . . . 4  wff  A. y  e.  A  y  <  x
1413, 4, 2wrex 2415 . . 3  wff  E. x  e.  RR  A. y  e.  A  y  <  x
155, 10, 11wbr 3924 . . . . . 6  wff  x  < 
y
16 vz . . . . . . . . . 10  setvar  z
1716cv 1330 . . . . . . . . 9  class  z
185, 17, 11wbr 3924 . . . . . . . 8  wff  x  < 
z
1918, 16, 1wrex 2415 . . . . . . 7  wff  E. z  e.  A  x  <  z
2017, 10, 11wbr 3924 . . . . . . . 8  wff  z  < 
y
2120, 16, 1wral 2414 . . . . . . 7  wff  A. z  e.  A  z  <  y
2219, 21wo 697 . . . . . 6  wff  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y )
2315, 22wi 4 . . . . 5  wff  ( x  <  y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) )
2423, 9, 2wral 2414 . . . 4  wff  A. y  e.  RR  ( x  < 
y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) )
2524, 4, 2wral 2414 . . 3  wff  A. x  e.  RR  A. y  e.  RR  ( x  < 
y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) )
268, 14, 25w3a 962 . 2  wff  ( ( A  C_  RR  /\  E. x  x  e.  A
)  /\  E. x  e.  RR  A. y  e.  A  y  <  x  /\  A. x  e.  RR  A. y  e.  RR  (
x  <  y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )
27 cle 7794 . . . . . 6  class  <_
2810, 5, 27wbr 3924 . . . . 5  wff  y  <_  x
2928, 9, 1wral 2414 . . . 4  wff  A. y  e.  A  y  <_  x
30 cB . . . . . . 7  class  B
31 cR . . . . . . 7  class  R
3230, 31wcel 1480 . . . . . 6  wff  B  e.  R
3310, 30, 27wbr 3924 . . . . . . 7  wff  y  <_  B
3433, 9, 1wral 2414 . . . . . 6  wff  A. y  e.  A  y  <_  B
3532, 34wa 103 . . . . 5  wff  ( B  e.  R  /\  A. y  e.  A  y  <_  B )
365, 30, 27wbr 3924 . . . . 5  wff  x  <_  B
3735, 36wi 4 . . . 4  wff  ( ( B  e.  R  /\  A. y  e.  A  y  <_  B )  ->  x  <_  B )
3829, 37wa 103 . . 3  wff  ( A. y  e.  A  y  <_  x  /\  ( ( B  e.  R  /\  A. y  e.  A  y  <_  B )  ->  x  <_  B ) )
3938, 4, 2wrex 2415 . 2  wff  E. x  e.  RR  ( A. y  e.  A  y  <_  x  /\  ( ( B  e.  R  /\  A. y  e.  A  y  <_  B )  ->  x  <_  B ) )
4026, 39wi 4 1  wff  ( ( ( A  C_  RR  /\ 
E. x  x  e.  A )  /\  E. x  e.  RR  A. y  e.  A  y  <  x  /\  A. x  e.  RR  A. y  e.  RR  ( x  < 
y  ->  ( E. z  e.  A  x  <  z  \/  A. z  e.  A  z  <  y ) ) )  ->  E. x  e.  RR  ( A. y  e.  A  y  <_  x  /\  (
( B  e.  R  /\  A. y  e.  A  y  <_  B )  ->  x  <_  B ) ) )
Colors of variables: wff set class
This axiom is referenced by: (None)
  Copyright terms: Public domain W3C validator