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

Metamath Proof Explorer

Theorem poslubdg

Description: Properties which determine the least upper bound in a poset. (Contributed by Stefan O'Rear, 31-Jan-2015)

Ref Expression
Hypotheses poslubdg.l ⊢ ≤ = ( le ‘ 𝐾 )
poslubdg.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
poslubdg.u ⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐾 ) )
poslubdg.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
poslubdg.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
poslubdg.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
poslubdg.ub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ≤ 𝑇 )
poslubdg.le ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 ) → 𝑇 ≤ 𝑦 )
Assertion poslubdg ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = 𝑇 )

Proof

Step Hyp Ref Expression
1 poslubdg.l ⊢ ≤ = ( le ‘ 𝐾 )
2 poslubdg.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
3 poslubdg.u ⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐾 ) )
4 poslubdg.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
5 poslubdg.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
6 poslubdg.t ⊢ ( 𝜑 → 𝑇 ∈ 𝐵 )
7 poslubdg.ub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ≤ 𝑇 )
8 poslubdg.le ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 ) → 𝑇 ≤ 𝑦 )
9 3 fveq1d ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) )
10 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
11 eqid ⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
12 5 2 sseqtrd ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐾 ) )
13 6 2 eleqtrd ⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
14 2 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ( Base ‘ 𝐾 ) ) )
15 14 biimpar ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ) → 𝑦 ∈ 𝐵 )
16 15 3adant3 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 ) → 𝑦 ∈ 𝐵 )
17 16 8 syld3an2 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ 𝑆 𝑥 ≤ 𝑦 ) → 𝑇 ≤ 𝑦 )
18 1 10 11 4 12 13 7 17 poslubd ⊢ ( 𝜑 → ( ( lub ‘ 𝐾 ) ‘ 𝑆 ) = 𝑇 )
19 9 18 eqtrd ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = 𝑇 )