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

Metamath Proof Explorer

Theorem islln

Description: The predicate "is a lattice line". (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 islln 
|- ( K e. D -> ( X e. 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 1 2 3 4 llnset 
 |-  ( K e. D -> N = { x e. B | E. p e. A p C x } )
6 5 eleq2d 
 |-  ( K e. D -> ( X e. N <-> X e. { x e. B | E. p e. A p C x } ) )
7 breq2 
 |-  ( x = X -> ( p C x <-> p C X ) )
8 7 rexbidv 
 |-  ( x = X -> ( E. p e. A p C x <-> E. p e. A p C X ) )
9 8 elrab 
 |-  ( X e. { x e. B | E. p e. A p C x } <-> ( X e. B /\ E. p e. A p C X ) )
10 6 9 bitrdi 
 |-  ( K e. D -> ( X e. N <-> ( X e. B /\ E. p e. A p C X ) ) )