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

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 )