Metamath Proof Explorer


Theorem llnset

Description: The set of lattice lines in a Hilbert lattice. (Contributed by NM, 16-Jun-2012)

Ref Expression
Hypotheses llnset.b
|- B = ( Base ` K )
llnset.c
|- C = ( 
llnset.a
|- A = ( Atoms ` K )
llnset.n
|- N = ( LLines ` K )
Assertion llnset
|- ( K e. D -> N = { x e. B | E. p e. A p C x } )

Proof

Step Hyp Ref Expression
1 llnset.b
 |-  B = ( Base ` K )
2 llnset.c
 |-  C = ( 
3 llnset.a
 |-  A = ( Atoms ` K )
4 llnset.n
 |-  N = ( LLines ` K )
5 elex
 |-  ( K e. D -> K e. _V )
6 fveq2
 |-  ( k = K -> ( Base ` k ) = ( Base ` K ) )
7 6 1 eqtr4di
 |-  ( k = K -> ( Base ` k ) = B )
8 fveq2
 |-  ( k = K -> ( Atoms ` k ) = ( Atoms ` K ) )
9 8 3 eqtr4di
 |-  ( k = K -> ( Atoms ` k ) = A )
10 fveq2
 |-  ( k = K -> ( 
11 10 2 eqtr4di
 |-  ( k = K -> ( 
12 11 breqd
 |-  ( k = K -> ( p (  p C x ) )
13 9 12 rexeqbidv
 |-  ( k = K -> ( E. p e. ( Atoms ` k ) p (  E. p e. A p C x ) )
14 7 13 rabeqbidv
 |-  ( k = K -> { x e. ( Base ` k ) | E. p e. ( Atoms ` k ) p ( 
15 df-llines
 |-  LLines = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( Atoms ` k ) p ( 
16 1 fvexi
 |-  B e. _V
17 16 rabex
 |-  { x e. B | E. p e. A p C x } e. _V
18 14 15 17 fvmpt
 |-  ( K e. _V -> ( LLines ` K ) = { x e. B | E. p e. A p C x } )
19 4 18 syl5eq
 |-  ( K e. _V -> N = { x e. B | E. p e. A p C x } )
20 5 19 syl
 |-  ( K e. D -> N = { x e. B | E. p e. A p C x } )