Theorem lubcl

Description: The least upper bound function value belongs to the base set. (Contributed by NM, 7-Sep-2018)

	Ref	Expression
Hypotheses	lubcl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	lubcl.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
	lubcl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
	lubcl.s	⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
Assertion	lubcl	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		lubcl.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		lubcl.u	⊢ 𝑈 = ( lub ‘ 𝐾 )
3		lubcl.k	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
4		lubcl.s	⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
5		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
6		biid	⊢ ( ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
7	1 5 2 3 4	lubelss	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
8	1 5 2 6 3 7	lubval	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) )
9	1 5 2 6 3 4	lubeu	⊢ ( 𝜑 → ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
10		riotacl	⊢ ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) → ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ∈ 𝐵 )
11	9 10	syl	⊢ ( 𝜑 → ( ℩ 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ∈ 𝐵 )
12	8 11	eqeltrd	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )