Theorem isclatd

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

	Ref	Expression
Hypotheses	isclatd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
	isclatd.u	⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐾 ) )
	isclatd.g	⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐾 ) )
	isclatd.k	⊢ ( 𝜑 → 𝐾 ∈ Poset )
	isclatd.1	⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) → 𝑠 ∈ dom 𝑈 )
	isclatd.2	⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) → 𝑠 ∈ dom 𝐺 )
Assertion	isclatd	⊢ ( 𝜑 → 𝐾 ∈ CLat )

Proof

Step	Hyp	Ref	Expression
1		isclatd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐾 ) )
2		isclatd.u	⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐾 ) )
3		isclatd.g	⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐾 ) )
4		isclatd.k	⊢ ( 𝜑 → 𝐾 ∈ Poset )
5		isclatd.1	⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) → 𝑠 ∈ dom 𝑈 )
6		isclatd.2	⊢ ( ( 𝜑 ∧ 𝑠 ⊆ 𝐵 ) → 𝑠 ∈ dom 𝐺 )
7		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
8		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
9		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
10		biid	⊢ ( ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) )
11	7 8 9 10 4	lubdm	⊢ ( 𝜑 → dom ( lub ‘ 𝐾 ) = { 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) } )
12		ssrab2	⊢ { 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) } ⊆ 𝒫 ( Base ‘ 𝐾 )
13	11 12	eqsstrdi	⊢ ( 𝜑 → dom ( lub ‘ 𝐾 ) ⊆ 𝒫 ( Base ‘ 𝐾 ) )
14		elpwi	⊢ ( 𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵 )
15	14 5	sylan2	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ dom 𝑈 )
16	15	ralrimiva	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ dom 𝑈 )
17		dfss3	⊢ ( 𝒫 𝐵 ⊆ dom 𝑈 ↔ ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ dom 𝑈 )
18	16 17	sylibr	⊢ ( 𝜑 → 𝒫 𝐵 ⊆ dom 𝑈 )
19	1	pweqd	⊢ ( 𝜑 → 𝒫 𝐵 = 𝒫 ( Base ‘ 𝐾 ) )
20	2	dmeqd	⊢ ( 𝜑 → dom 𝑈 = dom ( lub ‘ 𝐾 ) )
21	18 19 20	3sstr3d	⊢ ( 𝜑 → 𝒫 ( Base ‘ 𝐾 ) ⊆ dom ( lub ‘ 𝐾 ) )
22	13 21	eqssd	⊢ ( 𝜑 → dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) )
23		eqid	⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
24		biid	⊢ ( ( ∀ 𝑦 ∈ 𝑡 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑡 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
25	7 8 23 24 4	glbdm	⊢ ( 𝜑 → dom ( glb ‘ 𝐾 ) = { 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) } )
26		ssrab2	⊢ { 𝑡 ∈ 𝒫 ( Base ‘ 𝐾 ) ∣ ∃! 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑡 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) } ⊆ 𝒫 ( Base ‘ 𝐾 )
27	25 26	eqsstrdi	⊢ ( 𝜑 → dom ( glb ‘ 𝐾 ) ⊆ 𝒫 ( Base ‘ 𝐾 ) )
28	14 6	sylan2	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ dom 𝐺 )
29	28	ralrimiva	⊢ ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ dom 𝐺 )
30		dfss3	⊢ ( 𝒫 𝐵 ⊆ dom 𝐺 ↔ ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ∈ dom 𝐺 )
31	29 30	sylibr	⊢ ( 𝜑 → 𝒫 𝐵 ⊆ dom 𝐺 )
32	3	dmeqd	⊢ ( 𝜑 → dom 𝐺 = dom ( glb ‘ 𝐾 ) )
33	31 19 32	3sstr3d	⊢ ( 𝜑 → 𝒫 ( Base ‘ 𝐾 ) ⊆ dom ( glb ‘ 𝐾 ) )
34	27 33	eqssd	⊢ ( 𝜑 → dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) )
35	7 9 23	isclat	⊢ ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) ) )
36	35	biimpri	⊢ ( ( 𝐾 ∈ Poset ∧ ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) ) → 𝐾 ∈ CLat )
37	4 22 34 36	syl12anc	⊢ ( 𝜑 → 𝐾 ∈ CLat )