Theorem lubl

Description: The LUB of a complete lattice subset is the least bound. (Contributed by NM, 19-Oct-2011)

	Ref	Expression
Hypotheses	lublem.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lublem.l	⊢ ≤ = ( le ‘ 𝐾 )
	lublem.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
Assertion	lubl	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		lublem.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lublem.l	⊢ ≤ = ( le ‘ 𝐾 )
3		lublem.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
4	1 2 3	lublem	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ ( 𝑈 ‘ 𝑆 ) ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) ) )
5	4	simprd	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ) → ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) )
6		breq2	⊢ ( 𝑧 = 𝑋 → ( 𝑦 ≤ 𝑧 ↔ 𝑦 ≤ 𝑋 ) )
7	6	ralbidv	⊢ ( 𝑧 = 𝑋 → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 ) )
8		breq2	⊢ ( 𝑧 = 𝑋 → ( ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ↔ ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 ) )
9	7 8	imbi12d	⊢ ( 𝑧 = 𝑋 → ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 ) ) )
10	9	rspccva	⊢ ( ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑧 ) ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 ) )
11	5 10	stoic3	⊢ ( ( 𝐾 ∈ CLat ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 ) )