Theorem clatglble

Description: The greatest lower bound is the least element. (Contributed by NM, 5-Dec-2011)

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

Proof

Step	Hyp	Ref	Expression
1		clatglb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		clatglb.l	⊢ ≤ = ( le ‘ 𝐾 )
3		clatglb.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		simp1	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → 𝐾 ∈ CLat )
5	1 3	clatglbcl2	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ dom 𝐺 )
6	5	3adant3	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → 𝑆 ∈ dom 𝐺 )
7		simp3	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → 𝑋 ∈ 𝑆 )
8	1 2 3 4 6 7	glble	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑆 ) ≤ 𝑋 )