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