Metamath Proof Explorer


Theorem llnbase

Description: A lattice line is a lattice element. (Contributed by NM, 16-Jun-2012)

Ref Expression
Hypotheses llnbase.b
|- B = ( Base ` K )
llnbase.n
|- N = ( LLines ` K )
Assertion llnbase
|- ( X e. N -> X e. B )

Proof

Step Hyp Ref Expression
1 llnbase.b
 |-  B = ( Base ` K )
2 llnbase.n
 |-  N = ( LLines ` K )
3 n0i
 |-  ( X e. N -> -. N = (/) )
4 2 eqeq1i
 |-  ( N = (/) <-> ( LLines ` K ) = (/) )
5 3 4 sylnib
 |-  ( X e. N -> -. ( LLines ` K ) = (/) )
6 fvprc
 |-  ( -. K e. _V -> ( LLines ` K ) = (/) )
7 5 6 nsyl2
 |-  ( X e. N -> K e. _V )
8 eqid
 |-  ( 
9 eqid
 |-  ( Atoms ` K ) = ( Atoms ` K )
10 1 8 9 2 islln
 |-  ( K e. _V -> ( X e. N <-> ( X e. B /\ E. p e. ( Atoms ` K ) p ( 
11 10 simprbda
 |-  ( ( K e. _V /\ X e. N ) -> X e. B )
12 7 11 mpancom
 |-  ( X e. N -> X e. B )