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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐵 𝜓 )