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