Metamath Proof Explorer


Theorem eliccioo

Description: Membership in a closed interval of extended reals versus the same open interval. (Contributed by Thierry Arnoux, 18-Dec-2016)

Ref Expression
Assertion eliccioo A * B * A B C A B C = A C A B C = B

Proof

Step Hyp Ref Expression
1 prunioo A * B * A B A B A B = A B
2 1 eleq2d A * B * A B C A B A B C A B
3 2 biimpar A * B * A B C A B C A B A B
4 elun C A B A B C A B C A B
5 elprg C A B C A B C = A C = B
6 5 orbi2d C A B C A B C A B C A B C = A C = B
7 4 6 syl5bb C A B C A B A B C A B C = A C = B
8 7 adantl A * B * A B C A B C A B A B C A B C = A C = B
9 3 8 mpbid A * B * A B C A B C A B C = A C = B
10 3orass C A B C = A C = B C A B C = A C = B
11 3orcoma C A B C = A C = B C = A C A B C = B
12 10 11 bitr3i C A B C = A C = B C = A C A B C = B
13 9 12 sylib A * B * A B C A B C = A C A B C = B
14 lbicc2 A * B * A B A A B
15 14 adantr A * B * A B C = A A A B
16 eleq1 C = A C A B A A B
17 16 adantl A * B * A B C = A C A B A A B
18 15 17 mpbird A * B * A B C = A C A B
19 ioossicc A B A B
20 19 sseli C A B C A B
21 20 adantl A * B * A B C A B C A B
22 ubicc2 A * B * A B B A B
23 22 adantr A * B * A B C = B B A B
24 eleq1 C = B C A B B A B
25 24 adantl A * B * A B C = B C A B B A B
26 23 25 mpbird A * B * A B C = B C A B
27 18 21 26 3jaodan A * B * A B C = A C A B C = B C A B
28 13 27 impbida A * B * A B C A B C = A C A B C = B