Theorem glbeu

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

	Ref	Expression
Hypotheses	glbval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	glbval.l	⊢ ≤ = ( le ‘ 𝐾 )
	glbval.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
	glbval.p	⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
	glbva.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	glbval.s	⊢ ( 𝜑 → 𝑆 ∈ dom 𝐺 )
Assertion	glbeu	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐵 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		glbval.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		glbval.l	⊢ ≤ = ( le ‘ 𝐾 )
3		glbval.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		glbval.p	⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑥 ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ 𝑥 ) ) )
5		glbva.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
6		glbval.s	⊢ ( 𝜑 → 𝑆 ∈ dom 𝐺 )
7	1 2 3 4 5	glbeldm	⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝐺 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) )
8	6 7	mpbid	⊢ ( 𝜑 → ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
9	8	simprd	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐵 𝜓 )