Definition df-lat 17938

Description: Define the class of all lattices. A lattice is a poset in which the join and meet of any two elements always exists. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)

Assertion

Ref	Expression
df-lat	⊢ Lat = {𝑝 ∈ Poset ∣ (dom (join‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)) ∧ dom (meet‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)))}

Detailed syntax breakdown of Definition df-lat

Step	Hyp	Ref	Expression
1		clat 17937	. 2 class Lat
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1542	. . . . . . 7 class 𝑝
4		cjn 17818	. . . . . . 7 class join
5	3, 4	cfv 6380	. . . . . 6 class (join‘𝑝)
6	5	cdm 5551	. . . . 5 class dom (join‘𝑝)
7		cbs 16760	. . . . . . 7 class Base
8	3, 7	cfv 6380	. . . . . 6 class (Base‘𝑝)
9	8, 8	cxp 5549	. . . . 5 class ((Base‘𝑝) × (Base‘𝑝))
10	6, 9	wceq 1543	. . . 4 wff dom (join‘𝑝) = ((Base‘𝑝) × (Base‘𝑝))
11		cmee 17819	. . . . . . 7 class meet
12	3, 11	cfv 6380	. . . . . 6 class (meet‘𝑝)
13	12	cdm 5551	. . . . 5 class dom (meet‘𝑝)
14	13, 9	wceq 1543	. . . 4 wff dom (meet‘𝑝) = ((Base‘𝑝) × (Base‘𝑝))
15	10, 14	wa 399	. . 3 wff (dom (join‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)) ∧ dom (meet‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)))
16		cpo 17814	. . 3 class Poset
17	15, 2, 16	crab 3065	. 2 class {𝑝 ∈ Poset ∣ (dom (join‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)) ∧ dom (meet‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)))}
18	1, 17	wceq 1543	1 wff Lat = {𝑝 ∈ Poset ∣ (dom (join‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)) ∧ dom (meet‘𝑝) = ((Base‘𝑝) × (Base‘𝑝)))}

This definition is referenced by:  islat  17939