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

Metamath Proof Explorer

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 )