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

Metamath Proof Explorer

Theorem lubid

Description: The LUB of elements less than or equal to a fixed value equals that value. (Contributed by NM, 19-Oct-2011) (Revised by NM, 7-Sep-2018)

Ref Expression
Hypotheses lubid.b ⊢ B = Base K
lubid.l ⊢ ≤ ˙ = ≤ K
lubid.u ⊢ U = lub ⁡ K
lubid.k ⊢ φ → K ∈ Poset
lubid.x ⊢ φ → X ∈ B
Assertion lubid ⊢ φ → U ⁡ y ∈ B | y ≤ ˙ X = X

Proof

Step Hyp Ref Expression
1 lubid.b ⊢ B = Base K
2 lubid.l ⊢ ≤ ˙ = ≤ K
3 lubid.u ⊢ U = lub ⁡ K
4 lubid.k ⊢ φ → K ∈ Poset
5 lubid.x ⊢ φ → X ∈ B
6 biid ⊢ ∀ z ∈ y ∈ B | y ≤ ˙ X z ≤ ˙ x ∧ ∀ w ∈ B ∀ z ∈ y ∈ B | y ≤ ˙ X z ≤ ˙ w → x ≤ ˙ w ↔ ∀ z ∈ y ∈ B | y ≤ ˙ X z ≤ ˙ x ∧ ∀ w ∈ B ∀ z ∈ y ∈ B | y ≤ ˙ X z ≤ ˙ w → x ≤ ˙ w
7 ssrab2 ⊢ y ∈ B | y ≤ ˙ X ⊆ B
8 7 a1i ⊢ φ → y ∈ B | y ≤ ˙ X ⊆ B
9 1 2 3 6 4 8 lubval ⊢ φ → U ⁡ y ∈ B | y ≤ ˙ X = ι x ∈ B | ∀ z ∈ y ∈ B | y ≤ ˙ X z ≤ ˙ x ∧ ∀ w ∈ B ∀ z ∈ y ∈ B | y ≤ ˙ X z ≤ ˙ w → x ≤ ˙ w
10 1 2 3 4 5 lublecllem ⊢ φ ∧ x ∈ B → ∀ z ∈ y ∈ B | y ≤ ˙ X z ≤ ˙ x ∧ ∀ w ∈ B ∀ z ∈ y ∈ B | y ≤ ˙ X z ≤ ˙ w → x ≤ ˙ w ↔ x = X
11 5 10 riota5 ⊢ φ → ι x ∈ B | ∀ z ∈ y ∈ B | y ≤ ˙ X z ≤ ˙ x ∧ ∀ w ∈ B ∀ z ∈ y ∈ B | y ≤ ˙ X z ≤ ˙ w → x ≤ ˙ w = X
12 9 11 eqtrd ⊢ φ → U ⁡ y ∈ B | y ≤ ˙ X = X