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	⊢ ( 𝜑 → ( 𝑈 ‘ { 𝑦 ∈ 𝐵 ∣ 𝑦 ≤ 𝑋 } ) = 𝑋 )