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 = Base K
lublem.l ⊢ ≤ ˙ = ≤ K
lublem.u ⊢ U = lub ⁡ K
Assertion lubss ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → U ⁡ S ≤ ˙ U ⁡ T

Proof

Step Hyp Ref Expression
1 lublem.b ⊢ B = Base K
2 lublem.l ⊢ ≤ ˙ = ≤ K
3 lublem.u ⊢ U = lub ⁡ K
4 simp1 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → K ∈ CLat
5 sstr2 ⊢ S ⊆ T → T ⊆ B → S ⊆ B
6 5 impcom ⊢ T ⊆ B ∧ S ⊆ T → S ⊆ B
7 6 3adant1 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → S ⊆ B
8 1 3 clatlubcl ⊢ K ∈ CLat ∧ T ⊆ B → U ⁡ T ∈ B
9 8 3adant3 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → U ⁡ T ∈ B
10 4 7 9 3jca ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → K ∈ CLat ∧ S ⊆ B ∧ U ⁡ T ∈ B
11 simpl1 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T ∧ y ∈ S → K ∈ CLat
12 simpl2 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T ∧ y ∈ S → T ⊆ B
13 ssel2 ⊢ S ⊆ T ∧ y ∈ S → y ∈ T
14 13 3ad2antl3 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T ∧ y ∈ S → y ∈ T
15 1 2 3 lubub ⊢ K ∈ CLat ∧ T ⊆ B ∧ y ∈ T → y ≤ ˙ U ⁡ T
16 11 12 14 15 syl3anc ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T ∧ y ∈ S → y ≤ ˙ U ⁡ T
17 16 ralrimiva ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → ∀ y ∈ S y ≤ ˙ U ⁡ T
18 1 2 3 lubl ⊢ K ∈ CLat ∧ S ⊆ B ∧ U ⁡ T ∈ B → ∀ y ∈ S y ≤ ˙ U ⁡ T → U ⁡ S ≤ ˙ U ⁡ T
19 10 17 18 sylc ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → U ⁡ S ≤ ˙ U ⁡ T