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

Metamath Proof Explorer

Theorem infxrge0gelb

Description: The infimum of a set of nonnegative extended reals is greater than or equal to a lower bound. (Contributed by Thierry Arnoux, 19-Jul-2020) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses infxrge0glb.a ⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,] +∞ ) )
infxrge0glb.b ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
Assertion infxrge0gelb ( 𝜑 → ( 𝐵 ≤ inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 infxrge0glb.a ⊢ ( 𝜑 → 𝐴 ⊆ ( 0 [,] +∞ ) )
2 infxrge0glb.b ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
3 1 2 infxrge0glb ⊢ ( 𝜑 → ( inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) )
4 3 notbid ⊢ ( 𝜑 → ( ¬ inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) )
5 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
6 5 2 sselid ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
7 xrltso ⊢ < Or ℝ*
8 soss ⊢ ( ( 0 [,] +∞ ) ⊆ ℝ* → ( < Or ℝ* → < Or ( 0 [,] +∞ ) ) )
9 5 7 8 mp2 ⊢ < Or ( 0 [,] +∞ )
10 9 a1i ⊢ ( 𝜑 → < Or ( 0 [,] +∞ ) )
11 xrge0infss ⊢ ( 𝐴 ⊆ ( 0 [,] +∞ ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
12 1 11 syl ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
13 10 12 infcl ⊢ ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ∈ ( 0 [,] +∞ ) )
14 5 13 sselid ⊢ ( 𝜑 → inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ∈ ℝ* )
15 6 14 xrlenltd ⊢ ( 𝜑 → ( 𝐵 ≤ inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ↔ ¬ inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ) )
16 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ* )
17 1 5 sstrdi ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
18 17 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ* )
19 16 18 xrlenltd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ≤ 𝑥 ↔ ¬ 𝑥 < 𝐵 ) )
20 19 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ) )
21 ralnex ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝑥 < 𝐵 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 )
22 20 21 bitrdi ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝑥 < 𝐵 ) )
23 4 15 22 3bitr4d ⊢ ( 𝜑 → ( 𝐵 ≤ inf ( 𝐴 , ( 0 [,] +∞ ) , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ≤ 𝑥 ) )