Metamath Proof Explorer

Theorem icc0

Description: An empty closed interval of extended reals. (Contributed by FL, 30-May-2014)

Ref Expression
Assertion icc0 
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) )

Proof

Step Hyp Ref Expression
1 iccval 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A [,] B ) = { x e. RR* | ( A <_ x /\ x <_ B ) } )
2 1 eqeq1d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> { x e. RR* | ( A <_ x /\ x <_ B ) } = (/) ) )
3 df-ne 
 |-  ( { x e. RR* | ( A <_ x /\ x <_ B ) } =/= (/) <-> -. { x e. RR* | ( A <_ x /\ x <_ B ) } = (/) )
4 rabn0 
 |-  ( { x e. RR* | ( A <_ x /\ x <_ B ) } =/= (/) <-> E. x e. RR* ( A <_ x /\ x <_ B ) )
5 3 4 bitr3i 
 |-  ( -. { x e. RR* | ( A <_ x /\ x <_ B ) } = (/) <-> E. x e. RR* ( A <_ x /\ x <_ B ) )
6 xrletr 
 |-  ( ( A e. RR* /\ x e. RR* /\ B e. RR* ) -> ( ( A <_ x /\ x <_ B ) -> A <_ B ) )
7 6 3com23 
 |-  ( ( A e. RR* /\ B e. RR* /\ x e. RR* ) -> ( ( A <_ x /\ x <_ B ) -> A <_ B ) )
8 7 3expa 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ x e. RR* ) -> ( ( A <_ x /\ x <_ B ) -> A <_ B ) )
9 8 rexlimdva 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( E. x e. RR* ( A <_ x /\ x <_ B ) -> A <_ B ) )
10 simp2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B e. RR* )
11 simp3 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A <_ B )
12 xrleid 
 |-  ( B e. RR* -> B <_ B )
13 12 3ad2ant2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> B <_ B )
14 breq2 
 |-  ( x = B -> ( A <_ x <-> A <_ B ) )
15 breq1 
 |-  ( x = B -> ( x <_ B <-> B <_ B ) )
16 14 15 anbi12d 
 |-  ( x = B -> ( ( A <_ x /\ x <_ B ) <-> ( A <_ B /\ B <_ B ) ) )
17 16 rspcev 
 |-  ( ( B e. RR* /\ ( A <_ B /\ B <_ B ) ) -> E. x e. RR* ( A <_ x /\ x <_ B ) )
18 10 11 13 17 syl12anc 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> E. x e. RR* ( A <_ x /\ x <_ B ) )
19 18 3expia 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B -> E. x e. RR* ( A <_ x /\ x <_ B ) ) )
20 9 19 impbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( E. x e. RR* ( A <_ x /\ x <_ B ) <-> A <_ B ) )
21 5 20 syl5bb 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. { x e. RR* | ( A <_ x /\ x <_ B ) } = (/) <-> A <_ B ) )
22 xrlenlt 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B <-> -. B < A ) )
23 21 22 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. { x e. RR* | ( A <_ x /\ x <_ B ) } = (/) <-> -. B < A ) )
24 23 con4bid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( { x e. RR* | ( A <_ x /\ x <_ B ) } = (/) <-> B < A ) )
25 2 24 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) )