Metamath Proof Explorer


Theorem lubss

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

Ref Expression
Hypotheses lublem.b B=BaseK
lublem.l ˙=K
lublem.u U=lubK
Assertion lubss KCLatTBSTUS˙UT

Proof

Step Hyp Ref Expression
1 lublem.b B=BaseK
2 lublem.l ˙=K
3 lublem.u U=lubK
4 simp1 KCLatTBSTKCLat
5 sstr2 STTBSB
6 5 impcom TBSTSB
7 6 3adant1 KCLatTBSTSB
8 1 3 clatlubcl KCLatTBUTB
9 8 3adant3 KCLatTBSTUTB
10 4 7 9 3jca KCLatTBSTKCLatSBUTB
11 simpl1 KCLatTBSTySKCLat
12 simpl2 KCLatTBSTySTB
13 ssel2 STySyT
14 13 3ad2antl3 KCLatTBSTySyT
15 1 2 3 lubub KCLatTByTy˙UT
16 11 12 14 15 syl3anc KCLatTBSTySy˙UT
17 16 ralrimiva KCLatTBSTySy˙UT
18 1 2 3 lubl KCLatSBUTBySy˙UTUS˙UT
19 10 17 18 sylc KCLatTBSTUS˙UT