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	$⊢ \underset{˙}{\leq} = \leq_{K}$
	poslubdg.b	$⊢ φ \to B = {Base}_{K}$
	poslubdg.u	$⊢ φ \to U = lub (K)$
	poslubdg.k	$⊢ φ \to K \in Poset$
	poslubdg.s	$⊢ φ \to S \subseteq B$
	poslubdg.t	$⊢ φ \to T \in B$
	poslubdg.ub	$⊢ (φ \land x \in S) \to x \underset{˙}{\leq} T$
	poslubdg.le	$⊢ (φ \land y \in B \land \forall x \in S x \underset{˙}{\leq} y) \to T \underset{˙}{\leq} y$
Assertion	poslubdg	$⊢ φ \to U (S) = T$

Step	Hyp	Ref	Expression
1		poslubdg.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		poslubdg.b	$⊢ φ \to B = {Base}_{K}$
3		poslubdg.u	$⊢ φ \to U = lub (K)$
4		poslubdg.k	$⊢ φ \to K \in Poset$
5		poslubdg.s	$⊢ φ \to S \subseteq B$
6		poslubdg.t	$⊢ φ \to T \in B$
7		poslubdg.ub	$⊢ (φ \land x \in S) \to x \underset{˙}{\leq} T$
8		poslubdg.le	$⊢ (φ \land y \in B \land \forall x \in S x \underset{˙}{\leq} y) \to T \underset{˙}{\leq} y$
9	3	fveq1d	$⊢ φ \to U (S) = lub (K) (S)$
10		eqid	$⊢ {Base}_{K} = {Base}_{K}$
11		eqid	$⊢ lub (K) = lub (K)$
12	5 2	sseqtrd	$⊢ φ \to S \subseteq {Base}_{K}$
13	6 2	eleqtrd	$⊢ φ \to T \in {Base}_{K}$
14	2	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in {Base}_{K})$
15	14	biimpar	$⊢ (φ \land y \in {Base}_{K}) \to y \in B$
16	15	3adant3	$⊢ (φ \land y \in {Base}_{K} \land \forall x \in S x \underset{˙}{\leq} y) \to y \in B$
17	16 8	syld3an2	$⊢ (φ \land y \in {Base}_{K} \land \forall x \in S x \underset{˙}{\leq} y) \to T \underset{˙}{\leq} y$
18	1 10 11 4 12 13 7 17	poslubd	$⊢ φ \to lub (K) (S) = T$
19	9 18	eqtrd	$⊢ φ \to U (S) = T$

Metamath Proof Explorer