Metamath Proof Explorer

Theorem elioomnf

Description: Membership in an unbounded interval of extended reals. (Contributed by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion elioomnf 
|- ( A e. RR* -> ( B e. ( -oo (,) A ) <-> ( B e. RR /\ B < A ) ) )

Proof

Step Hyp Ref Expression
1 mnfxr 
 |-  -oo e. RR*
2 elioo2 
 |-  ( ( -oo e. RR* /\ A e. RR* ) -> ( B e. ( -oo (,) A ) <-> ( B e. RR /\ -oo < B /\ B < A ) ) )
3 1 2 mpan 
 |-  ( A e. RR* -> ( B e. ( -oo (,) A ) <-> ( B e. RR /\ -oo < B /\ B < A ) ) )
4 an32 
 |-  ( ( ( B e. RR /\ -oo < B ) /\ B < A ) <-> ( ( B e. RR /\ B < A ) /\ -oo < B ) )
5 df-3an 
 |-  ( ( B e. RR /\ -oo < B /\ B < A ) <-> ( ( B e. RR /\ -oo < B ) /\ B < A ) )
6 mnflt 
 |-  ( B e. RR -> -oo < B )
7 6 adantr 
 |-  ( ( B e. RR /\ B < A ) -> -oo < B )
8 7 pm4.71i 
 |-  ( ( B e. RR /\ B < A ) <-> ( ( B e. RR /\ B < A ) /\ -oo < B ) )
9 4 5 8 3bitr4i 
 |-  ( ( B e. RR /\ -oo < B /\ B < A ) <-> ( B e. RR /\ B < A ) )
10 3 9 bitrdi 
 |-  ( A e. RR* -> ( B e. ( -oo (,) A ) <-> ( B e. RR /\ B < A ) ) )