This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ioossioobi

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

Ref Expression
Hypotheses ioossioobi.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
ioossioobi.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
ioossioobi.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
ioossioobi.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
ioossioobi.cltd ⊢ ( 𝜑 → 𝐶 < 𝐷 )
Assertion ioossioobi ( 𝜑 → ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ioossioobi.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 ioossioobi.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 ioossioobi.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
4 ioossioobi.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ* )
5 ioossioobi.cltd ⊢ ( 𝜑 → 𝐶 < 𝐷 )
6 simpr ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
7 df-ioo ⊢ (,) = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
8 7 ixxssxr ⊢ ( 𝐴 (,) 𝐵 ) ⊆ ℝ*
9 infxrss ⊢ ( ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ* ) → inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) ≤ inf ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) )
10 6 8 9 sylancl ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) ≤ inf ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ∈ ℝ* )
12 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐵 ∈ ℝ* )
13 ioon0 ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( ( 𝐶 (,) 𝐷 ) ≠ ∅ ↔ 𝐶 < 𝐷 ) )
14 3 4 13 syl2anc ⊢ ( 𝜑 → ( ( 𝐶 (,) 𝐷 ) ≠ ∅ ↔ 𝐶 < 𝐷 ) )
15 5 14 mpbird ⊢ ( 𝜑 → ( 𝐶 (,) 𝐷 ) ≠ ∅ )
16 15 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → ( 𝐶 (,) 𝐷 ) ≠ ∅ )
17 ssn0 ⊢ ( ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐶 (,) 𝐷 ) ≠ ∅ ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
18 6 16 17 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 (,) 𝐵 ) ≠ ∅ )
19 idd ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑤 < 𝐵 → 𝑤 < 𝐵 ) )
20 xrltle ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑤 < 𝐵 → 𝑤 ≤ 𝐵 ) )
21 idd ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤 → 𝐴 < 𝑤 ) )
22 xrltle ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐴 < 𝑤 → 𝐴 ≤ 𝑤 ) )
23 7 19 20 21 22 ixxlb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 (,) 𝐵 ) ≠ ∅ ) → inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐴 )
24 11 12 18 23 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → inf ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐴 )
25 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐶 ∈ ℝ* )
26 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐷 ∈ ℝ* )
27 idd ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( 𝑤 < 𝐷 → 𝑤 < 𝐷 ) )
28 xrltle ⊢ ( ( 𝑤 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ) → ( 𝑤 < 𝐷 → 𝑤 ≤ 𝐷 ) )
29 idd ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐶 < 𝑤 → 𝐶 < 𝑤 ) )
30 xrltle ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝐶 < 𝑤 → 𝐶 ≤ 𝑤 ) )
31 7 27 28 29 30 ixxlb ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ ( 𝐶 (,) 𝐷 ) ≠ ∅ ) → inf ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) = 𝐶 )
32 25 26 16 31 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → inf ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) = 𝐶 )
33 10 24 32 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐴 ≤ 𝐶 )
34 supxrss ⊢ ( ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ∧ ( 𝐴 (,) 𝐵 ) ⊆ ℝ* ) → sup ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) ≤ sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) )
35 6 8 34 sylancl ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → sup ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) ≤ sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) )
36 7 27 28 29 30 ixxub ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐷 ∈ ℝ* ∧ ( 𝐶 (,) 𝐷 ) ≠ ∅ ) → sup ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) = 𝐷 )
37 25 26 16 36 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → sup ( ( 𝐶 (,) 𝐷 ) , ℝ* , < ) = 𝐷 )
38 7 19 20 21 22 ixxub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝐴 (,) 𝐵 ) ≠ ∅ ) → sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐵 )
39 11 12 18 38 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → sup ( ( 𝐴 (,) 𝐵 ) , ℝ* , < ) = 𝐵 )
40 35 37 39 3brtr3d ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → 𝐷 ≤ 𝐵 )
41 33 40 jca ⊢ ( ( 𝜑 ∧ ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ) → ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) )
42 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐴 ∈ ℝ* )
43 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐵 ∈ ℝ* )
44 simprl ⊢ ( ( 𝜑 ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐴 ≤ 𝐶 )
45 simprr ⊢ ( ( 𝜑 ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → 𝐷 ≤ 𝐵 )
46 ioossioo ⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
47 42 43 44 45 46 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) → ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) )
48 41 47 impbida ⊢ ( 𝜑 → ( ( 𝐶 (,) 𝐷 ) ⊆ ( 𝐴 (,) 𝐵 ) ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐷 ≤ 𝐵 ) ) )