Theorem clatglbss

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

	Ref	Expression
Hypotheses	clatglb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	clatglb.l	⊢ ≤ = ( le ‘ 𝐾 )
	clatglb.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
Assertion	clatglbss	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ( 𝐺 ‘ 𝑇 ) ≤ ( 𝐺 ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		clatglb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		clatglb.l	⊢ ≤ = ( le ‘ 𝐾 )
3		clatglb.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		simpl1	⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐾 ∈ CLat )
5		simpl2	⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑇 ⊆ 𝐵 )
6		simp3	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → 𝑆 ⊆ 𝑇 )
7	6	sselda	⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑇 )
8	1 2 3	clatglble	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑦 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑇 ) ≤ 𝑦 )
9	4 5 7 8	syl3anc	⊢ ( ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑇 ) ≤ 𝑦 )
10	9	ralrimiva	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ∀ 𝑦 ∈ 𝑆 ( 𝐺 ‘ 𝑇 ) ≤ 𝑦 )
11		simp1	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → 𝐾 ∈ CLat )
12	1 3	clatglbcl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ) → ( 𝐺 ‘ 𝑇 ) ∈ 𝐵 )
13	12	3adant3	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ( 𝐺 ‘ 𝑇 ) ∈ 𝐵 )
14		sstr	⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ 𝐵 ) → 𝑆 ⊆ 𝐵 )
15	14	ancoms	⊢ ( ( 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → 𝑆 ⊆ 𝐵 )
16	15	3adant1	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → 𝑆 ⊆ 𝐵 )
17	1 2 3	clatleglb	⊢ ( ( 𝐾 ∈ CLat ∧ ( 𝐺 ‘ 𝑇 ) ∈ 𝐵 ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝐺 ‘ 𝑇 ) ≤ ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝐺 ‘ 𝑇 ) ≤ 𝑦 ) )
18	11 13 16 17	syl3anc	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ( ( 𝐺 ‘ 𝑇 ) ≤ ( 𝐺 ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝐺 ‘ 𝑇 ) ≤ 𝑦 ) )
19	10 18	mpbird	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑇 ⊆ 𝐵 ∧ 𝑆 ⊆ 𝑇 ) → ( 𝐺 ‘ 𝑇 ) ≤ ( 𝐺 ‘ 𝑆 ) )