Metamath Proof Explorer

Theorem ico0

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

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

Proof

Step Hyp Ref Expression
1 icoval 
 |-  ( ( 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 xrlelttr 
 |-  ( ( 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 simpr1 
 |-  ( ( x e. RR* /\ ( A e. RR* /\ B e. RR* /\ A < B ) ) -> A e. RR* )
15 simpl 
 |-  ( ( x e. RR* /\ ( A e. RR* /\ B e. RR* /\ A < B ) ) -> x e. RR* )
16 xrltle 
 |-  ( ( A e. RR* /\ x e. RR* ) -> ( A < x -> A <_ x ) )
17 14 15 16 syl2anc 
 |-  ( ( x e. RR* /\ ( A e. RR* /\ B e. RR* /\ A < B ) ) -> ( A < x -> A <_ x ) )
18 17 anim1d 
 |-  ( ( x e. RR* /\ ( A e. RR* /\ B e. RR* /\ A < B ) ) -> ( ( A < x /\ x < B ) -> ( A <_ x /\ x < B ) ) )
19 13 18 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 ) ) ) )
20 19 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 ) ) ) ) )
21 12 20 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 ) ) ) ) )
22 21 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 ) ) ) ) )
23 22 pm2.43b 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> ( ( x e. QQ /\ ( A < x /\ x < B ) ) -> ( x e. RR* /\ ( A <_ x /\ x < B ) ) ) )
24 23 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 ) ) )
25 10 24 mpd 
 |-  ( ( A e. RR* /\ B e. RR* /\ A < B ) -> E. x e. RR* ( A <_ x /\ x < B ) )
26 25 3expia 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B -> E. x e. RR* ( A <_ x /\ x < B ) ) )
27 9 26 impbid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( E. x e. RR* ( A <_ x /\ x < B ) <-> A < B ) )
28 5 27 syl5bb 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. { x e. RR* | ( A <_ x /\ x < B ) } = (/) <-> A < B ) )
29 xrltnle 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> -. B <_ A ) )
30 28 29 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( -. { x e. RR* | ( A <_ x /\ x < B ) } = (/) <-> -. B <_ A ) )
31 30 con4bid 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( { x e. RR* | ( A <_ x /\ x < B ) } = (/) <-> B <_ A ) )
32 2 31 bitrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,) B ) = (/) <-> B <_ A ) )