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

Metamath Proof Explorer

Theorem glbprop

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

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

Proof

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