Definition df-lhyp 34292

Description: Define the set of lattice hyperplanes, which are all lattice elements covered by 1 (i.e. all co-atoms). We call them "hyperplanes" instead of "co-atoms" in analogy with projective geometry hyperplanes. (Contributed by NM, 11-May-2012.)

Assertion

Ref	Expression
df-lhyp	⊢ LHyp = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})

Distinct variable group:   𝑥,𝑘

Detailed syntax breakdown of Definition df-lhyp

Step	Hyp	Ref	Expression
1		clh 34288	. 2 class LHyp
2		vk	. . 3 setvar 𝑘
3		cvv 3173	. . 3 class V
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1474	. . . . 5 class 𝑥
6	2	cv 1474	. . . . . 6 class 𝑘
7		cp1 16861	. . . . . 6 class 1.
8	6, 7	cfv 5804	. . . . 5 class (1.‘𝑘)
9		ccvr 33567	. . . . . 6 class ⋖
10	6, 9	cfv 5804	. . . . 5 class ( ⋖ ‘𝑘)
11	5, 8, 10	wbr 4583	. . . 4 wff 𝑥( ⋖ ‘𝑘)(1.‘𝑘)
12		cbs 15695	. . . . 5 class Base
13	6, 12	cfv 5804	. . . 4 class (Base‘𝑘)
14	11, 4, 13	crab 2900	. . 3 class {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)}
15	2, 3, 14	cmpt 4643	. 2 class (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
16	1, 15	wceq 1475	1 wff LHyp = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})

This definition is referenced by:  lhpset  34299