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

Metamath Proof Explorer

Theorem lubelss

Description: A member of the domain of the least upper bound function is a subset of the base set. (Contributed by NM, 7-Sep-2018)

Ref Expression
Hypotheses lubs.b ⊢ B = Base K
lubs.l ⊢ ≤ ˙ = ≤ K
lubs.u ⊢ U = lub ⁡ K
lubs.k ⊢ φ → K ∈ V
lubs.s ⊢ φ → S ∈ dom ⁡ U
Assertion lubelss ⊢ φ → S ⊆ B

Proof

Step Hyp Ref Expression
1 lubs.b ⊢ B = Base K
2 lubs.l ⊢ ≤ ˙ = ≤ K
3 lubs.u ⊢ U = lub ⁡ K
4 lubs.k ⊢ φ → K ∈ V
5 lubs.s ⊢ φ → S ∈ dom ⁡ U
6 biid ⊢ ∀ y ∈ S y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ ˙ z → x ≤ ˙ z ↔ ∀ y ∈ S y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ ˙ z → x ≤ ˙ z
7 1 2 3 6 4 lubeldm ⊢ φ → S ∈ dom ⁡ U ↔ S ⊆ B ∧ ∃! x ∈ B ∀ y ∈ S y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ ˙ z → x ≤ ˙ z
8 5 7 mpbid ⊢ φ → S ⊆ B ∧ ∃! x ∈ B ∀ y ∈ S y ≤ ˙ x ∧ ∀ z ∈ B ∀ y ∈ S y ≤ ˙ z → x ≤ ˙ z
9 8 simpld ⊢ φ → S ⊆ B