Metamath Proof Explorer


Theorem lubprop

Description: Properties of greatest lower bound of a poset. (Contributed by NM, 22-Oct-2011) (Revised by NM, 7-Sep-2018)

Ref Expression
Hypotheses lubprop.b
|- B = ( Base ` K )
lubprop.l
|- .<_ = ( le ` K )
lubprop.u
|- U = ( lub ` K )
lubprop.k
|- ( ph -> K e. V )
lubprop.s
|- ( ph -> S e. dom U )
Assertion lubprop
|- ( ph -> ( A. y e. S y .<_ ( U ` S ) /\ A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) ) )

Proof

Step Hyp Ref Expression
1 lubprop.b
 |-  B = ( Base ` K )
2 lubprop.l
 |-  .<_ = ( le ` K )
3 lubprop.u
 |-  U = ( lub ` K )
4 lubprop.k
 |-  ( ph -> K e. V )
5 lubprop.s
 |-  ( ph -> S e. dom U )
6 biid
 |-  ( ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) <-> ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
7 1 2 3 4 5 lubelss
 |-  ( ph -> S C_ B )
8 1 2 3 6 4 7 lubval
 |-  ( ph -> ( U ` S ) = ( iota_ x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) )
9 8 eqcomd
 |-  ( ph -> ( iota_ x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) = ( U ` S ) )
10 1 3 4 5 lubcl
 |-  ( ph -> ( U ` S ) e. B )
11 1 2 3 6 4 5 lubeu
 |-  ( ph -> E! x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) )
12 breq2
 |-  ( x = ( U ` S ) -> ( y .<_ x <-> y .<_ ( U ` S ) ) )
13 12 ralbidv
 |-  ( x = ( U ` S ) -> ( A. y e. S y .<_ x <-> A. y e. S y .<_ ( U ` S ) ) )
14 breq1
 |-  ( x = ( U ` S ) -> ( x .<_ z <-> ( U ` S ) .<_ z ) )
15 14 imbi2d
 |-  ( x = ( U ` S ) -> ( ( A. y e. S y .<_ z -> x .<_ z ) <-> ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) ) )
16 15 ralbidv
 |-  ( x = ( U ` S ) -> ( A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) <-> A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) ) )
17 13 16 anbi12d
 |-  ( x = ( U ` S ) -> ( ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) <-> ( A. y e. S y .<_ ( U ` S ) /\ A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) ) ) )
18 17 riota2
 |-  ( ( ( U ` S ) e. B /\ E! x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) -> ( ( A. y e. S y .<_ ( U ` S ) /\ A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) ) <-> ( iota_ x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) = ( U ` S ) ) )
19 10 11 18 syl2anc
 |-  ( ph -> ( ( A. y e. S y .<_ ( U ` S ) /\ A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) ) <-> ( iota_ x e. B ( A. y e. S y .<_ x /\ A. z e. B ( A. y e. S y .<_ z -> x .<_ z ) ) ) = ( U ` S ) ) )
20 9 19 mpbird
 |-  ( ph -> ( A. y e. S y .<_ ( U ` S ) /\ A. z e. B ( A. y e. S y .<_ z -> ( U ` S ) .<_ z ) ) )