Metamath Proof Explorer

Theorem glbcl

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

Ref Expression
Hypotheses glbc.b ⊢ B = Base K
glbc.g ⊢ G = glb ⁡ K
glbc.k ⊢ φ → K ∈ V
glbc.s ⊢ φ → S ∈ dom ⁡ G
Assertion glbcl ⊢ φ → G ⁡ S ∈ B

Proof

Step Hyp Ref Expression
1 glbc.b ⊢ B = Base K
2 glbc.g ⊢ G = glb ⁡ K
3 glbc.k ⊢ φ → K ∈ V
4 glbc.s ⊢ φ → S ∈ dom ⁡ G
5 eqid ⊢ ≤ K = ≤ K
6 biid ⊢ ∀ y ∈ S x ≤ K y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ K y → z ≤ K x ↔ ∀ y ∈ S x ≤ K y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ K y → z ≤ K x
7 1 5 2 3 4 glbelss ⊢ φ → S ⊆ B
8 1 5 2 6 3 7 glbval ⊢ φ → G ⁡ S = ι x ∈ B | ∀ y ∈ S x ≤ K y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ K y → z ≤ K x
9 1 5 2 6 3 4 glbeu ⊢ φ → ∃! x ∈ B ∀ y ∈ S x ≤ K y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ K y → z ≤ K x
10 riotacl ⊢ ∃! x ∈ B ∀ y ∈ S x ≤ K y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ K y → z ≤ K x → ι x ∈ B | ∀ y ∈ S x ≤ K y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ K y → z ≤ K x ∈ B
11 9 10 syl ⊢ φ → ι x ∈ B | ∀ y ∈ S x ≤ K y ∧ ∀ z ∈ B ∀ y ∈ S z ≤ K y → z ≤ K x ∈ B
12 8 11 eqeltrd ⊢ φ → G ⁡ S ∈ B