Metamath Proof Explorer


Theorem infxrge0glb

Description: The infimum of a set of nonnegative extended reals is the greatest 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 infxrge0glb ( 𝜑 → ( inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ∃ 𝑥𝐴 𝑥 < 𝐵 ) )

Proof

Step Hyp Ref Expression
1 infxrge0glb.a ( 𝜑𝐴 ⊆ ( 0 [,] +∞ ) )
2 infxrge0glb.b ( 𝜑𝐵 ∈ ( 0 [,] +∞ ) )
3 iccssxr ( 0 [,] +∞ ) ⊆ ℝ*
4 xrltso < Or ℝ*
5 soss ( ( 0 [,] +∞ ) ⊆ ℝ* → ( < Or ℝ* → < Or ( 0 [,] +∞ ) ) )
6 3 4 5 mp2 < Or ( 0 [,] +∞ )
7 6 a1i ( 𝜑 → < Or ( 0 [,] +∞ ) )
8 xrge0infss ( 𝐴 ⊆ ( 0 [,] +∞ ) → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
9 1 8 syl ( 𝜑 → ∃ 𝑥 ∈ ( 0 [,] +∞ ) ( ∀ 𝑦𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ( 0 [,] +∞ ) ( 𝑥 < 𝑦 → ∃ 𝑧𝐴 𝑧 < 𝑦 ) ) )
10 7 9 1 infglbb ( ( 𝜑𝐵 ∈ ( 0 [,] +∞ ) ) → ( inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ∃ 𝑧𝐴 𝑧 < 𝐵 ) )
11 2 10 mpdan ( 𝜑 → ( inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ∃ 𝑧𝐴 𝑧 < 𝐵 ) )
12 breq1 ( 𝑥 = 𝑧 → ( 𝑥 < 𝐵𝑧 < 𝐵 ) )
13 12 cbvrexvw ( ∃ 𝑥𝐴 𝑥 < 𝐵 ↔ ∃ 𝑧𝐴 𝑧 < 𝐵 )
14 11 13 bitr4di ( 𝜑 → ( inf ( 𝐴 , ( 0 [,] +∞ ) , < ) < 𝐵 ↔ ∃ 𝑥𝐴 𝑥 < 𝐵 ) )