Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. RR* ) |
2 |
|
xrleid |
|- ( A e. RR* -> A <_ A ) |
3 |
2
|
3ad2ant1 |
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A <_ A ) |
4 |
|
simp3 |
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A <_ B ) |
5 |
|
elicc1 |
|- ( ( A e. RR* /\ B e. RR* ) -> ( A e. ( A [,] B ) <-> ( A e. RR* /\ A <_ A /\ A <_ B ) ) ) |
6 |
5
|
3adant3 |
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> ( A e. ( A [,] B ) <-> ( A e. RR* /\ A <_ A /\ A <_ B ) ) ) |
7 |
1 3 4 6
|
mpbir3and |
|- ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) ) |