Metamath Proof Explorer

Theorem ioc0

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

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

Proof

Step Hyp Ref Expression
1 iocval 
 |-  ( ( 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 xrltletr 
 |-  ( ( 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 a1i 
 |-  ( ( x e. RR* /\ ( A e. RR* /\ B e. RR* /\ A < B ) ) -> ( x e. QQ -> x e. RR* ) )
14 xrltle 
 |-  ( ( x e. RR* /\ B e. RR* ) -> ( x < B -> x <_ B ) )
15 14 3ad2antr2 
 |-  ( ( x e. RR* /\ ( A e. RR* /\ B e. RR* /\ A < B ) ) -> ( x < B -> x <_ B ) )
16 15 anim2d 
 |-  ( ( x e. RR* /\ ( A e. RR* /\ B e. RR* /\ A < B ) ) -> ( ( A < x /\ x < B ) -> ( A < x /\ x <_ B ) ) )
17 13 16 anim12d 
 |-  ( ( x e. RR* /\ ( A e. RR* /\ B e. RR* /\ A < B ) ) -> ( ( x e. QQ /\ ( A < x /\ x < B ) ) -> ( x e. RR* /\ ( A < x /\ x <_ B ) ) ) )
18 17 ex 
 |-  ( x e. RR* -> ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( x e. QQ /\ ( A < x /\ x < B ) ) -> ( x e. RR* /\ ( A < x /\ x <_ B ) ) ) ) )
19 12 18 syl 
 |-  ( x e. QQ -> ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( x e. QQ /\ ( A < x /\ x < B ) ) -> ( x e. RR* /\ ( A < x /\ x <_ B ) ) ) ) )
20 19 adantr 
 |-  ( ( x e. QQ /\ ( A < x /\ x < B ) ) -> ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( x e. QQ /\ ( A < x /\ x < B ) ) -> ( x e. RR* /\ ( A < x /\ x <_ B ) ) ) ) )
21 20 pm2.43b 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( x e. QQ /\ ( A < x /\ x < B ) ) -> ( x e. RR* /\ ( A < x /\ x <_ B ) ) ) )
22 21 reximdv2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( E. x e. QQ ( A < x /\ x < B ) -> E. x e. RR* ( A < x /\ x <_ B ) ) )
23 10 22 mpd 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. x e. RR* ( A < x /\ x <_ B ) )
24 23 3expia 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> E. x e. RR* ( A < x /\ x <_ B ) ) )
25 9 24 impbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( E. x e. RR* ( A < x /\ x <_ B ) <-> A < B ) )
26 5 25 syl5bb 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. { x e. RR* | ( A < x /\ x <_ B ) } = (/) <-> A < B ) )
27 xrltnle 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -. B <_ A ) )
28 26 27 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. { x e. RR* | ( A < x /\ x <_ B ) } = (/) <-> -. B <_ A ) )
29 28 con4bid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( { x e. RR* | ( A < x /\ x <_ B ) } = (/) <-> B <_ A ) )
30 2 29 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A (,] B ) = (/) <-> B <_ A ) )