posglbmo

Description: Greatest lower bounds in a poset are unique if they exist. (Contributed by NM, 20-Sep-2018)

	Ref	Expression
Hypotheses	poslubmo.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	poslubmo.b	$⊢ B = {Base}_{K}$
Assertion	posglbmo	$⊢ (K \in Poset \land S \subseteq B) \to \exists^{*} x \in B (\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x))$

Proof

Step	Hyp	Ref	Expression
1		poslubmo.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		poslubmo.b	$⊢ B = {Base}_{K}$
3		simprrl	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to \forall y \in S w \underset{˙}{\leq} y$
4		breq1	$⊢ z = w \to (z \underset{˙}{\leq} y \leftrightarrow w \underset{˙}{\leq} y)$
5	4	ralbidv	$⊢ z = w \to (\forall y \in S z \underset{˙}{\leq} y \leftrightarrow \forall y \in S w \underset{˙}{\leq} y)$
6		breq1	$⊢ z = w \to (z \underset{˙}{\leq} x \leftrightarrow w \underset{˙}{\leq} x)$
7	5 6	imbi12d	$⊢ z = w \to ((\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x) \leftrightarrow (\forall y \in S w \underset{˙}{\leq} y \to w \underset{˙}{\leq} x))$
8		simprlr	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)$
9		simplrr	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to w \in B$
10	7 8 9	rspcdva	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to (\forall y \in S w \underset{˙}{\leq} y \to w \underset{˙}{\leq} x)$
11	3 10	mpd	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to w \underset{˙}{\leq} x$
12		simprll	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to \forall y \in S x \underset{˙}{\leq} y$
13		breq1	$⊢ z = x \to (z \underset{˙}{\leq} y \leftrightarrow x \underset{˙}{\leq} y)$
14	13	ralbidv	$⊢ z = x \to (\forall y \in S z \underset{˙}{\leq} y \leftrightarrow \forall y \in S x \underset{˙}{\leq} y)$
15		breq1	$⊢ z = x \to (z \underset{˙}{\leq} w \leftrightarrow x \underset{˙}{\leq} w)$
16	14 15	imbi12d	$⊢ z = x \to ((\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w) \leftrightarrow (\forall y \in S x \underset{˙}{\leq} y \to x \underset{˙}{\leq} w))$
17		simprrr	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)$
18		simplrl	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to x \in B$
19	16 17 18	rspcdva	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to (\forall y \in S x \underset{˙}{\leq} y \to x \underset{˙}{\leq} w)$
20	12 19	mpd	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to x \underset{˙}{\leq} w$
21		ancom	$⊢ (w \underset{˙}{\leq} x \land x \underset{˙}{\leq} w) \leftrightarrow (x \underset{˙}{\leq} w \land w \underset{˙}{\leq} x)$
22	2 1	posasymb	$⊢ (K \in Poset \land x \in B \land w \in B) \to ((x \underset{˙}{\leq} w \land w \underset{˙}{\leq} x) \leftrightarrow x = w)$
23	21 22	syl5bb	$⊢ (K \in Poset \land x \in B \land w \in B) \to ((w \underset{˙}{\leq} x \land x \underset{˙}{\leq} w) \leftrightarrow x = w)$
24	23	3expb	$⊢ (K \in Poset \land (x \in B \land w \in B)) \to ((w \underset{˙}{\leq} x \land x \underset{˙}{\leq} w) \leftrightarrow x = w)$
25	24	ad4ant13	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to ((w \underset{˙}{\leq} x \land x \underset{˙}{\leq} w) \leftrightarrow x = w)$
26	11 20 25	mpbi2and	$⊢ (((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \land ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))) \to x = w$
27	26	ex	$⊢ ((K \in Poset \land S \subseteq B) \land (x \in B \land w \in B)) \to (((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w))) \to x = w)$
28	27	ralrimivva	$⊢ (K \in Poset \land S \subseteq B) \to \forall x \in B \forall w \in B (((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w))) \to x = w)$
29		breq1	$⊢ x = w \to (x \underset{˙}{\leq} y \leftrightarrow w \underset{˙}{\leq} y)$
30	29	ralbidv	$⊢ x = w \to (\forall y \in S x \underset{˙}{\leq} y \leftrightarrow \forall y \in S w \underset{˙}{\leq} y)$
31		breq2	$⊢ x = w \to (z \underset{˙}{\leq} x \leftrightarrow z \underset{˙}{\leq} w)$
32	31	imbi2d	$⊢ x = w \to ((\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x) \leftrightarrow (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w))$
33	32	ralbidv	$⊢ x = w \to (\forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x) \leftrightarrow \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w))$
34	30 33	anbi12d	$⊢ x = w \to ((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \leftrightarrow (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w)))$
35	34	rmo4	$⊢ \exists^{*} x \in B (\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \leftrightarrow \forall x \in B \forall w \in B (((\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x)) \land (\forall y \in S w \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} w))) \to x = w)$
36	28 35	sylibr	$⊢ (K \in Poset \land S \subseteq B) \to \exists^{*} x \in B (\forall y \in S x \underset{˙}{\leq} y \land \forall z \in B (\forall y \in S z \underset{˙}{\leq} y \to z \underset{˙}{\leq} x))$

Metamath Proof Explorer

Theorem posglbmo

Proof