Definition df-la 8906

Description: Define the class of all lattices, which are posets in which every two elements have upper and lower bounds.

Assertion

Ref	Expression
df-la	⊢ Lat = {r ∈ Poset∣∀x ∈ dom r∀y ∈ dom r((r supw {x, y}) ∈ dom r ⋀ (r infw {x, y}) ∈ dom r)}

Distinct variable group:   x,r,y

Detailed syntax breakdown of Definition df-la

Step	Hyp	Ref	Expression
1		cla 8900	. 2 class Lat
2		vr	. . . . . . . . 9 set r
3	2	cv 991	. . . . . . . 8 class r
4		vx	. . . . . . . . . 10 set x
5	4	cv 991	. . . . . . . . 9 class x
6		vy	. . . . . . . . . 10 set y
7	6	cv 991	. . . . . . . . 9 class y
8	5, 7	cpr 2468	. . . . . . . 8 class {x, y}
9		cspw 8896	. . . . . . . 8 class supw
10	3, 8, 9	co 4021	. . . . . . 7 class (r supw {x, y})
11	3	cdm 3251	. . . . . . 7 class dom r
12	10, 11	wcel 994	. . . . . 6 wff (r supw {x, y}) ∈ dom r
13		cinf 8897	. . . . . . . 8 class infw
14	3, 8, 13	co 4021	. . . . . . 7 class (r infw {x, y})
15	14, 11	wcel 994	. . . . . 6 wff (r infw {x, y}) ∈ dom r
16	12, 15	wa 221	. . . . 5 wff ((r supw {x, y}) ∈ dom r ⋀ (r infw {x, y}) ∈ dom r)
17	16, 6, 11	wral 1691	. . . 4 wff ∀y ∈ dom r((r supw {x, y}) ∈ dom r ⋀ (r infw {x, y}) ∈ dom r)
18	17, 4, 11	wral 1691	. . 3 wff ∀x ∈ dom r∀y ∈ dom r((r supw {x, y}) ∈ dom r ⋀ (r infw {x, y}) ∈ dom r)
19		cps 8895	. . 3 class Poset
20	18, 2, 19	crab 1694	. 2 class {r ∈ Poset∣∀x ∈ dom r∀y ∈ dom r((r supw {x, y}) ∈ dom r ⋀ (r infw {x, y}) ∈ dom r)}
21	1, 20	wceq 992	1 wff Lat = {r ∈ Poset∣∀x ∈ dom r∀y ∈ dom r((r supw {x, y}) ∈ dom r ⋀ (r infw {x, y}) ∈ dom r)}

This definition is referenced by:  isla 8929

Copyright terms: Public domain