lubsscl

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

	Ref	Expression
Hypotheses	lubsscl.k	$⊢ φ \to K \in Poset$
	lubsscl.t	$⊢ φ \to T \subseteq S$
	lubsscl.u	$⊢ U = lub (K)$
	lubsscl.s	$⊢ φ \to S \in dom U$
	lubsscl.x	$⊢ φ \to U (S) \in T$
Assertion	lubsscl	$⊢ φ \to (T \in dom U \land U (T) = U (S))$

Proof

Step	Hyp	Ref	Expression
1		lubsscl.k	$⊢ φ \to K \in Poset$
2		lubsscl.t	$⊢ φ \to T \subseteq S$
3		lubsscl.u	$⊢ U = lub (K)$
4		lubsscl.s	$⊢ φ \to S \in dom U$
5		lubsscl.x	$⊢ φ \to U (S) \in T$
6		eqid	$⊢ {Base}_{K} = {Base}_{K}$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8	6 7 3 1 4	lubelss	$⊢ φ \to S \subseteq {Base}_{K}$
9	2 8	sstrd	$⊢ φ \to T \subseteq {Base}_{K}$
10	9 5	sseldd	$⊢ φ \to U (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 U$
13	2	sselda	$⊢ (φ \land y \in T) \to y \in S$
14	6 7 3 11 12 13	luble	$⊢ (φ \land y \in T) \to y \leq_{K} U (S)$
15	14	ralrimiva	$⊢ φ \to \forall y \in T y \leq_{K} U (S)$
16		breq1	$⊢ y = U (S) \to (y \leq_{K} z \leftrightarrow U (S) \leq_{K} z)$
17		simp3	$⊢ (φ \land z \in {Base}_{K} \land \forall y \in T y \leq_{K} z) \to \forall y \in T y \leq_{K} z$
18	5	3ad2ant1	$⊢ (φ \land z \in {Base}_{K} \land \forall y \in T y \leq_{K} z) \to U (S) \in T$
19	16 17 18	rspcdva	$⊢ (φ \land z \in {Base}_{K} \land \forall y \in T y \leq_{K} z) \to U (S) \leq_{K} z$
20	19	3expia	$⊢ (φ \land z \in {Base}_{K}) \to (\forall y \in T y \leq_{K} z \to U (S) \leq_{K} z)$
21	20	ralrimiva	$⊢ φ \to \forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to U (S) \leq_{K} z)$
22		breq2	$⊢ x = U (S) \to (y \leq_{K} x \leftrightarrow y \leq_{K} U (S))$
23	22	ralbidv	$⊢ x = U (S) \to (\forall y \in T y \leq_{K} x \leftrightarrow \forall y \in T y \leq_{K} U (S))$
24		breq1	$⊢ x = U (S) \to (x \leq_{K} z \leftrightarrow U (S) \leq_{K} z)$
25	24	imbi2d	$⊢ x = U (S) \to ((\forall y \in T y \leq_{K} z \to x \leq_{K} z) \leftrightarrow (\forall y \in T y \leq_{K} z \to U (S) \leq_{K} z))$
26	25	ralbidv	$⊢ x = U (S) \to (\forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to x \leq_{K} z) \leftrightarrow \forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to U (S) \leq_{K} z))$
27	23 26	anbi12d	$⊢ x = U (S) \to ((\forall y \in T y \leq_{K} x \land \forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to x \leq_{K} z)) \leftrightarrow (\forall y \in T y \leq_{K} U (S) \land \forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to U (S) \leq_{K} z)))$
28	27	rspcev	$⊢ (U (S) \in {Base}_{K} \land (\forall y \in T y \leq_{K} U (S) \land \forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to U (S) \leq_{K} z))) \to \exists x \in {Base}_{K} (\forall y \in T y \leq_{K} x \land \forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to x \leq_{K} z))$
29	10 15 21 28	syl12anc	$⊢ φ \to \exists x \in {Base}_{K} (\forall y \in T y \leq_{K} x \land \forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to x \leq_{K} z))$
30		biid	$⊢ (\forall y \in T y \leq_{K} x \land \forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to x \leq_{K} z)) \leftrightarrow (\forall y \in T y \leq_{K} x \land \forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to x \leq_{K} z))$
31	6 7 3 30 1	lubeldm2	$⊢ φ \to (T \in dom U \leftrightarrow (T \subseteq {Base}_{K} \land \exists x \in {Base}_{K} (\forall y \in T y \leq_{K} x \land \forall z \in {Base}_{K} (\forall y \in T y \leq_{K} z \to x \leq_{K} z))))$
32	9 29 31	mpbir2and	$⊢ φ \to T \in dom U$
33	7 6 3 1 9 10 14 19	poslubd	$⊢ φ \to U (T) = U (S)$
34	32 33	jca	$⊢ φ \to (T \in dom U \land U (T) = U (S))$

Metamath Proof Explorer

Theorem lubsscl

Proof