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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ∈ 𝐵 )