Definition df-llines

Description: Define the set of all "lattice lines" (lattice elements which cover an atom) in a Hilbert lattice k , in other words all elements of height 2 (or lattice dimension 2 or projective dimension 1). (Contributed by NM, 16-Jun-2012)

	Ref	Expression
Assertion	df-llines	⊢ LLines = ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clln	⊢ LLines
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( Base ‘ 𝑘 )
7		vp	⊢ 𝑝
8		catm	⊢ Atoms
9	5 8	cfv	⊢ ( Atoms ‘ 𝑘 )
10	7	cv	⊢ 𝑝
11		ccvr	⊢ ⋖
12	5 11	cfv	⊢ ( ⋖ ‘ 𝑘 )
13	3	cv	⊢ 𝑥
14	10 13 12	wbr	⊢ 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥
15	14 7 9	wrex	⊢ ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥
16	15 3 6	crab	⊢ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 }
17	1 2 16	cmpt	⊢ ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )
18	0 17	wceq	⊢ LLines = ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( Atoms ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )