Metamath Proof Explorer

Theorem ioossioobi

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

Ref Expression
Hypotheses ioossioobi.a ⊢φ→A∈ℝ*
ioossioobi.b ⊢φ→B∈ℝ*
ioossioobi.c ⊢φ→C∈ℝ*
ioossioobi.d ⊢φ→D∈ℝ*
ioossioobi.cltd ⊢φ→C<D
Assertion ioossioobi ⊢φ→CD⊆AB↔A≤C∧D≤B

Proof

Step Hyp Ref Expression
1 ioossioobi.a ⊢φ→A∈ℝ*
2 ioossioobi.b ⊢φ→B∈ℝ*
3 ioossioobi.c ⊢φ→C∈ℝ*
4 ioossioobi.d ⊢φ→D∈ℝ*
5 ioossioobi.cltd ⊢φ→C<D
6 simpr ⊢φ∧CD⊆AB→CD⊆AB
7 df-ioo ⊢.=x∈ℝ*,y∈ℝ*⟼z∈ℝ*|x<z∧z<y
8 7 ixxssxr ⊢AB⊆ℝ*
9 infxrss ⊢CD⊆AB∧AB⊆ℝ*→supABℝ*<≤supCDℝ*<
10 6 8 9 sylancl ⊢φ∧CD⊆AB→supABℝ*<≤supCDℝ*<
11 1 adantr ⊢φ∧CD⊆AB→A∈ℝ*
12 2 adantr ⊢φ∧CD⊆AB→B∈ℝ*
13 ioon0 ⊢C∈ℝ*∧D∈ℝ*→CD≠∅↔C<D
14 3 4 13 syl2anc ⊢φ→CD≠∅↔C<D
15 5 14 mpbird ⊢φ→CD≠∅
16 15 adantr ⊢φ∧CD⊆AB→CD≠∅
17 ssn0 ⊢CD⊆AB∧CD≠∅→AB≠∅
18 6 16 17 syl2anc ⊢φ∧CD⊆AB→AB≠∅
19 idd ⊢w∈ℝ*∧B∈ℝ*→w<B→w<B
20 xrltle ⊢w∈ℝ*∧B∈ℝ*→w<B→w≤B
21 idd ⊢A∈ℝ*∧w∈ℝ*→A<w→A<w
22 xrltle ⊢A∈ℝ*∧w∈ℝ*→A<w→A≤w
23 7 19 20 21 22 ixxlb ⊢A∈ℝ*∧B∈ℝ*∧AB≠∅→supABℝ*<=A
24 11 12 18 23 syl3anc ⊢φ∧CD⊆AB→supABℝ*<=A
25 3 adantr ⊢φ∧CD⊆AB→C∈ℝ*
26 4 adantr ⊢φ∧CD⊆AB→D∈ℝ*
27 idd ⊢w∈ℝ*∧D∈ℝ*→w<D→w<D
28 xrltle ⊢w∈ℝ*∧D∈ℝ*→w<D→w≤D
29 idd ⊢C∈ℝ*∧w∈ℝ*→C<w→C<w
30 xrltle ⊢C∈ℝ*∧w∈ℝ*→C<w→C≤w
31 7 27 28 29 30 ixxlb ⊢C∈ℝ*∧D∈ℝ*∧CD≠∅→supCDℝ*<=C
32 25 26 16 31 syl3anc ⊢φ∧CD⊆AB→supCDℝ*<=C
33 10 24 32 3brtr3d ⊢φ∧CD⊆AB→A≤C
34 supxrss ⊢CD⊆AB∧AB⊆ℝ*→supCDℝ*<≤supABℝ*<
35 6 8 34 sylancl ⊢φ∧CD⊆AB→supCDℝ*<≤supABℝ*<
36 7 27 28 29 30 ixxub ⊢C∈ℝ*∧D∈ℝ*∧CD≠∅→supCDℝ*<=D
37 25 26 16 36 syl3anc ⊢φ∧CD⊆AB→supCDℝ*<=D
38 7 19 20 21 22 ixxub ⊢A∈ℝ*∧B∈ℝ*∧AB≠∅→supABℝ*<=B
39 11 12 18 38 syl3anc ⊢φ∧CD⊆AB→supABℝ*<=B
40 35 37 39 3brtr3d ⊢φ∧CD⊆AB→D≤B
41 33 40 jca ⊢φ∧CD⊆AB→A≤C∧D≤B
42 1 adantr ⊢φ∧A≤C∧D≤B→A∈ℝ*
43 2 adantr ⊢φ∧A≤C∧D≤B→B∈ℝ*
44 simprl ⊢φ∧A≤C∧D≤B→A≤C
45 simprr ⊢φ∧A≤C∧D≤B→D≤B
46 ioossioo ⊢A∈ℝ*∧B∈ℝ*∧A≤C∧D≤B→CD⊆AB
47 42 43 44 45 46 syl22anc ⊢φ∧A≤C∧D≤B→CD⊆AB
48 41 47 impbida ⊢φ→CD⊆AB↔A≤C∧D≤B