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 )