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

Metamath Proof Explorer

Theorem luble

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

Ref Expression
Hypotheses lubprop.b ⊢ B = Base K
lubprop.l ⊢ ≤ ˙ = ≤ K
lubprop.u ⊢ U = lub ⁡ K
lubprop.k ⊢ φ → K ∈ V
lubprop.s ⊢ φ → S ∈ dom ⁡ U
luble.x ⊢ φ → X ∈ S
Assertion luble ⊢ φ → X ≤ ˙ U ⁡ S

Proof

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