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

Metamath Proof Explorer

Theorem lubid

Description: The LUB of elements less than or equal to a fixed value equals that value. (Contributed by NM, 19-Oct-2011) (Revised by NM, 7-Sep-2018)

Ref Expression
Hypotheses lubid.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lubid.l ⊢ ≤ = ( le ‘ 𝐾 )
lubid.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
lubid.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
lubid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion lubid ( 𝜑 → ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 lubid.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lubid.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lubid.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 lubid.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
5 lubid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 biid ⊢ ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ↔ ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) )
7 ssrab2 ⊢ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐵
8 7 a1i ⊢ ( 𝜑 → { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ⊆ 𝐵 )
9 1 2 3 6 4 8 lubval ⊢ ( 𝜑 → ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ) = ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ) )
10 1 2 3 4 5 lublecllem ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ↔ 𝑥 = 𝑋 ) )
11 5 10 riota5 ⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑥 ∧ ∀ 𝑤 ∈ 𝐵 ( ∀ 𝑧 ∈ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } 𝑧 ≤ 𝑤 → 𝑥 ≤ 𝑤 ) ) ) = 𝑋 )
12 9 11 eqtrd ⊢ ( 𝜑 → ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 )