Theorem llnbase 33459

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 3740	. . . 4 |- ( X e. N -> -. N = (/) )
2		llnbase.n	. . . . 5 |- N = ( LLines ` K )
3	2	eqeq1i 2458	. . . 4 |- ( N = (/) <-> ( LLines ` K ) = (/) )
4	1, 3	sylnib 304	. . 3 |- ( X e. N -> -. ( LLines ` K ) = (/) )
5		fvprc 5783	. . 3 |- ( -. K e. _V -> ( LLines ` K ) = (/) )
6	4, 5	nsyl2 127	. 2 |- ( X e. N -> K e. _V )
7		llnbase.b	. . . 4 |- B = ( Base ` K )
8		eqid 2451	. . . 4 |- ( <o ` K ) = ( <o ` K )
9		eqid 2451	. . . 4 |- ( Atoms ` K ) = ( Atoms ` K )
10	7, 8, 9, 2	islln 33456	. . 3 |- ( K e. _V -> ( X e. N <-> ( X e. B /\ E. p e. ( Atoms ` K ) p ( <o ` K ) X ) ) )
11	10	simprbda 623	. 2 |- ( ( K e. _V /\ X e. N ) -> X e. B )
12	6, 11	mpancom 669	1 |- ( X e. N -> X e. B )

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758   E.wrex 2796   _Vcvv 3068   (/)c0 3735   class class class wbr 4390   ` cfv 5516   Basecbs 14276   <o ccvr 33213   Atomscatm 33214   LLinesclln 33441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-iota 5479  df-fun 5518  df-fv 5524  df-llines 33448

This theorem is referenced by:  islln2  33461  llnnleat  33463  llnneat  33464  atcvrlln2  33469  llnexatN  33471  llncmp  33472  2llnmat  33474  islpln3  33483  llnmlplnN  33489  lplnle  33490  lplnnle2at  33491  llncvrlpln2  33507  llncvrlpln  33508  2llnmj  33510  lplncmp  33512  lplnexatN  33513  lplnexllnN  33514  2llnm2N  33518  2llnm3N  33519  2llnm4  33520  2llnmeqat  33521  dalem21  33644  dalem54  33676  dalem55  33677  dalem57  33679  dalem60  33682  llnexchb2lem  33818  llnexchb2  33819  llnexch2N  33820