Metamath Proof Explorer

Theorem ioossioobi

Description: Biconditional form of ioossioo . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ioossioobi.a 
|- ( ph -> A e. RR* )
ioossioobi.b 
|- ( ph -> B e. RR* )
ioossioobi.c 
|- ( ph -> C e. RR* )
ioossioobi.d 
|- ( ph -> D e. RR* )
ioossioobi.cltd 
|- ( ph -> C < D )
Assertion ioossioobi 
|- ( ph -> ( ( C (,) D ) C_ ( A (,) B ) <-> ( A <_ C /\ D <_ B ) ) )

Proof

Step Hyp Ref Expression
1 ioossioobi.a 
 |-  ( ph -> A e. RR* )
2 ioossioobi.b 
 |-  ( ph -> B e. RR* )
3 ioossioobi.c 
 |-  ( ph -> C e. RR* )
4 ioossioobi.d 
 |-  ( ph -> D e. RR* )
5 ioossioobi.cltd 
 |-  ( ph -> C < D )
6 simpr 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> ( C (,) D ) C_ ( A (,) B ) )
7 df-ioo 
 |-  (,) = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x < z /\ z < y ) } )
8 7 ixxssxr 
 |-  ( A (,) B ) C_ RR*
9 infxrss 
 |-  ( ( ( C (,) D ) C_ ( A (,) B ) /\ ( A (,) B ) C_ RR* ) -> inf ( ( A (,) B ) , RR* , < ) <_ inf ( ( C (,) D ) , RR* , < ) )
10 6 8 9 sylancl 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> inf ( ( A (,) B ) , RR* , < ) <_ inf ( ( C (,) D ) , RR* , < ) )
11 1 adantr 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> A e. RR* )
12 2 adantr 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> B e. RR* )
13 ioon0 
 |-  ( ( C e. RR* /\ D e. RR* ) -> ( ( C (,) D ) =/= (/) <-> C < D ) )
14 3 4 13 syl2anc 
 |-  ( ph -> ( ( C (,) D ) =/= (/) <-> C < D ) )
15 5 14 mpbird 
 |-  ( ph -> ( C (,) D ) =/= (/) )
16 15 adantr 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> ( C (,) D ) =/= (/) )
17 ssn0 
 |-  ( ( ( C (,) D ) C_ ( A (,) B ) /\ ( C (,) D ) =/= (/) ) -> ( A (,) B ) =/= (/) )
18 6 16 17 syl2anc 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> ( A (,) B ) =/= (/) )
19 idd 
 |-  ( ( w e. RR* /\ B e. RR* ) -> ( w < B -> w < B ) )
20 xrltle 
 |-  ( ( w e. RR* /\ B e. RR* ) -> ( w < B -> w <_ B ) )
21 idd 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A < w ) )
22 xrltle 
 |-  ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A <_ w ) )
23 7 19 20 21 22 ixxlb 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A (,) B ) =/= (/) ) -> inf ( ( A (,) B ) , RR* , < ) = A )
24 11 12 18 23 syl3anc 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> inf ( ( A (,) B ) , RR* , < ) = A )
25 3 adantr 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> C e. RR* )
26 4 adantr 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> D e. RR* )
27 idd 
 |-  ( ( w e. RR* /\ D e. RR* ) -> ( w < D -> w < D ) )
28 xrltle 
 |-  ( ( w e. RR* /\ D e. RR* ) -> ( w < D -> w <_ D ) )
29 idd 
 |-  ( ( C e. RR* /\ w e. RR* ) -> ( C < w -> C < w ) )
30 xrltle 
 |-  ( ( C e. RR* /\ w e. RR* ) -> ( C < w -> C <_ w ) )
31 7 27 28 29 30 ixxlb 
 |-  ( ( C e. RR* /\ D e. RR* /\ ( C (,) D ) =/= (/) ) -> inf ( ( C (,) D ) , RR* , < ) = C )
32 25 26 16 31 syl3anc 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> inf ( ( C (,) D ) , RR* , < ) = C )
33 10 24 32 3brtr3d 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> A <_ C )
34 supxrss 
 |-  ( ( ( C (,) D ) C_ ( A (,) B ) /\ ( A (,) B ) C_ RR* ) -> sup ( ( C (,) D ) , RR* , < ) <_ sup ( ( A (,) B ) , RR* , < ) )
35 6 8 34 sylancl 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> sup ( ( C (,) D ) , RR* , < ) <_ sup ( ( A (,) B ) , RR* , < ) )
36 7 27 28 29 30 ixxub 
 |-  ( ( C e. RR* /\ D e. RR* /\ ( C (,) D ) =/= (/) ) -> sup ( ( C (,) D ) , RR* , < ) = D )
37 25 26 16 36 syl3anc 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> sup ( ( C (,) D ) , RR* , < ) = D )
38 7 19 20 21 22 ixxub 
 |-  ( ( A e. RR* /\ B e. RR* /\ ( A (,) B ) =/= (/) ) -> sup ( ( A (,) B ) , RR* , < ) = B )
39 11 12 18 38 syl3anc 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> sup ( ( A (,) B ) , RR* , < ) = B )
40 35 37 39 3brtr3d 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> D <_ B )
41 33 40 jca 
 |-  ( ( ph /\ ( C (,) D ) C_ ( A (,) B ) ) -> ( A <_ C /\ D <_ B ) )
42 1 adantr 
 |-  ( ( ph /\ ( A <_ C /\ D <_ B ) ) -> A e. RR* )
43 2 adantr 
 |-  ( ( ph /\ ( A <_ C /\ D <_ B ) ) -> B e. RR* )
44 simprl 
 |-  ( ( ph /\ ( A <_ C /\ D <_ B ) ) -> A <_ C )
45 simprr 
 |-  ( ( ph /\ ( A <_ C /\ D <_ B ) ) -> D <_ B )
46 ioossioo 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( A <_ C /\ D <_ B ) ) -> ( C (,) D ) C_ ( A (,) B ) )
47 42 43 44 45 46 syl22anc 
 |-  ( ( ph /\ ( A <_ C /\ D <_ B ) ) -> ( C (,) D ) C_ ( A (,) B ) )
48 41 47 impbida 
 |-  ( ph -> ( ( C (,) D ) C_ ( A (,) B ) <-> ( A <_ C /\ D <_ B ) ) )