Description: 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)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | elioo3g | |- ( C e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < C /\ C < B ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-ioo | |- (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } ) |
|
| 2 | 1 | elixx3g | |- ( C e. ( A (,) B ) <-> ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < C /\ C < B ) ) ) |