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 ⊢ B = Base K
glbprop.l ⊢ ≤ ˙ = ≤ K
glbprop.u ⊢ U = glb ⁡ K
glbprop.k ⊢ φ → K ∈ V
glbprop.s ⊢ φ → S ∈ dom ⁡ U
glble.x ⊢ φ → X ∈ S
Assertion glble ⊢ φ → U ⁡ S ≤ ˙ X

Proof

Step Hyp Ref Expression
1 glbprop.b ⊢ B = Base K
2 glbprop.l ⊢ ≤ ˙ = ≤ K
3 glbprop.u ⊢ U = glb ⁡ K
4 glbprop.k ⊢ φ → K ∈ V
5 glbprop.s ⊢ φ → S ∈ dom ⁡ U
6 glble.x ⊢ φ → X ∈ S
7 breq2 ⊢ y = X → U ⁡ S ≤ ˙ y ↔ U ⁡ S ≤ ˙ X
8 1 2 3 4 5 glbprop ⊢ φ → ∀ y ∈ S U ⁡ S ≤ ˙ y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ ˙ y → z ≤ ˙ U ⁡ S
9 8 simpld ⊢ φ → ∀ y ∈ S U ⁡ S ≤ ˙ y
10 7 9 6 rspcdva ⊢ φ → U ⁡ S ≤ ˙ X