Metamath Proof Explorer


Theorem iooval2

Description: Value of the open interval function. (Contributed by NM, 6-Feb-2007) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion iooval2 A*B*AB=x|A<xx<B

Proof

Step Hyp Ref Expression
1 iooval A*B*AB=x*|A<xx<B
2 elioore xABx
3 2 ssriv AB
4 1 3 eqsstrrdi A*B*x*|A<xx<B
5 df-ss x*|A<xx<Bx*|A<xx<B=x*|A<xx<B
6 4 5 sylib A*B*x*|A<xx<B=x*|A<xx<B
7 inrab2 x*|A<xx<B=x*|A<xx<B
8 ressxr *
9 sseqin2 **=
10 8 9 mpbi *=
11 10 rabeqi x*|A<xx<B=x|A<xx<B
12 7 11 eqtri x*|A<xx<B=x|A<xx<B
13 6 12 eqtr3di A*B*x*|A<xx<B=x|A<xx<B
14 1 13 eqtrd A*B*AB=x|A<xx<B