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
|- ( ph -> K e. Poset )
lubpr.b
|- B = ( Base ` K )
lubpr.x
|- ( ph -> X e. B )
lubpr.y
|- ( ph -> Y e. B )
lubpr.l
|- .<_ = ( le ` K )
lubpr.c
|- ( ph -> X .<_ Y )
lubpr.s
|- ( ph -> S = { X , Y } )
lubpr.u
|- U = ( lub ` K )
Assertion lubpr
|- ( ph -> ( U ` S ) = Y )

Proof

Step Hyp Ref Expression
1 lubpr.k
 |-  ( ph -> K e. Poset )
2 lubpr.b
 |-  B = ( Base ` K )
3 lubpr.x
 |-  ( ph -> X e. B )
4 lubpr.y
 |-  ( ph -> Y e. B )
5 lubpr.l
 |-  .<_ = ( le ` K )
6 lubpr.c
 |-  ( ph -> X .<_ Y )
7 lubpr.s
 |-  ( ph -> S = { X , Y } )
8 lubpr.u
 |-  U = ( lub ` K )
9 1 2 3 4 5 6 7 8 lubprlem
 |-  ( ph -> ( S e. dom U /\ ( U ` S ) = Y ) )
10 9 simprd
 |-  ( ph -> ( U ` S ) = Y )