Metamath Proof Explorer

Theorem lubcl

Description: The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018)

Ref Expression
Hypotheses lubcl.b ⊢ B = Base K
lubcl.u ⊢ U = lub ⁡ K
lubcl.k ⊢ φ → K ∈ V
lubcl.s ⊢ φ → S ∈ dom ⁡ U
Assertion lubcl ⊢ φ → U ⁡ S ∈ B

Proof

Step Hyp Ref Expression
1 lubcl.b ⊢ B = Base K
2 lubcl.u ⊢ U = lub ⁡ K
3 lubcl.k ⊢ φ → K ∈ V
4 lubcl.s ⊢ φ → S ∈ dom ⁡ U
5 eqid ⊢ ≤ K = ≤ K
6 biid ⊢ ∀ y ∈ S y ≤ K x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ K z → x ≤ K z ↔ ∀ y ∈ S y ≤ K x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ K z → x ≤ K z
7 1 5 2 3 4 lubelss ⊢ φ → S ⊆ B
8 1 5 2 6 3 7 lubval ⊢ φ → U ⁡ S = ι x ∈ B | ∀ y ∈ S y ≤ K x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ K z → x ≤ K z
9 1 5 2 6 3 4 lubeu ⊢ φ → ∃! x ∈ B ∀ y ∈ S y ≤ K x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ K z → x ≤ K z
10 riotacl ⊢ ∃! x ∈ B ∀ y ∈ S y ≤ K x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ K z → x ≤ K z → ι x ∈ B | ∀ y ∈ S y ≤ K x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ K z → x ≤ K z ∈ B
11 9 10 syl ⊢ φ → ι x ∈ B | ∀ y ∈ S y ≤ K x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ K z → x ≤ K z ∈ B
12 8 11 eqeltrd ⊢ φ → U ⁡ S ∈ B