Theorem atbase 39788

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32440 analog.) (Contributed by NM, 10-Oct-2011.)

Hypotheses

Ref	Expression
atombase.b	⊢ 𝐵 = (Base‘𝐾)
atombase.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
atbase	⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Proof of Theorem atbase

Step	Hyp	Ref	Expression
1		n0i 4275	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2745	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 329	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6826	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 141	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2740	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2740	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 39785	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 499	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 694	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  Vcvv 3432  ∅c0 4268   class class class wbr 5079  ‘cfv 6492  Basecbs 17177  0.cp0 18385   ⋖ ccvr 39761  Atomscatm 39762

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-ats 39766

This theorem is referenced by:  atssbase  39789  0ltat  39790  leatb  39791  meetat  39795  atnle0  39808  atlen0  39809  atcmp  39810  atcvreq0  39813  atncvrN  39814  atnle  39816  atnem0  39817  atlatmstc  39818  atlatle  39819  cvlexch2  39828  cvlexchb1  39829  cvlexchb2  39830  cvlatexchb1  39833  cvlatexchb2  39834  cvlatexch1  39835  cvlatexch2  39836  cvlatexch3  39837  cvlcvr1  39838  cvlcvrp  39839  cvlatcvr1  39840  cvlatcvr2  39841  cvlsupr2  39842  cvlsupr7  39847  cvlsupr8  39848  hlatjcl  39866  hlatjcom  39867  hlatjidm  39868  hlatjass  39869  hlatj32  39871  hlatj4  39873  hlatlej1  39874  atnlej1  39878  atnlej2  39879  hlrelat5N  39900  hlrelat  39901  hlrelat2  39902  exatleN  39903  cvr2N  39910  hlrelat3  39911  cvrval3  39912  cvrval5  39914  cvrexchlem  39918  cvratlem  39920  cvrat  39921  atcvr0eq  39925  lnnat  39926  cvrat2  39928  atcvrneN  39929  atcvrj1  39930  atcvrj2b  39931  atltcvr  39934  atle  39935  atlelt  39937  2atlt  39938  atexchcvrN  39939  cvrat3  39941  cvrat4  39942  cvrat42  39943  2atjm  39944  atbtwn  39945  3noncolr2  39948  4noncolr3  39952  athgt  39955  3dim0  39956  3dimlem3a  39959  3dimlem3OLDN  39961  3dimlem4a  39962  3dimlem4OLDN  39964  3dim3  39968  2dim  39969  1cvratex  39972  1cvrjat  39974  1cvrat  39975  ps-1  39976  ps-2  39977  hlatexch3N  39979  hlatexch4  39980  ps-2b  39981  3atlem1  39982  3atlem2  39983  3atlem4  39985  3atlem5  39986  3atlem6  39987  3at  39989  islln3  40009  llnnleat  40012  llnn0  40015  llnle  40017  llnexatN  40020  llncmp  40021  2llnmat  40023  2at0mat0  40024  2atm  40026  ps-2c  40027  lplni2  40036  lplnle  40039  lplnnle2at  40040  lplnn0N  40046  islpln2a  40047  2atmat  40060  lplnexllnN  40063  2llnjaN  40065  2llnm4  40069  2llnmeqat  40070  lvoli3  40076  islvol5  40078  lvoli2  40080  lvolnle3at  40081  3atnelvolN  40085  lvoln0N  40090  islvol2aN  40091  4atlem3  40095  4atlem3a  40096  4atlem3b  40097  4atlem4a  40098  4atlem4b  40099  4atlem4c  40100  4atlem4d  40101  4atlem9  40102  4atlem10a  40103  4atlem10  40105  4atlem11a  40106  4atlem11b  40107  4atlem11  40108  4atlem12a  40109  4atlem12b  40110  4atlem12  40111  4at2  40113  lplncvrlvol2  40114  2lplnja  40118  dalempeb  40138  dalemqeb  40139  dalemreb  40140  dalemseb  40141  dalemteb  40142  dalemueb  40143  dalem3  40163  dalem16  40178  dalemcceb  40188  dalem21  40193  dalem25  40197  dalem38  40209  dalem39  40210  dalem43  40214  dalem44  40215  dalem45  40216  dalem53  40224  dalem54  40225  dalem55  40226  dalem57  40228  dalem60  40231  snatpsubN  40249  linepsubN  40251  pmaple  40260  pmapat  40262  pmap1N  40266  pmapsub  40267  pmapglbx  40268  isline2  40273  linepmap  40274  isline3  40275  isline4N  40276  lneq2at  40277  lncvrelatN  40280  lncmp  40282  2lnat  40283  2atm2atN  40284  2llnma1b  40285  2llnma1  40286  2llnma3r  40287  cdlema1N  40290  cdlemblem  40292  cdlemb  40293  elpaddn0  40299  paddcom  40312  paddasslem2  40320  paddasslem5  40323  paddasslem12  40330  paddasslem13  40331  pmapjoin  40351  pmapjat1  40352  pmapjat2  40353  pmapjlln1  40354  atmod1i1  40356  atmod1i2  40358  llnmod1i2  40359  atmod2i1  40360  atmod2i2  40361  atmod3i1  40363  atmod3i2  40364  atmod4i1  40365  atmod4i2  40366  llnexchb2lem  40367  llnexchb2  40368  dalawlem2  40371  dalawlem3  40372  dalawlem5  40374  dalawlem6  40375  dalawlem7  40376  dalawlem8  40377  dalawlem11  40380  dalawlem12  40381  polval2N  40405  pol1N  40409  polatN  40430  2polatN  40431  paddatclN  40448  linepsubclN  40450  lhp2lt  40500  lhp0lt  40502  lhpexle2lem  40508  lhpexle3lem  40510  lhpjat2  40520  lhpj1  40521  lhpmcvr3  40524  lhpmcvr4N  40525  lhpmcvr5N  40526  lhpmcvr6N  40527  lhpmatb  40530  lhp2at0  40531  lhp2atnle  40532  lhp2at0nle  40534  lhprelat3N  40539  lhple  40541  lhpat4N  40543  lhpat3  40545  4atexlemtlw  40566  4atexlemc  40568  4atexlemnclw  40569  4atexlemcnd  40571  4atex2-0aOLDN  40577  lauteq  40594  ltrnid  40634  ltrnel  40638  ltrnat  40639  ltrncnvat  40640  ltrncnvel  40641  ltrncoval  40644  ltrncnv  40645  ltrn11at  40646  ltrneq2  40647  ltrneq  40648  idltrn  40649  trlval2  40662  trlcnv  40664  trljat1  40665  trljat2  40666  ltrnideq  40674  arglem1N  40689  cdlemc1  40690  cdlemc2  40691  cdlemc4  40693  cdlemc5  40694  cdlemc6  40695  cdlemd1  40697  cdlemd2  40698  cdlemd3  40699  cdlemd4  40700  cdlemd7  40703  cdleme0aa  40709  cdleme0b  40711  cdleme0c  40712  cdleme0cp  40713  cdleme0cq  40714  cdleme0e  40716  cdleme0fN  40717  cdleme1b  40725  cdleme1  40726  cdleme2  40727  cdleme3b  40728  cdleme3c  40729  cdleme3e  40731  cdleme3g  40733  cdleme3h  40734  cdleme3  40736  cdleme5  40739  cdleme7d  40745  cdleme7e  40746  cdleme7ga  40747  cdleme7  40748  cdleme8  40749  cdleme9  40752  cdleme10  40753  cdleme11c  40760  cdleme11e  40762  cdleme11fN  40763  cdleme11g  40764  cdleme11k  40767  cdleme11  40769  cdleme15b  40774  cdleme15  40777  cdleme16b  40778  cdleme17b  40786  cdleme17c  40787  cdlemednpq  40798  cdleme20zN  40800  cdleme19a  40802  cdleme20bN  40809  cdleme20d  40811  cdleme20j  40817  cdleme21c  40826  cdleme22aa  40838  cdleme22b  40840  cdleme22cN  40841  cdleme22d  40842  cdleme22e  40843  cdleme22eALTN  40844  cdleme23b  40849  cdleme23c  40850  cdleme27N  40868  cdleme28a  40869  cdleme30a  40877  cdlemefrs29pre00  40894  cdlemefrs29bpre0  40895  cdlemefrs29cpre1  40897  cdlemefrs32fva  40899  cdlemefrs32fva1  40900  cdlemefr32snb  40904  cdlemefs32snb  40914  cdleme32snb  40935  cdleme32fva  40936  cdleme32fva1  40937  cdleme32fvaw  40938  cdleme35a  40947  cdleme35fnpq  40948  cdleme35b  40949  cdleme35c  40950  cdleme35f  40953  cdleme42c  40971  cdleme42e  40978  cdleme42h  40981  cdleme42i  40982  cdleme42ke  40984  cdleme42keg  40985  cdleme42mgN  40987  cdleme17d4  40996  cdleme48fvg  40999  cdleme48bw  41001  cdlemeg46req  41028  cdleme50trn3  41052  cdlemf1  41060  cdlemf2  41061  trlord  41068  ltrniotacnvval  41081  cdlemg2fv2  41099  cdlemg2l  41102  cdlemg7fvbwN  41106  cdlemg4c  41111  cdlemg4  41116  cdlemg6c  41119  cdlemg8b  41127  cdlemg11b  41141  cdlemg13a  41150  cdlemg17a  41160  cdlemg17h  41167  cdlemg17  41176  cdlemg18b  41178  cdlemg19a  41182  cdlemg27a  41191  cdlemg27b  41195  cdlemg31a  41196  cdlemg31b  41197  cdlemg31d  41199  cdlemg33b0  41200  cdlemg33a  41205  cdlemg35  41212  trlcolem  41225  cdlemg42  41228  cdlemg44a  41230  cdlemg46  41234  cdlemh1  41314  cdlemh2  41315  cdlemh  41316  cdlemi1  41317  cdlemi  41319  cdlemk3  41332  cdlemk4  41333  cdlemkvcl  41341  cdlemk7  41347  cdlemk11  41348  cdlemk15  41354  cdlemk1u  41358  cdlemk7u  41369  cdlemk11u  41370  cdlemk37  41413  cdlemk39  41415  cdlemkid1  41421  cdlemkid2  41423  cdlemk48  41449  cdlemk50  41451  cdlemk51  41452  cdlemk52  41453  dia2dimlem1  41563  dia2dimlem2  41564  dia2dimlem3  41565  dia2dimlem5  41567  dia2dimlem7  41569  dia2dimlem9  41571  dia2dimlem10  41572  dia2dimlem12  41574  dia2dimlem13  41575  cdlemm10N  41617  cdlemn2  41694  cdlemn3  41696  cdlemn9  41704  cdlemn10  41705  dihjustlem  41715  dihord1  41717  dihord2pre2  41725  dihvalcqat  41738  dib2dim  41742  dih2dimb  41743  dih2dimbALTN  41744  dihord5apre  41761  dihglbcpreN  41799  dihmeetlem3N  41804  dihmeetlem6  41808  dihjatc1  41810  dihjatc2N  41811  dihjatc3  41812  dihmeetlem9N  41814  dihmeetlem10N  41815  dihmeetlem11N  41816  dihmeetlem13N  41818  dihmeetlem15N  41820  dihmeetlem16N  41821  dihmeetlem17N  41822  dihatexv2  41838  dihjatb  41915  dihjatc  41916  dihjatcclem1  41917  dihjatcclem2  41918  dihjatcclem4  41920  dihjat  41922  dihjat3  41931  dihjat5N  41936  dvh4dimat  41937