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 ) ) ) )