glbsscl

Description: If a subset of S contains the GLB of S , then the two sets have the same GLB. (Contributed by Zhi Wang, 26-Sep-2024)

	Ref	Expression
Hypotheses	lubsscl.k	$⊢ φ \to K \in Poset$
	lubsscl.t	$⊢ φ \to T \subseteq S$
	glbsscl.g	$⊢ G = glb (K)$
	glbsscl.s	$⊢ φ \to S \in dom G$
	glbsscl.x	$⊢ φ \to G (S) \in T$
Assertion	glbsscl	$⊢ φ \to (T \in dom G \land G (T) = G (S))$

Proof

Step	Hyp	Ref	Expression
1		lubsscl.k	$⊢ φ \to K \in Poset$
2		lubsscl.t	$⊢ φ \to T \subseteq S$
3		glbsscl.g	$⊢ G = glb (K)$
4		glbsscl.s	$⊢ φ \to S \in dom G$
5		glbsscl.x	$⊢ φ \to G (S) \in T$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8	6 7 3 1 4	glbelss	$⊢ φ \to S \subseteq {Base}_{K}$
9	2 8	sstrd	$⊢ φ \to T \subseteq {Base}_{K}$
10	9 5	sseldd	$⊢ φ \to G (S) \in {Base}_{K}$
11	1	adantr	$⊢ (φ \land y \in T) \to K \in Poset$
12	4	adantr	$⊢ (φ \land y \in T) \to S \in dom G$
13	2	sselda	$⊢ (φ \land y \in T) \to y \in S$
14	6 7 3 11 12 13	glble	$⊢ (φ \land y \in T) \to G (S) \leq_{K} y$
15	14	ralrimiva	$⊢ φ \to \forall y \in T G (S) \leq_{K} y$
16		breq2	$⊢ y = G (S) \to (z \leq_{K} y \leftrightarrow z \leq_{K} G (S))$
17		simp3	$⊢ (φ \land z \in {Base}_{K} \land \forall y \in T z \leq_{K} y) \to \forall y \in T z \leq_{K} y$
18	5	3ad2ant1	$⊢ (φ \land z \in {Base}_{K} \land \forall y \in T z \leq_{K} y) \to G (S) \in T$
19	16 17 18	rspcdva	$⊢ (φ \land z \in {Base}_{K} \land \forall y \in T z \leq_{K} y) \to z \leq_{K} G (S)$
20	19	3expia	$⊢ (φ \land z \in {Base}_{K}) \to (\forall y \in T z \leq_{K} y \to z \leq_{K} G (S))$
21	20	ralrimiva	$⊢ φ \to \forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} G (S))$
22		breq1	$⊢ x = G (S) \to (x \leq_{K} y \leftrightarrow G (S) \leq_{K} y)$
23	22	ralbidv	$⊢ x = G (S) \to (\forall y \in T x \leq_{K} y \leftrightarrow \forall y \in T G (S) \leq_{K} y)$
24		breq2	$⊢ x = G (S) \to (z \leq_{K} x \leftrightarrow z \leq_{K} G (S))$
25	24	imbi2d	$⊢ x = G (S) \to ((\forall y \in T z \leq_{K} y \to z \leq_{K} x) \leftrightarrow (\forall y \in T z \leq_{K} y \to z \leq_{K} G (S)))$
26	25	ralbidv	$⊢ x = G (S) \to (\forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} x) \leftrightarrow \forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} G (S)))$
27	23 26	anbi12d	$⊢ x = G (S) \to ((\forall y \in T x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} x)) \leftrightarrow (\forall y \in T G (S) \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} G (S))))$
28	27	rspcev	$⊢ (G (S) \in {Base}_{K} \land (\forall y \in T G (S) \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} G (S)))) \to \exists x \in {Base}_{K} (\forall y \in T x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} x))$
29	10 15 21 28	syl12anc	$⊢ φ \to \exists x \in {Base}_{K} (\forall y \in T x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} x))$
30		biid	$⊢ (\forall y \in T x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} x)) \leftrightarrow (\forall y \in T x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} x))$
31	6 7 3 30 1	glbeldm2	$⊢ φ \to (T \in dom G \leftrightarrow (T \subseteq {Base}_{K} \land \exists x \in {Base}_{K} (\forall y \in T x \leq_{K} y \land \forall z \in {Base}_{K} (\forall y \in T z \leq_{K} y \to z \leq_{K} x))))$
32	9 29 31	mpbir2and	$⊢ φ \to T \in dom G$
33		eqidd	$⊢ φ \to {Base}_{K} = {Base}_{K}$
34	3	a1i	$⊢ φ \to G = glb (K)$
35	7 33 34 1 9 10 14 19	posglbdg	$⊢ φ \to G (T) = G (S)$
36	32 35	jca	$⊢ φ \to (T \in dom G \land G (T) = G (S))$

Metamath Proof Explorer

Theorem glbsscl

Proof