Theorem clatglb

Description: Properties of greatest lower bound of a complete lattice. (Contributed by NM, 5-Dec-2011)

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

Proof

Step	Hyp	Ref	Expression
1		clatglb.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		clatglb.l	⊢ ≤ = ( le ‘ 𝐾 )
3		clatglb.g	⊢ 𝐺 = ( glb ‘ 𝐾 )
4		simpl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝐾 ∈ CLat )
5	1 3	clatglbcl2	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → 𝑆 ∈ dom 𝐺 )
6	1 2 3 4 5	glbprop	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 ( 𝐺 ‘ 𝑆 ) ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝐺 ‘ 𝑆 ) ) ) )