Metamath Proof Explorer


Theorem ixxssixx

Description: An interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Hypotheses ixx.1 O=x*,y*z*|xRzzSy
ixx.2 P=x*,y*z*|xTzzUy
ixx.3 A*w*ARwATw
ixx.4 w*B*wSBwUB
Assertion ixxssixx AOBAPB

Proof

Step Hyp Ref Expression
1 ixx.1 O=x*,y*z*|xRzzSy
2 ixx.2 P=x*,y*z*|xTzzUy
3 ixx.3 A*w*ARwATw
4 ixx.4 w*B*wSBwUB
5 1 elmpocl wAOBA*B*
6 simp1 w*ARwwSBw*
7 6 a1i A*B*w*ARwwSBw*
8 simpl A*B*A*
9 3simpa w*ARwwSBw*ARw
10 3 expimpd A*w*ARwATw
11 8 9 10 syl2im A*B*w*ARwwSBATw
12 simpr A*B*B*
13 3simpb w*ARwwSBw*wSB
14 4 ancoms B*w*wSBwUB
15 14 expimpd B*w*wSBwUB
16 12 13 15 syl2im A*B*w*ARwwSBwUB
17 7 11 16 3jcad A*B*w*ARwwSBw*ATwwUB
18 1 elixx1 A*B*wAOBw*ARwwSB
19 2 elixx1 A*B*wAPBw*ATwwUB
20 17 18 19 3imtr4d A*B*wAOBwAPB
21 5 20 mpcom wAOBwAPB
22 21 ssriv AOBAPB