Theorem lubeu

Description: Unique existence proper of a member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	lubval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lubval.l	⊢ ≤ = ( le ‘ 𝐾 )
	lubval.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	lubval.p	⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
	lubval.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	lubeleu.s	⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
Assertion	lubeu	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐵 𝜓 )

Proof

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