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

Metamath Proof Explorer

Theorem lubid

Description: The LUB of elements less than or equal to a fixed value equals that value. (Contributed by NM, 19-Oct-2011) (Revised by NM, 7-Sep-2018)

Ref Expression
Hypotheses lubid.b 
|- B = ( Base ` K )
lubid.l 
|- .<_ = ( le ` K )
lubid.u 
|- U = ( lub ` K )
lubid.k 
|- ( ph -> K e. Poset )
lubid.x 
|- ( ph -> X e. B )
Assertion lubid 
|- ( ph -> ( U ` { y e. B | y .<_ X } ) = X )

Proof

Step Hyp Ref Expression
1 lubid.b 
 |-  B = ( Base ` K )
2 lubid.l 
 |-  .<_ = ( le ` K )
3 lubid.u 
 |-  U = ( lub ` K )
4 lubid.k 
 |-  ( ph -> K e. Poset )
5 lubid.x 
 |-  ( ph -> X e. B )
6 biid 
 |-  ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) )
7 ssrab2 
 |-  { y e. B | y .<_ X } C_ B
8 7 a1i 
 |-  ( ph -> { y e. B | y .<_ X } C_ B )
9 1 2 3 6 4 8 lubval 
 |-  ( ph -> ( U ` { y e. B | y .<_ X } ) = ( iota_ x e. B ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) ) )
10 1 2 3 4 5 lublecllem 
 |-  ( ( ph /\ x e. B ) -> ( ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) <-> x = X ) )
11 5 10 riota5 
 |-  ( ph -> ( iota_ x e. B ( A. z e. { y e. B | y .<_ X } z .<_ x /\ A. w e. B ( A. z e. { y e. B | y .<_ X } z .<_ w -> x .<_ w ) ) ) = X )
12 9 11 eqtrd 
 |-  ( ph -> ( U ` { y e. B | y .<_ X } ) = X )