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

Metamath Proof Explorer

Theorem lineset

Description: The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011)

Ref Expression
Hypotheses lineset.l ⊢ ≤ = ( le ‘ 𝐾 )
lineset.j ⊢ ∨ = ( join ‘ 𝐾 )
lineset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
lineset.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
Assertion lineset ( 𝐾 ∈ 𝐵 → 𝑁 = { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )

Proof

Step Hyp Ref Expression
1 lineset.l ⊢ ≤ = ( le ‘ 𝐾 )
2 lineset.j ⊢ ∨ = ( join ‘ 𝐾 )
3 lineset.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4 lineset.n ⊢ 𝑁 = ( Lines ‘ 𝐾 )
5 elex ⊢ ( 𝐾 ∈ 𝐵 → 𝐾 ∈ V )
6 fveq2 ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = ( Atoms ‘ 𝐾 ) )
7 6 3 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( Atoms ‘ 𝑘 ) = 𝐴 )
8 fveq2 ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ( le ‘ 𝐾 ) )
9 8 1 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( le ‘ 𝑘 ) = ≤ )
10 9 breqd ⊢ ( 𝑘 = 𝐾 → ( 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) ↔ 𝑝 ≤ ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) ) )
11 fveq2 ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ( join ‘ 𝐾 ) )
12 11 2 eqtr4di ⊢ ( 𝑘 = 𝐾 → ( join ‘ 𝑘 ) = ∨ )
13 12 oveqd ⊢ ( 𝑘 = 𝐾 → ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) = ( 𝑞 ∨ 𝑟 ) )
14 13 breq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑝 ≤ ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) ↔ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) )
15 10 14 bitrd ⊢ ( 𝑘 = 𝐾 → ( 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) ↔ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) ) )
16 7 15 rabeqbidv ⊢ ( 𝑘 = 𝐾 → { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } )
17 16 eqeq2d ⊢ ( 𝑘 = 𝐾 → ( 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ↔ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) )
18 17 anbi2d ⊢ ( 𝑘 = 𝐾 → ( ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) ↔ ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
19 7 18 rexeqbidv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) ↔ ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
20 7 19 rexeqbidv ⊢ ( 𝑘 = 𝐾 → ( ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) ↔ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) ) )
21 20 abbidv ⊢ ( 𝑘 = 𝐾 → { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) } = { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )
22 df-lines ⊢ Lines = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) } )
23 3 fvexi ⊢ 𝐴 ∈ V
24 df-sn ⊢ { { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } } = { 𝑠 ∣ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } }
25 snex ⊢ { { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } } ∈ V
26 24 25 eqeltrri ⊢ { 𝑠 ∣ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } } ∈ V
27 simpr ⊢ ( ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) → 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } )
28 27 ss2abi ⊢ { 𝑠 ∣ ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } ⊆ { 𝑠 ∣ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } }
29 26 28 ssexi ⊢ { 𝑠 ∣ ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } ∈ V
30 23 23 29 ab2rexex2 ⊢ { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } ∈ V
31 21 22 30 fvmpt ⊢ ( 𝐾 ∈ V → ( Lines ‘ 𝐾 ) = { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )
32 4 31 eqtrid ⊢ ( 𝐾 ∈ V → 𝑁 = { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )
33 5 32 syl ⊢ ( 𝐾 ∈ 𝐵 → 𝑁 = { 𝑠 ∣ ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ 𝐴 ∣ 𝑝 ≤ ( 𝑞 ∨ 𝑟 ) } ) } )