Metamath Proof Explorer

Theorem ioo0

Description: An empty open interval of extended reals. (Contributed by NM, 6-Feb-2007)

Ref Expression
Assertion ioo0 
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )

Proof

Step Hyp Ref Expression
1 iooval 
 |-  ( ( 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 xrlttr 
 |-  ( ( 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 qbtwnxr 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. x e. QQ ( A < x /\ x < B ) )
11 qre 
 |-  ( x e. QQ -> x e. RR )
12 11 rexrd 
 |-  ( x e. QQ -> x e. RR* )
13 12 anim1i 
 |-  ( ( x e. QQ /\ ( A < x /\ x < B ) ) -> ( x e. RR* /\ ( A < x /\ x < B ) ) )
14 13 reximi2 
 |-  ( E. x e. QQ ( A < x /\ x < B ) -> E. x e. RR* ( A < x /\ x < B ) )
15 10 14 syl 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. x e. RR* ( A < x /\ x < B ) )
16 15 3expia 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> E. x e. RR* ( A < x /\ x < B ) ) )
17 9 16 impbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( E. x e. RR* ( A < x /\ x < B ) <-> A < B ) )
18 5 17 syl5bb 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. { x e. RR* | ( A < x /\ x < B ) } = (/) <-> A < B ) )
19 xrltnle 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -. B <_ A ) )
20 18 19 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. { x e. RR* | ( A < x /\ x < B ) } = (/) <-> -. B <_ A ) )
21 20 con4bid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( { x e. RR* | ( A < x /\ x < B ) } = (/) <-> B <_ A ) )
22 2 21 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,) B ) = (/) <-> B <_ A ) )