Metamath Proof Explorer


Theorem iccdifprioo

Description: An open interval is the closed interval without the bounds. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion iccdifprioo A * B * A B A B = A B

Proof

Step Hyp Ref Expression
1 prunioo A * B * A B A B A B = A B
2 1 eqcomd A * B * A B A B = A B A B
3 2 difeq1d A * B * A B A B A B = A B A B A B
4 difun2 A B A B A B = A B A B
5 iooinlbub A B A B =
6 disj3 A B A B = A B = A B A B
7 5 6 mpbi A B = A B A B
8 4 7 eqtr4i A B A B A B = A B
9 3 8 eqtrdi A * B * A B A B A B = A B
10 9 3expa A * B * A B A B A B = A B
11 difssd A * B * ¬ A B A B A B A B
12 simpr A * B * ¬ A B ¬ A B
13 xrlenlt A * B * A B ¬ B < A
14 13 adantr A * B * ¬ A B A B ¬ B < A
15 12 14 mtbid A * B * ¬ A B ¬ ¬ B < A
16 15 notnotrd A * B * ¬ A B B < A
17 icc0 A * B * A B = B < A
18 17 adantr A * B * ¬ A B A B = B < A
19 16 18 mpbird A * B * ¬ A B A B =
20 11 19 sseqtrd A * B * ¬ A B A B A B
21 ss0 A B A B A B A B =
22 20 21 syl A * B * ¬ A B A B A B =
23 simplr A * B * ¬ A B B *
24 simpll A * B * ¬ A B A *
25 23 24 16 xrltled A * B * ¬ A B B A
26 ioo0 A * B * A B = B A
27 26 adantr A * B * ¬ A B A B = B A
28 25 27 mpbird A * B * ¬ A B A B =
29 22 28 eqtr4d A * B * ¬ A B A B A B = A B
30 10 29 pm2.61dan A * B * A B A B = A B