Theorem glble

Description: The greatest lower bound is the least element. (Contributed by NM, 22-Oct-2011) (Revised by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	glbprop.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	glbprop.l	⊢ ≤ = ( le ‘ 𝐾 )
	glbprop.u	⊢ 𝑈 = ( glb ‘ 𝐾 )
	glbprop.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	glbprop.s	⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
	glble.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
Assertion	glble	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		glbprop.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		glbprop.l	⊢ ≤ = ( le ‘ 𝐾 )
3		glbprop.u	⊢ 𝑈 = ( glb ‘ 𝐾 )
4		glbprop.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
5		glbprop.s	⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
6		glble.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
7		breq2	⊢ ( 𝑦 = 𝑋 → ( ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ↔ ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 ) )
8	1 2 3 4 5	glbprop	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑆 ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑧 ≤ 𝑦 → 𝑧 ≤ ( 𝑈 ‘ 𝑆 ) ) ) )
9	8	simpld	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 ( 𝑈 ‘ 𝑆 ) ≤ 𝑦 )
10	7 9 6	rspcdva	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 )