Metamath Proof Explorer

Theorem clatglbss

Description: Subset law for greatest lower bound. (Contributed by Mario Carneiro, 16-Apr-2014)

Ref Expression
Hypotheses clatglb.b ⊢ B = Base K
clatglb.l ⊢ ≤ ˙ = ≤ K
clatglb.g ⊢ G = glb ⁡ K
Assertion clatglbss ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → G ⁡ T ≤ ˙ G ⁡ S

Proof

Step Hyp Ref Expression
1 clatglb.b ⊢ B = Base K
2 clatglb.l ⊢ ≤ ˙ = ≤ K
3 clatglb.g ⊢ G = glb ⁡ K
4 simpl1 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T ∧ y ∈ S → K ∈ CLat
5 simpl2 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T ∧ y ∈ S → T ⊆ B
6 simp3 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → S ⊆ T
7 6 sselda ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T ∧ y ∈ S → y ∈ T
8 1 2 3 clatglble ⊢ K ∈ CLat ∧ T ⊆ B ∧ y ∈ T → G ⁡ T ≤ ˙ y
9 4 5 7 8 syl3anc ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T ∧ y ∈ S → G ⁡ T ≤ ˙ y
10 9 ralrimiva ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → ∀ y ∈ S G ⁡ T ≤ ˙ y
11 simp1 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → K ∈ CLat
12 1 3 clatglbcl ⊢ K ∈ CLat ∧ T ⊆ B → G ⁡ T ∈ B
13 12 3adant3 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → G ⁡ T ∈ B
14 sstr ⊢ S ⊆ T ∧ T ⊆ B → S ⊆ B
15 14 ancoms ⊢ T ⊆ B ∧ S ⊆ T → S ⊆ B
16 15 3adant1 ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → S ⊆ B
17 1 2 3 clatleglb ⊢ K ∈ CLat ∧ G ⁡ T ∈ B ∧ S ⊆ B → G ⁡ T ≤ ˙ G ⁡ S ↔ ∀ y ∈ S G ⁡ T ≤ ˙ y
18 11 13 16 17 syl3anc ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → G ⁡ T ≤ ˙ G ⁡ S ↔ ∀ y ∈ S G ⁡ T ≤ ˙ y
19 10 18 mpbird ⊢ K ∈ CLat ∧ T ⊆ B ∧ S ⊆ T → G ⁡ T ≤ ˙ G ⁡ S