This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑋 → ( 𝑈 ‘ 𝑆 ) ≤ 𝑋 ) )