P. 103 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 10201-10300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	xrre 10201	A way of proving that an extended real is real. (Contributed by NM, 9-Mar-2006.)
|- ( ( ( A e. RR* /\ B e. RR ) /\ ( -oo < A /\ A <_ B ) ) -> A e. RR )
Theorem	xrre2 10202	An extended real between two others is real. (Contributed by NM, 6-Feb-2007.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B e. RR )
Theorem	xrre3 10203	A way of proving that an extended real is real. (Contributed by FL, 29-May-2014.)
|- ( ( ( A e. RR* /\ B e. RR ) /\ ( B <_ A /\ A < +oo ) ) -> A e. RR )
Theorem	ge0gtmnf 10204	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ 0 <_ A ) -> -oo < A )
Theorem	ge0nemnf 10205	A nonnegative extended real is greater than negative infinity. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ 0 <_ A ) -> A =/= -oo )
Theorem	xrrege0 10206	A nonnegative extended real that is less than a real bound is real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR ) /\ ( 0 <_ A /\ A <_ B ) ) -> A e. RR )
Theorem	z2ge 10207*	There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005.)
|- ( ( M e. ZZ /\ N e. ZZ ) -> E. k e. ZZ ( M <_ k /\ N <_ k ) )
Theorem	xnegeq 10208	Equality of two extended numbers with -e in front of them. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
|- ( A = B -> -e A = -e B )
Theorem	xnegpnf 10209	Minus +oo. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.)
|- -e +oo = -oo
Theorem	xnegmnf 10210	Minus -oo. Remark of [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Revised by Mario Carneiro, 20-Aug-2015.)
|- -e -oo = +oo
Theorem	rexneg 10211	Minus a real number. Remark [BourbakiTop1] p. IV.15. (Contributed by FL, 26-Dec-2011.) (Proof shortened by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR -> -e A = -u A )
Theorem	xneg0 10212	The negative of zero. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- -e 0 = 0
Theorem	xnegcl 10213	Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> -e A e. RR* )
Theorem	xnegneg 10214	Extended real version of negneg 8566. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> -e -e A = A )
Theorem	xneg11 10215	Extended real version of neg11 8567. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( -e A = -e B <-> A = B ) )
Theorem	xltnegi 10216	Forward direction of xltneg 10217. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* /\ A < B ) -> -e B < -e A )
Theorem	xltneg 10217	Extended real version of ltneg 8780. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -e B < -e A ) )
Theorem	xleneg 10218	Extended real version of leneg 8783. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -e B <_ -e A ) )
Theorem	xlt0neg1 10219	Extended real version of lt0neg1 8786. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> ( A < 0 <-> 0 < -e A ) )
Theorem	xlt0neg2 10220	Extended real version of lt0neg2 8787. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> ( 0 < A <-> -e A < 0 ) )
Theorem	xle0neg1 10221	Extended real version of le0neg1 8788. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( A e. RR* -> ( A <_ 0 <-> 0 <_ -e A ) )
Theorem	xle0neg2 10222	Extended real version of le0neg2 8789. (Contributed by Mario Carneiro, 9-Sep-2015.)
|- ( A e. RR* -> ( 0 <_ A <-> -e A <_ 0 ) )
Theorem	xrpnfdc 10223	An extended real is or is not plus infinity. (Contributed by Jim Kingdon, 13-Apr-2023.)
|- ( A e. RR* -> DECID A = +oo )
Theorem	xrmnfdc 10224	An extended real is or is not minus infinity. (Contributed by Jim Kingdon, 13-Apr-2023.)
|- ( A e. RR* -> DECID A = -oo )
Theorem	xaddf 10225	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- +e : ( RR* X. RR* ) --> RR*
Theorem	xaddval 10226	Value of the extended real addition operation. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) = if ( A = +oo , if ( B = -oo , 0 , +oo ) , if ( A = -oo , if ( B = +oo , 0 , -oo ) , if ( B = +oo , +oo , if ( B = -oo , -oo , ( A + B ) ) ) ) ) )
Theorem	xaddpnf1 10227	Addition of positive infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ A =/= -oo ) -> ( A +e +oo ) = +oo )
Theorem	xaddpnf2 10228	Addition of positive infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ A =/= -oo ) -> ( +oo +e A ) = +oo )
Theorem	xaddmnf1 10229	Addition of negative infinity on the right. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ A =/= +oo ) -> ( A +e -oo ) = -oo )
Theorem	xaddmnf2 10230	Addition of negative infinity on the left. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ A =/= +oo ) -> ( -oo +e A ) = -oo )
Theorem	pnfaddmnf 10231	Addition of positive and negative infinity. This is often taken to be a "null" value or out of the domain, but we define it (somewhat arbitrarily) to be zero so that the resulting function is total, which simplifies proofs. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( +oo +e -oo ) = 0
Theorem	mnfaddpnf 10232	Addition of negative and positive infinity. This is often taken to be a "null" value or out of the domain, but we define it (somewhat arbitrarily) to be zero so that the resulting function is total, which simplifies proofs. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( -oo +e +oo ) = 0
Theorem	rexadd 10233	The extended real addition operation when both arguments are real. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( A +e B ) = ( A + B ) )
Theorem	rexsub 10234	Extended real subtraction when both arguments are real. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( A e. RR /\ B e. RR ) -> ( A +e -e B ) = ( A - B ) )
Theorem	rexaddd 10235	The extended real addition operation when both arguments are real. Deduction version of rexadd 10233. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
|- ( ph -> A e. RR )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A +e B ) = ( A + B ) )
Theorem	xnegcld 10236	Closure of extended real negative. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> -e A e. RR* )
Theorem	xrex 10237	The set of extended reals exists. (Contributed by NM, 24-Dec-2006.)
|- RR* e. _V
Theorem	xaddnemnf 10238	Closure of extended real addition in the subset RR* / { -oo }. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) ) -> ( A +e B ) =/= -oo )
Theorem	xaddnepnf 10239	Closure of extended real addition in the subset RR* / { +oo }. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ A =/= +oo ) /\ ( B e. RR* /\ B =/= +oo ) ) -> ( A +e B ) =/= +oo )
Theorem	xnegid 10240	Extended real version of negid 8563. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> ( A +e -e A ) = 0 )
Theorem	xaddcl 10241	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) e. RR* )
Theorem	xaddcom 10242	The extended real addition operation is commutative. (Contributed by NM, 26-Dec-2011.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) = ( B +e A ) )
Theorem	xaddid1 10243	Extended real version of addrid 8454. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> ( A +e 0 ) = A )
Theorem	xaddid2 10244	Extended real version of addlid 8455. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( A e. RR* -> ( 0 +e A ) = A )
Theorem	xaddid1d 10245	0 is a right identity for extended real addition. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. RR* )   =>    |- ( ph -> ( A +e 0 ) = A )
Theorem	xnn0lenn0nn0 10246	An extended nonnegative integer which is less than or equal to a nonnegative integer is a nonnegative integer. (Contributed by AV, 24-Nov-2021.)
|- ( ( M e. NN0* /\ N e. NN0 /\ M <_ N ) -> M e. NN0 )
Theorem	xnn0le2is012 10247	An extended nonnegative integer which is less than or equal to 2 is either 0 or 1 or 2. (Contributed by AV, 24-Nov-2021.)
|- ( ( N e. NN0* /\ N <_ 2 ) -> ( N = 0 \/ N = 1 \/ N = 2 ) )
Theorem	xnn0xadd0 10248	The sum of two extended nonnegative integers is 0 iff each of the two extended nonnegative integers is 0. (Contributed by AV, 14-Dec-2020.)
|- ( ( A e. NN0* /\ B e. NN0* ) -> ( ( A +e B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
Theorem	xnegdi 10249	Extended real version of negdi 8573. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> -e ( A +e B ) = ( -e A +e -e B ) )
Theorem	xaddass 10250	Associativity of extended real addition. The correct condition here is "it is not the case that both +oo and -oo appear as one of A , B , C, i.e. -. { +oo , -oo } C_ { A , B , C }", but this condition is difficult to work with, so we break the theorem into two parts: this one, where -oo is not present in A , B , C, and xaddass2 10251, where +oo is not present. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\ ( C e. RR* /\ C =/= -oo ) ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )
Theorem	xaddass2 10251	Associativity of extended real addition. See xaddass 10250 for notes on the hypotheses. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ A =/= +oo ) /\ ( B e. RR* /\ B =/= +oo ) /\ ( C e. RR* /\ C =/= +oo ) ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) )
Theorem	xpncan 10252	Extended real version of pncan 8522. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR ) -> ( ( A +e B ) +e -e B ) = A )
Theorem	xnpcan 10253	Extended real version of npcan 8525. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR ) -> ( ( A +e -e B ) +e B ) = A )
Theorem	xleadd1a 10254	Extended real version of leadd1 8748; note that the converse implication is not true, unlike the real version (for example 0 < 1 but ( 1 +e +oo ) <_ ( 0 +e +oo )). (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( A +e C ) <_ ( B +e C ) )
Theorem	xleadd2a 10255	Commuted form of xleadd1a 10254. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ A <_ B ) -> ( C +e A ) <_ ( C +e B ) )
Theorem	xleadd1 10256	Weakened version of xleadd1a 10254 under which the reverse implication is true. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( A <_ B <-> ( A +e C ) <_ ( B +e C ) ) )
Theorem	xltadd1 10257	Extended real version of ltadd1 8747. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Jim Kingdon, 16-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( A < B <-> ( A +e C ) < ( B +e C ) ) )
Theorem	xltadd2 10258	Extended real version of ltadd2 8737. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* /\ C e. RR ) -> ( A < B <-> ( C +e A ) < ( C +e B ) ) )
Theorem	xaddge0 10259	The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A +e B ) )
Theorem	xle2add 10260	Extended real version of le2add 8762. (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A <_ C /\ B <_ D ) -> ( A +e B ) <_ ( C +e D ) ) )
Theorem	xlt2add 10261	Extended real version of lt2add 8763. Note that ltleadd 8764, which has weaker assumptions, is not true for the extended reals (since 0 + +oo < 1 + +oo fails). (Contributed by Mario Carneiro, 23-Aug-2015.)
|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( C e. RR* /\ D e. RR* ) ) -> ( ( A < C /\ B < D ) -> ( A +e B ) < ( C +e D ) ) )
Theorem	xsubge0 10262	Extended real version of subge0 8793. (Contributed by Mario Carneiro, 24-Aug-2015.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( 0 <_ ( A +e -e B ) <-> B <_ A ) )
Theorem	xposdif 10263	Extended real version of posdif 8773. (Contributed by Mario Carneiro, 24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> 0 < ( B +e -e A ) ) )
Theorem	xlesubadd 10264	Under certain conditions, the conclusion of lesubadd 8752 is true even in the extended reals. (Contributed by Mario Carneiro, 4-Sep-2015.)
|- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( 0 <_ A /\ B =/= -oo /\ 0 <_ C ) ) -> ( ( A +e -e B ) <_ C <-> A <_ ( C +e B ) ) )
Theorem	xaddcld 10265	The extended real addition operation is closed in extended reals. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR* )   &    |- ( ph -> B e. RR* )   =>    |- ( ph -> ( A +e B ) e. RR* )
Theorem	xadd4d 10266	Rearrangement of 4 terms in a sum for extended addition, analogous to add4d 8485. (Contributed by Alexander van der Vekens, 21-Dec-2017.)
|- ( ph -> ( A e. RR* /\ A =/= -oo ) )   &    |- ( ph -> ( B e. RR* /\ B =/= -oo ) )   &    |- ( ph -> ( C e. RR* /\ C =/= -oo ) )   &    |- ( ph -> ( D e. RR* /\ D =/= -oo ) )   =>    |- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )
Theorem	xnn0add4d 10267	Rearrangement of 4 terms in a sum for extended addition of extended nonnegative integers, analogous to xadd4d 10266. (Contributed by AV, 12-Dec-2020.)
|- ( ph -> A e. NN0* )   &    |- ( ph -> B e. NN0* )   &    |- ( ph -> C e. NN0* )   &    |- ( ph -> D e. NN0* )   =>    |- ( ph -> ( ( A +e B ) +e ( C +e D ) ) = ( ( A +e C ) +e ( B +e D ) ) )
Theorem	xleaddadd 10268	Cancelling a factor of two in <_ (expressed as addition rather than as a factor to avoid extended real multiplication). (Contributed by Jim Kingdon, 18-Apr-2023.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> ( A +e A ) <_ ( B +e B ) ) )
4.5.3  Real number intervals
Syntax	cioo 10269	Extend class notation with the set of open intervals of extended reals.
class (,)
Syntax	cioc 10270	Extend class notation with the set of open-below, closed-above intervals of extended reals.
class (,]
Syntax	cico 10271	Extend class notation with the set of closed-below, open-above intervals of extended reals.
class [,)
Syntax	cicc 10272	Extend class notation with the set of closed intervals of extended reals.
class [,]
Definition	df-ioo 10273*	Define the set of open intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
|- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
Definition	df-ioc 10274*	Define the set of open-below, closed-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
|- (,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z <_ y ) } )
Definition	df-ico 10275*	Define the set of closed-below, open-above intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
|- [,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z < y ) } )
Definition	df-icc 10276*	Define the set of closed intervals of extended reals. (Contributed by NM, 24-Dec-2006.)
|- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
Theorem	ixxval 10277*	Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- ( ( A e. RR* /\ B e. RR* ) -> ( A O B ) = { z e. RR* | ( A R z /\ z S B ) } )
Theorem	elixx1 10278*	Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A O B ) <-> ( C e. RR* /\ A R C /\ C S B ) ) )
Theorem	ixxf 10279*	The set of intervals of extended reals maps to subsets of extended reals. (Contributed by FL, 14-Jun-2007.) (Revised by Mario Carneiro, 16-Nov-2013.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- O : ( RR* X. RR* ) --> ~P RR*
Theorem	ixxex 10280*	The set of intervals of extended reals exists. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- O e. _V
Theorem	ixxssxr 10281*	The set of intervals of extended reals maps to subsets of extended reals. (Contributed by Mario Carneiro, 4-Jul-2014.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- ( A O B ) C_ RR*
Theorem	elixx3g 10282*	Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show A e. RR* and B e. RR*. (Contributed by Mario Carneiro, 3-Nov-2013.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   =>    |- ( C e. ( A O B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A R C /\ C S B ) ) )
Theorem	ixxssixx 10283*	An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   &    |- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )   &    |- ( ( A e. RR* /\ w e. RR* ) -> ( A R w -> A T w ) )   &    |- ( ( w e. RR* /\ B e. RR* ) -> ( w S B -> w U B ) )   =>    |- ( A O B ) C_ ( A P B )
Theorem	ixxdisj 10284*	Split an interval into disjoint pieces. (Contributed by Mario Carneiro, 16-Jun-2014.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   &    |- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )   &    |- ( ( B e. RR* /\ w e. RR* ) -> ( B T w <-> -. w S B ) )   =>    |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( A O B ) i^i ( B P C ) ) = (/) )
Theorem	ixxss1 10285*	Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   &    |- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z S y ) } )   &    |- ( ( A e. RR* /\ B e. RR* /\ w e. RR* ) -> ( ( A W B /\ B T w ) -> A R w ) )   =>    |- ( ( A e. RR* /\ A W B ) -> ( B P C ) C_ ( A O C ) )
Theorem	ixxss2 10286*	Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   &    |- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z T y ) } )   &    |- ( ( w e. RR* /\ B e. RR* /\ C e. RR* ) -> ( ( w T B /\ B W C ) -> w S C ) )   =>    |- ( ( C e. RR* /\ B W C ) -> ( A P B ) C_ ( A O C ) )
Theorem	ixxss12 10287*	Subset relationship for intervals of extended reals. (Contributed by Mario Carneiro, 20-Feb-2015.) (Revised by Mario Carneiro, 28-Apr-2015.)
|- O = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x R z /\ z S y ) } )   &    |- P = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x T z /\ z U y ) } )   &    |- ( ( A e. RR* /\ C e. RR* /\ w e. RR* ) -> ( ( A W C /\ C T w ) -> A R w ) )   &    |- ( ( w e. RR* /\ D e. RR* /\ B e. RR* ) -> ( ( w U D /\ D X B ) -> w S B ) )   =>    |- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A W C /\ D X B ) ) -> ( C P D ) C_ ( A O B ) )
Theorem	iooex 10288	The set of open intervals of extended reals exists. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- (,) e. _V
Theorem	iooval 10289*	Value of the open interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR* | ( A < x /\ x < B ) } )
Theorem	iooidg 10290	An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.)
|- ( A e. RR* -> ( A (,) A ) = (/) )
Theorem	elioo3g 10291	Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show A e. RR* and B e. RR*. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( C e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < C /\ C < B ) ) )
Theorem	elioo1 10292	Membership in an open interval of extended reals. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A (,) B ) <-> ( C e. RR* /\ A < C /\ C < B ) ) )
Theorem	elioore 10293	A member of an open interval of reals is a real. (Contributed by NM, 17-Aug-2008.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( A e. ( B (,) C ) -> A e. RR )
Theorem	lbioog 10294	An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
|- ( ( A e. RR* /\ B e. RR* ) -> -. A e. ( A (,) B ) )
Theorem	ubioog 10295	An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.)
|- ( ( A e. RR* /\ B e. RR* ) -> -. B e. ( A (,) B ) )
Theorem	iooval2 10296*	Value of the open interval function. (Contributed by NM, 6-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,) B ) = { x e. RR | ( A < x /\ x < B ) } )
Theorem	iooss1 10297	Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 20-Feb-2015.)
|- ( ( A e. RR* /\ A <_ B ) -> ( B (,) C ) C_ ( A (,) C ) )
Theorem	iooss2 10298	Subset relationship for open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( C e. RR* /\ B <_ C ) -> ( A (,) B ) C_ ( A (,) C ) )
Theorem	iocval 10299*	Value of the open-below, closed-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A (,] B ) = { x e. RR* | ( A < x /\ x <_ B ) } )
Theorem	icoval 10300*	Value of the closed-below, open-above interval function. (Contributed by NM, 24-Dec-2006.) (Revised by Mario Carneiro, 3-Nov-2013.)
|- ( ( A e. RR* /\ B e. RR* ) -> ( A [,) B ) = { x e. RR* | ( A <_ x /\ x < B ) } )