Theorem poslubdg

Description: Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Hypotheses	poslubdg.l	|- .<_ = ( le ` K )
	poslubdg.b	|- ( ph -> B = ( Base ` K ) )
	poslubdg.u	|- ( ph -> U = ( lub ` K ) )
	poslubdg.k	|- ( ph -> K e. Poset )
	poslubdg.s	|- ( ph -> S C_ B )
	poslubdg.t	|- ( ph -> T e. B )
	poslubdg.ub	|- ( ( ph /\ x e. S ) -> x .<_ T )
	poslubdg.le	|- ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y )
Assertion	poslubdg	|- ( ph -> ( U ` S ) = T )

Proof

Step	Hyp	Ref	Expression
1		poslubdg.l	|- .<_ = ( le ` K )
2		poslubdg.b	|- ( ph -> B = ( Base ` K ) )
3		poslubdg.u	|- ( ph -> U = ( lub ` K ) )
4		poslubdg.k	|- ( ph -> K e. Poset )
5		poslubdg.s	|- ( ph -> S C_ B )
6		poslubdg.t	|- ( ph -> T e. B )
7		poslubdg.ub	|- ( ( ph /\ x e. S ) -> x .<_ T )
8		poslubdg.le	|- ( ( ph /\ y e. B /\ A. x e. S x .<_ y ) -> T .<_ y )
9	3	fveq1d	|- ( ph -> ( U ` S ) = ( ( lub ` K ) ` S ) )
10		eqid	|- ( Base ` K ) = ( Base ` K )
11		eqid	|- ( lub ` K ) = ( lub ` K )
12	5 2	sseqtrd	|- ( ph -> S C_ ( Base ` K ) )
13	6 2	eleqtrd	|- ( ph -> T e. ( Base ` K ) )
14	2	eleq2d	|- ( ph -> ( y e. B <-> y e. ( Base ` K ) ) )
15	14	biimpar	|- ( ( ph /\ y e. ( Base ` K ) ) -> y e. B )
16	15	3adant3	|- ( ( ph /\ y e. ( Base ` K ) /\ A. x e. S x .<_ y ) -> y e. B )
17	16 8	syld3an2	|- ( ( ph /\ y e. ( Base ` K ) /\ A. x e. S x .<_ y ) -> T .<_ y )
18	1 10 11 4 12 13 7 17	poslubd	|- ( ph -> ( ( lub ` K ) ` S ) = T )
19	9 18	eqtrd	|- ( ph -> ( U ` S ) = T )