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 ⊢ 𝐵 = ( Base ‘ 𝐾 )
lubs.l ⊢ ≤ = ( le ‘ 𝐾 )
lubs.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
lubs.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
lubs.s ⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
Assertion lubelss ( 𝜑 → 𝑆 ⊆ 𝐵 )

Proof

Step Hyp Ref Expression
1 lubs.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lubs.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lubs.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 lubs.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
5 lubs.s ⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
6 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
7 1 2 3 6 4 lubeldm ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) ) )
8 5 7 mpbid ⊢ ( 𝜑 → ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) )
9 8 simpld ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )