Step |
Hyp |
Ref |
Expression |
1 |
|
rexr |
|- ( A e. RR -> A e. RR* ) |
2 |
|
rexr |
|- ( B e. RR -> B e. RR* ) |
3 |
|
elicc1 |
|- ( ( A e. RR* /\ B e. RR* ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ A <_ C /\ C <_ B ) ) ) |
4 |
1 2 3
|
syl2an |
|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR* /\ A <_ C /\ C <_ B ) ) ) |
5 |
|
mnfxr |
|- -oo e. RR* |
6 |
5
|
a1i |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> -oo e. RR* ) |
7 |
1
|
ad2antrr |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> A e. RR* ) |
8 |
|
simpr1 |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> C e. RR* ) |
9 |
|
mnflt |
|- ( A e. RR -> -oo < A ) |
10 |
9
|
ad2antrr |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> -oo < A ) |
11 |
|
simpr2 |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> A <_ C ) |
12 |
6 7 8 10 11
|
xrltletrd |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> -oo < C ) |
13 |
2
|
ad2antlr |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> B e. RR* ) |
14 |
|
pnfxr |
|- +oo e. RR* |
15 |
14
|
a1i |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> +oo e. RR* ) |
16 |
|
simpr3 |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> C <_ B ) |
17 |
|
ltpnf |
|- ( B e. RR -> B < +oo ) |
18 |
17
|
ad2antlr |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> B < +oo ) |
19 |
8 13 15 16 18
|
xrlelttrd |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> C < +oo ) |
20 |
|
xrrebnd |
|- ( C e. RR* -> ( C e. RR <-> ( -oo < C /\ C < +oo ) ) ) |
21 |
8 20
|
syl |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> ( C e. RR <-> ( -oo < C /\ C < +oo ) ) ) |
22 |
12 19 21
|
mpbir2and |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> C e. RR ) |
23 |
22 11 16
|
3jca |
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR* /\ A <_ C /\ C <_ B ) ) -> ( C e. RR /\ A <_ C /\ C <_ B ) ) |
24 |
23
|
ex |
|- ( ( A e. RR /\ B e. RR ) -> ( ( C e. RR* /\ A <_ C /\ C <_ B ) -> ( C e. RR /\ A <_ C /\ C <_ B ) ) ) |
25 |
|
rexr |
|- ( C e. RR -> C e. RR* ) |
26 |
25
|
3anim1i |
|- ( ( C e. RR /\ A <_ C /\ C <_ B ) -> ( C e. RR* /\ A <_ C /\ C <_ B ) ) |
27 |
24 26
|
impbid1 |
|- ( ( A e. RR /\ B e. RR ) -> ( ( C e. RR* /\ A <_ C /\ C <_ B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) ) |
28 |
4 27
|
bitrd |
|- ( ( A e. RR /\ B e. RR ) -> ( C e. ( A [,] B ) <-> ( C e. RR /\ A <_ C /\ C <_ B ) ) ) |