Theorem llnbase 33119

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

Hypotheses

Ref	Expression
llnbase.b	|- B = ( Base ` K )
llnbase.n	|- N = ( LLines ` K )

Assertion

Ref	Expression
llnbase	|- ( X e. N -> X e. B )

Proof of Theorem llnbase

Dummy variable p is distinct from all other variables.

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

Syntax hints:   -> wi 4   = wceq 1455   e. wcel 1898   E.wrex 2750   _Vcvv 3057   (/)c0 3743   class class class wbr 4416   ` cfv 5601   Basecbs 15170   <o ccvr 32873   Atomscatm 32874   LLinesclln 33101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-iota 5565  df-fun 5603  df-fv 5609  df-llines 33108

This theorem is referenced by:  islln2  33121  llnnleat  33123  llnneat  33124  atcvrlln2  33129  llnexatN  33131  llncmp  33132  2llnmat  33134  islpln3  33143  llnmlplnN  33149  lplnle  33150  lplnnle2at  33151  llncvrlpln2  33167  llncvrlpln  33168  2llnmj  33170  lplncmp  33172  lplnexatN  33173  lplnexllnN  33174  2llnm2N  33178  2llnm3N  33179  2llnm4  33180  2llnmeqat  33181  dalem21  33304  dalem54  33336  dalem55  33337  dalem57  33339  dalem60  33342  llnexchb2lem  33478  llnexchb2  33479  llnexch2N  33480