isclatd

Description: The predicate "is a complete lattice" (deduction form). (Contributed by Zhi Wang, 29-Sep-2024)

	Ref	Expression
Hypotheses	isclatd.b	$⊢ φ \to B = {Base}_{K}$
	isclatd.u	$⊢ φ \to U = lub (K)$
	isclatd.g	$⊢ φ \to G = glb (K)$
	isclatd.k	$⊢ φ \to K \in Poset$
	isclatd.1	$⊢ (φ \land s \subseteq B) \to s \in dom U$
	isclatd.2	$⊢ (φ \land s \subseteq B) \to s \in dom G$
Assertion	isclatd	$⊢ φ \to K \in CLat$

Proof

Step	Hyp	Ref	Expression
1		isclatd.b	$⊢ φ \to B = {Base}_{K}$
2		isclatd.u	$⊢ φ \to U = lub (K)$
3		isclatd.g	$⊢ φ \to G = glb (K)$
4		isclatd.k	$⊢ φ \to K \in Poset$
5		isclatd.1	$⊢ (φ \land s \subseteq B) \to s \in dom U$
6		isclatd.2	$⊢ (φ \land s \subseteq B) \to s \in dom G$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8		eqid	$⊢ \leq_{K} = \leq_{K}$
9		eqid	$⊢ lub (K) = lub (K)$
10		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))$
11	7 8 9 10 4	lubdm	$⊢ φ \to dom lub (K) = \{t \in 𝒫 {Base}_{K} \| \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))\}$
12		ssrab2	$⊢ \{t \in 𝒫 {Base}_{K} \| \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))\} \subseteq 𝒫 {Base}_{K}$
13	11 12	eqsstrdi	$⊢ φ \to dom lub (K) \subseteq 𝒫 {Base}_{K}$
14		elpwi	$⊢ s \in 𝒫 B \to s \subseteq B$
15	14 5	sylan2	$⊢ (φ \land s \in 𝒫 B) \to s \in dom U$
16	15	ralrimiva	$⊢ φ \to \forall s \in 𝒫 B s \in dom U$
17		dfss3	$⊢ 𝒫 B \subseteq dom U \leftrightarrow \forall s \in 𝒫 B s \in dom U$
18	16 17	sylibr	$⊢ φ \to 𝒫 B \subseteq dom U$
19	1	pweqd	$⊢ φ \to 𝒫 B = 𝒫 {Base}_{K}$
20	2	dmeqd	$⊢ φ \to dom U = dom lub (K)$
21	18 19 20	3sstr3d	$⊢ φ \to 𝒫 {Base}_{K} \subseteq dom lub (K)$
22	13 21	eqssd	$⊢ φ \to dom lub (K) = 𝒫 {Base}_{K}$
23		eqid	$⊢ glb (K) = glb (K)$
24		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))$
25	7 8 23 24 4	glbdm	$⊢ φ \to dom glb (K) = \{t \in 𝒫 {Base}_{K} \| \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))\}$
26		ssrab2	$⊢ \{t \in 𝒫 {Base}_{K} \| \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))\} \subseteq 𝒫 {Base}_{K}$
27	25 26	eqsstrdi	$⊢ φ \to dom glb (K) \subseteq 𝒫 {Base}_{K}$
28	14 6	sylan2	$⊢ (φ \land s \in 𝒫 B) \to s \in dom G$
29	28	ralrimiva	$⊢ φ \to \forall s \in 𝒫 B s \in dom G$
30		dfss3	$⊢ 𝒫 B \subseteq dom G \leftrightarrow \forall s \in 𝒫 B s \in dom G$
31	29 30	sylibr	$⊢ φ \to 𝒫 B \subseteq dom G$
32	3	dmeqd	$⊢ φ \to dom G = dom glb (K)$
33	31 19 32	3sstr3d	$⊢ φ \to 𝒫 {Base}_{K} \subseteq dom glb (K)$
34	27 33	eqssd	$⊢ φ \to dom glb (K) = 𝒫 {Base}_{K}$
35	7 9 23	isclat	$⊢ K \in CLat \leftrightarrow (K \in Poset \land (dom lub (K) = 𝒫 {Base}_{K} \land dom glb (K) = 𝒫 {Base}_{K}))$
36	35	biimpri	$⊢ (K \in Poset \land (dom lub (K) = 𝒫 {Base}_{K} \land dom glb (K) = 𝒫 {Base}_{K})) \to K \in CLat$
37	4 22 34 36	syl12anc	$⊢ φ \to K \in CLat$

Metamath Proof Explorer

Theorem isclatd

Proof