Theorem lubss

Description: Subset law for least upper bounds. ( chsupss analog.) (Contributed by NM, 20-Oct-2011)

	Ref	Expression
Hypotheses	lublem.b	|- B = ( Base ` K )
	lublem.l	|- .<_ = ( le ` K )
	lublem.u	|- U = ( lub ` K )
Assertion	lubss	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> ( U ` S ) .<_ ( U ` T ) )

Proof

Step	Hyp	Ref	Expression
1		lublem.b	|- B = ( Base ` K )
2		lublem.l	|- .<_ = ( le ` K )
3		lublem.u	|- U = ( lub ` K )
4		simp1	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> K e. CLat )
5		sstr2	|- ( S C_ T -> ( T C_ B -> S C_ B ) )
6	5	impcom	|- ( ( T C_ B /\ S C_ T ) -> S C_ B )
7	6	3adant1	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> S C_ B )
8	1 3	clatlubcl	|- ( ( K e. CLat /\ T C_ B ) -> ( U ` T ) e. B )
9	8	3adant3	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> ( U ` T ) e. B )
10	4 7 9	3jca	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> ( K e. CLat /\ S C_ B /\ ( U ` T ) e. B ) )
11		simpl1	|- ( ( ( K e. CLat /\ T C_ B /\ S C_ T ) /\ y e. S ) -> K e. CLat )
12		simpl2	|- ( ( ( K e. CLat /\ T C_ B /\ S C_ T ) /\ y e. S ) -> T C_ B )
13		ssel2	|- ( ( S C_ T /\ y e. S ) -> y e. T )
14	13	3ad2antl3	|- ( ( ( K e. CLat /\ T C_ B /\ S C_ T ) /\ y e. S ) -> y e. T )
15	1 2 3	lubub	|- ( ( K e. CLat /\ T C_ B /\ y e. T ) -> y .<_ ( U ` T ) )
16	11 12 14 15	syl3anc	|- ( ( ( K e. CLat /\ T C_ B /\ S C_ T ) /\ y e. S ) -> y .<_ ( U ` T ) )
17	16	ralrimiva	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> A. y e. S y .<_ ( U ` T ) )
18	1 2 3	lubl	|- ( ( K e. CLat /\ S C_ B /\ ( U ` T ) e. B ) -> ( A. y e. S y .<_ ( U ` T ) -> ( U ` S ) .<_ ( U ` T ) ) )
19	10 17 18	sylc	|- ( ( K e. CLat /\ T C_ B /\ S C_ T ) -> ( U ` S ) .<_ ( U ` T ) )