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 ` K )
lineset.j 
|- .\/ = ( join ` K )
lineset.a 
|- A = ( Atoms ` K )
lineset.n 
|- N = ( Lines ` K )
Assertion lineset 
|- ( K e. B -> N = { s | E. q e. A E. r e. A ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) } )

Proof

Step Hyp Ref Expression
1 lineset.l 
 |-  .<_ = ( le ` K )
2 lineset.j 
 |-  .\/ = ( join ` K )
3 lineset.a 
 |-  A = ( Atoms ` K )
4 lineset.n 
 |-  N = ( Lines ` K )
5 elex 
 |-  ( K e. B -> K e. _V )
6 fveq2 
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
7 6 3 eqtr4di 
 |-  ( k = K -> ( Atoms ` k ) = A )
8 fveq2 
 |-  ( k = K -> ( le ` k ) = ( le ` K ) )
9 8 1 eqtr4di 
 |-  ( k = K -> ( le ` k ) = .<_ )
10 9 breqd 
 |-  ( k = K -> ( p ( le ` k ) ( q ( join ` k ) r ) <-> p .<_ ( q ( join ` k ) r ) ) )
11 fveq2 
 |-  ( k = K -> ( join ` k ) = ( join ` K ) )
12 11 2 eqtr4di 
 |-  ( k = K -> ( join ` k ) = .\/ )
13 12 oveqd 
 |-  ( k = K -> ( q ( join ` k ) r ) = ( q .\/ r ) )
14 13 breq2d 
 |-  ( k = K -> ( p .<_ ( q ( join ` k ) r ) <-> p .<_ ( q .\/ r ) ) )
15 10 14 bitrd 
 |-  ( k = K -> ( p ( le ` k ) ( q ( join ` k ) r ) <-> p .<_ ( q .\/ r ) ) )
16 7 15 rabeqbidv 
 |-  ( k = K -> { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } = { p e. A | p .<_ ( q .\/ r ) } )
17 16 eqeq2d 
 |-  ( k = K -> ( s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } <-> s = { p e. A | p .<_ ( q .\/ r ) } ) )
18 17 anbi2d 
 |-  ( k = K -> ( ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } ) <-> ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) ) )
19 7 18 rexeqbidv 
 |-  ( k = K -> ( E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } ) <-> E. r e. A ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) ) )
20 7 19 rexeqbidv 
 |-  ( k = K -> ( E. q e. ( Atoms ` k ) E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } ) <-> E. q e. A E. r e. A ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) ) )
21 20 abbidv 
 |-  ( k = K -> { s | E. q e. ( Atoms ` k ) E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } ) } = { s | E. q e. A E. r e. A ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) } )
22 df-lines 
 |-  Lines = ( k e. _V |-> { s | E. q e. ( Atoms ` k ) E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } ) } )
23 3 fvexi 
 |-  A e. _V
24 df-sn 
 |-  { { p e. A | p .<_ ( q .\/ r ) } } = { s | s = { p e. A | p .<_ ( q .\/ r ) } }
25 snex 
 |-  { { p e. A | p .<_ ( q .\/ r ) } } e. _V
26 24 25 eqeltrri 
 |-  { s | s = { p e. A | p .<_ ( q .\/ r ) } } e. _V
27 simpr 
 |-  ( ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) -> s = { p e. A | p .<_ ( q .\/ r ) } )
28 27 ss2abi 
 |-  { s | ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) } C_ { s | s = { p e. A | p .<_ ( q .\/ r ) } }
29 26 28 ssexi 
 |-  { s | ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) } e. _V
30 23 23 29 ab2rexex2 
 |-  { s | E. q e. A E. r e. A ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) } e. _V
31 21 22 30 fvmpt 
 |-  ( K e. _V -> ( Lines ` K ) = { s | E. q e. A E. r e. A ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) } )
32 4 31 syl5eq 
 |-  ( K e. _V -> N = { s | E. q e. A E. r e. A ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) } )
33 5 32 syl 
 |-  ( K e. B -> N = { s | E. q e. A E. r e. A ( q =/= r /\ s = { p e. A | p .<_ ( q .\/ r ) } ) } )