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	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )