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

Metamath Proof Explorer

Definition df-lines

Description: Define set of all projective lines for a Hilbert lattice (actually in any set at all, for simplicity). The join of two distinct atoms equals a line. Definition of lines in item 1 of Holland95 p. 222. (Contributed by NM, 19-Sep-2011)

Ref Expression
Assertion df-lines Lines = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clines ⊢ Lines
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vs ⊢ 𝑠
4 vq ⊢ 𝑞
5 catm ⊢ Atoms
6 1 cv ⊢ 𝑘
7 6 5 cfv ⊢ ( Atoms ‘ 𝑘 )
8 vr ⊢ 𝑟
9 4 cv ⊢ 𝑞
10 8 cv ⊢ 𝑟
11 9 10 wne ⊢ 𝑞 ≠ 𝑟
12 3 cv ⊢ 𝑠
13 vp ⊢ 𝑝
14 13 cv ⊢ 𝑝
15 cple ⊢ le
16 6 15 cfv ⊢ ( le ‘ 𝑘 )
17 cjn ⊢ join
18 6 17 cfv ⊢ ( join ‘ 𝑘 )
19 9 10 18 co ⊢ ( 𝑞 ( join ‘ 𝑘 ) 𝑟 )
20 14 19 16 wbr ⊢ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 )
21 20 13 7 crab ⊢ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) }
22 12 21 wceq ⊢ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) }
23 11 22 wa ⊢ ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } )
24 23 8 7 wrex ⊢ ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } )
25 24 4 7 wrex ⊢ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } )
26 25 3 cab ⊢ { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) }
27 1 2 26 cmpt ⊢ ( 𝑘 ∈ V ↦ { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) } )
28 0 27 wceq ⊢ Lines = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) } )