Theorem lubcl

Description: The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	lubcl.b	|- B = ( Base ` K )
	lubcl.u	|- U = ( lub ` K )
	lubcl.k	|- ( ph -> K e. V )
	lubcl.s	|- ( ph -> S e. dom U )
Assertion	lubcl	|- ( ph -> ( U ` S ) e. B )

Proof

Step	Hyp	Ref	Expression
1		lubcl.b	|- B = ( Base ` K )
2		lubcl.u	|- U = ( lub ` K )
3		lubcl.k	|- ( ph -> K e. V )
4		lubcl.s	|- ( ph -> S e. dom U )
5		eqid	|- ( le ` K ) = ( le ` K )
6		biid	|- ( ( A. y e. S y ( le ` K ) x /\ A. z e. B ( A. y e. S y ( le ` K ) z -> x ( le ` K ) z ) ) <-> ( A. y e. S y ( le ` K ) x /\ A. z e. B ( A. y e. S y ( le ` K ) z -> x ( le ` K ) z ) ) )
7	1 5 2 3 4	lubelss	|- ( ph -> S C_ B )
8	1 5 2 6 3 7	lubval	|- ( ph -> ( U ` S ) = ( iota_ x e. B ( A. y e. S y ( le ` K ) x /\ A. z e. B ( A. y e. S y ( le ` K ) z -> x ( le ` K ) z ) ) ) )
9	1 5 2 6 3 4	lubeu	|- ( ph -> E! x e. B ( A. y e. S y ( le ` K ) x /\ A. z e. B ( A. y e. S y ( le ` K ) z -> x ( le ` K ) z ) ) )
10		riotacl	|- ( E! x e. B ( A. y e. S y ( le ` K ) x /\ A. z e. B ( A. y e. S y ( le ` K ) z -> x ( le ` K ) z ) ) -> ( iota_ x e. B ( A. y e. S y ( le ` K ) x /\ A. z e. B ( A. y e. S y ( le ` K ) z -> x ( le ` K ) z ) ) ) e. B )
11	9 10	syl	|- ( ph -> ( iota_ x e. B ( A. y e. S y ( le ` K ) x /\ A. z e. B ( A. y e. S y ( le ` K ) z -> x ( le ` K ) z ) ) ) e. B )
12	8 11	eqeltrd	|- ( ph -> ( U ` S ) e. B )