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

Metamath Proof Explorer

Theorem glble

Description: The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011) (Revised by NM, 7-Sep-2018)

Ref Expression
Hypotheses glbprop.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
glbprop.l ⊢ ≤ = ( le ‘ 𝐾 )
glbprop.u ⊢ 𝑈 = ( glb ‘ 𝐾 )
glbprop.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
glbprop.s ⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
glble.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
Assertion glble ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 )

Proof

Step Hyp Ref Expression
1 glbprop.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 glbprop.l ⊢ ≤ = ( le ‘ 𝐾 )
3 glbprop.u ⊢ 𝑈 = ( glb ‘ 𝐾 )
4 glbprop.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
5 glbprop.s ⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
6 glble.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
7 breq2 ⊢ ( 𝑦 = 𝑋 → ( ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ↔ ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 ) )
8 1 2 3 4 5 glbprop ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝑈 ‘ 𝑆 ) ) ) )
9 8 simpld ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 )
10 7 9 6 rspcdva ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 )