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

Metamath Proof Explorer

Theorem lubpr

Description: The LUB of the set of two comparable elements in a poset is the greater one of the two. (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Hypotheses lubpr.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
lubpr.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lubpr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
lubpr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
lubpr.l ⊢ ≤ = ( le ‘ 𝐾 )
lubpr.c ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
lubpr.s ⊢ ( 𝜑 → 𝑆 = { 𝑋 , 𝑌 } )
lubpr.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
Assertion lubpr ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = 𝑌 )

Proof

Step Hyp Ref Expression
1 lubpr.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
2 lubpr.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
3 lubpr.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 lubpr.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5 lubpr.l ⊢ ≤ = ( le ‘ 𝐾 )
6 lubpr.c ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
7 lubpr.s ⊢ ( 𝜑 → 𝑆 = { 𝑋 , 𝑌 } )
8 lubpr.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
9 1 2 3 4 5 6 7 8 lubprlem ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ∧ ( 𝑈 ‘ 𝑆 ) = 𝑌 ) )
10 9 simprd ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = 𝑌 )