This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )