Theorem atbase 40104

Description: An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32733 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 4296	. . . 4 ⊢ (𝑃 ∈ 𝐴 → ¬ 𝐴 = ∅)
2		atombase.a	. . . . 5 ⊢ 𝐴 = (Atoms‘𝐾)
3	2	eqeq1i 2771	. . . 4 ⊢ (𝐴 = ∅ ↔ (Atoms‘𝐾) = ∅)
4	1, 3	sylnib 331	. . 3 ⊢ (𝑃 ∈ 𝐴 → ¬ (Atoms‘𝐾) = ∅)
5		fvprc 6880	. . 3 ⊢ (¬ 𝐾 ∈ V → (Atoms‘𝐾) = ∅)
6	4, 5	nsyl2 142	. 2 ⊢ (𝑃 ∈ 𝐴 → 𝐾 ∈ V)
7		atombase.b	. . . 4 ⊢ 𝐵 = (Base‘𝐾)
8		eqid 2766	. . . 4 ⊢ (0.‘𝐾) = (0.‘𝐾)
9		eqid 2766	. . . 4 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
10	7, 8, 9, 2	isat 40101	. . 3 ⊢ (𝐾 ∈ V → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ (0.‘𝐾)( ⋖ ‘𝐾)𝑃)))
11	10	simprbda 504	. 2 ⊢ ((𝐾 ∈ V ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ 𝐵)
12	6, 11	mpancom 701	1 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  Vcvv 3458  ∅c0 4289   class class class wbr 5114  ‘cfv 6543  Basecbs 17294  0.cp0 18502   ⋖ ccvr 40077  Atomscatm 40078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-iota 6499  df-fun 6545  df-fv 6551  df-ats 40082

This theorem is used by:  atssbase  40105  0ltat  40106  leatb  40107  meetat  40111  atnle0  40124  atlen0  40125  atcmp  40126  atcvreq0  40129  atncvrN  40130  atnle  40132  atnem0  40133  atlatmstc  40134  atlatle  40135  cvlexch2  40144  cvlexchb1  40145  cvlexchb2  40146  cvlatexchb1  40149  cvlatexchb2  40150  cvlatexch1  40151  cvlatexch2  40152  cvlatexch3  40153  cvlcvr1  40154  cvlcvrp  40155  cvlatcvr1  40156  cvlatcvr2  40157  cvlsupr2  40158  cvlsupr7  40163  cvlsupr8  40164  hlatjcl  40182  hlatjcom  40183  hlatjidm  40184  hlatjass  40185  hlatj32  40187  hlatj4  40189  hlatlej1  40190  atnlej1  40194  atnlej2  40195  hlrelat5N  40216  hlrelat  40217  hlrelat2  40218  exatleN  40219  cvr2N  40226  hlrelat3  40227  cvrval3  40228  cvrval5  40230  cvrexchlem  40234  cvratlem  40236  cvrat  40237  atcvr0eq  40241  lnnat  40242  cvrat2  40244  atcvrneN  40245  atcvrj1  40246  atcvrj2b  40247  atltcvr  40250  atle  40251  atlelt  40253  2atlt  40254  atexchcvrN  40255  cvrat3  40257  cvrat4  40258  cvrat42  40259  2atjm  40260  atbtwn  40261  3noncolr2  40264  4noncolr3  40268  athgt  40271  3dim0  40272  3dimlem3a  40275  3dimlem3OLDN  40277  3dimlem4a  40278  3dimlem4OLDN  40280  3dim3  40284  2dim  40285  1cvratex  40288  1cvrjat  40290  1cvrat  40291  ps-1  40292  ps-2  40293  hlatexch3N  40295  hlatexch4  40296  ps-2b  40297  3atlem1  40298  3atlem2  40299  3atlem4  40301  3atlem5  40302  3atlem6  40303  3at  40305  islln3  40325  llnnleat  40328  llnn0  40331  llnle  40333  llnexatN  40336  llncmp  40337  2llnmat  40339  2at0mat0  40340  2atm  40342  ps-2c  40343  lplni2  40352  lplnle  40355  lplnnle2at  40356  lplnn0N  40362  islpln2a  40363  2atmat  40376  lplnexllnN  40379  2llnjaN  40381  2llnm4  40385  2llnmeqat  40386  lvoli3  40392  islvol5  40394  lvoli2  40396  lvolnle3at  40397  3atnelvolN  40401  lvoln0N  40406  islvol2aN  40407  4atlem3  40411  4atlem3a  40412  4atlem3b  40413  4atlem4a  40414  4atlem4b  40415  4atlem4c  40416  4atlem4d  40417  4atlem9  40418  4atlem10a  40419  4atlem10  40421  4atlem11a  40422  4atlem11b  40423  4atlem11  40424  4atlem12a  40425  4atlem12b  40426  4atlem12  40427  4at2  40429  lplncvrlvol2  40430  2lplnja  40434  dalempeb  40454  dalemqeb  40455  dalemreb  40456  dalemseb  40457  dalemteb  40458  dalemueb  40459  dalem3  40479  dalem16  40494  dalemcceb  40504  dalem21  40509  dalem25  40513  dalem38  40525  dalem39  40526  dalem43  40530  dalem44  40531  dalem45  40532  dalem53  40540  dalem54  40541  dalem55  40542  dalem57  40544  dalem60  40547  snatpsubN  40565  linepsubN  40567  pmaple  40576  pmapat  40578  pmap1N  40582  pmapsub  40583  pmapglbx  40584  isline2  40589  linepmap  40590  isline3  40591  isline4N  40592  lneq2at  40593  lncvrelatN  40596  lncmp  40598  2lnat  40599  2atm2atN  40600  2llnma1b  40601  2llnma1  40602  2llnma3r  40603  cdlema1N  40606  cdlemblem  40608  cdlemb  40609  elpaddn0  40615  paddcom  40628  paddasslem2  40636  paddasslem5  40639  paddasslem12  40646  paddasslem13  40647  pmapjoin  40667  pmapjat1  40668  pmapjat2  40669  pmapjlln1  40670  atmod1i1  40672  atmod1i2  40674  llnmod1i2  40675  atmod2i1  40676  atmod2i2  40677  atmod3i1  40679  atmod3i2  40680  atmod4i1  40681  atmod4i2  40682  llnexchb2lem  40683  llnexchb2  40684  dalawlem2  40687  dalawlem3  40688  dalawlem5  40690  dalawlem6  40691  dalawlem7  40692  dalawlem8  40693  dalawlem11  40696  dalawlem12  40697  polval2N  40721  pol1N  40725  polatN  40746  2polatN  40747  paddatclN  40764  linepsubclN  40766  lhp2lt  40816  lhp0lt  40818  lhpexle2lem  40824  lhpexle3lem  40826  lhpjat2  40836  lhpj1  40837  lhpmcvr3  40840  lhpmcvr4N  40841  lhpmcvr5N  40842  lhpmcvr6N  40843  lhpmatb  40846  lhp2at0  40847  lhp2atnle  40848  lhp2at0nle  40850  lhprelat3N  40855  lhple  40857  lhpat4N  40859  lhpat3  40861  4atexlemtlw  40882  4atexlemc  40884  4atexlemnclw  40885  4atexlemcnd  40887  4atex2-0aOLDN  40893  lauteq  40910  ltrnid  40950  ltrnel  40954  ltrnat  40955  ltrncnvat  40956  ltrncnvel  40957  ltrncoval  40960  ltrncnv  40961  ltrn11at  40962  ltrneq2  40963  ltrneq  40964  idltrn  40965  trlval2  40978  trlcnv  40980  trljat1  40981  trljat2  40982  ltrnideq  40990  arglem1N  41005  cdlemc1  41006  cdlemc2  41007  cdlemc4  41009  cdlemc5  41010  cdlemc6  41011  cdlemd1  41013  cdlemd2  41014  cdlemd3  41015  cdlemd4  41016  cdlemd7  41019  cdleme0aa  41025  cdleme0b  41027  cdleme0c  41028  cdleme0cp  41029  cdleme0cq  41030  cdleme0e  41032  cdleme0fN  41033  cdleme1b  41041  cdleme1  41042  cdleme2  41043  cdleme3b  41044  cdleme3c  41045  cdleme3e  41047  cdleme3g  41049  cdleme3h  41050  cdleme3  41052  cdleme5  41055  cdleme7d  41061  cdleme7e  41062  cdleme7ga  41063  cdleme7  41064  cdleme8  41065  cdleme9  41068  cdleme10  41069  cdleme11c  41076  cdleme11e  41078  cdleme11fN  41079  cdleme11g  41080  cdleme11k  41083  cdleme11  41085  cdleme15b  41090  cdleme15  41093  cdleme16b  41094  cdleme17b  41102  cdleme17c  41103  cdlemednpq  41114  cdleme20zN  41116  cdleme19a  41118  cdleme20bN  41125  cdleme20d  41127  cdleme20j  41133  cdleme21c  41142  cdleme22aa  41154  cdleme22b  41156  cdleme22cN  41157  cdleme22d  41158  cdleme22e  41159  cdleme22eALTN  41160  cdleme23b  41165  cdleme23c  41166  cdleme27N  41184  cdleme28a  41185  cdleme30a  41193  cdlemefrs29pre00  41210  cdlemefrs29bpre0  41211  cdlemefrs29cpre1  41213  cdlemefrs32fva  41215  cdlemefrs32fva1  41216  cdlemefr32snb  41220  cdlemefs32snb  41230  cdleme32snb  41251  cdleme32fva  41252  cdleme32fva1  41253  cdleme32fvaw  41254  cdleme35a  41263  cdleme35fnpq  41264  cdleme35b  41265  cdleme35c  41266  cdleme35f  41269  cdleme42c  41287  cdleme42e  41294  cdleme42h  41297  cdleme42i  41298  cdleme42ke  41300  cdleme42keg  41301  cdleme42mgN  41303  cdleme17d4  41312  cdleme48fvg  41315  cdleme48bw  41317  cdlemeg46req  41344  cdleme50trn3  41368  cdlemf1  41376  cdlemf2  41377  trlord  41384  ltrniotacnvval  41397  cdlemg2fv2  41415  cdlemg2l  41418  cdlemg7fvbwN  41422  cdlemg4c  41427  cdlemg4  41432  cdlemg6c  41435  cdlemg8b  41443  cdlemg11b  41457  cdlemg13a  41466  cdlemg17a  41476  cdlemg17h  41483  cdlemg17  41492  cdlemg18b  41494  cdlemg19a  41498  cdlemg27a  41507  cdlemg27b  41511  cdlemg31a  41512  cdlemg31b  41513  cdlemg31d  41515  cdlemg33b0  41516  cdlemg33a  41521  cdlemg35  41528  trlcolem  41541  cdlemg42  41544  cdlemg44a  41546  cdlemg46  41550  cdlemh1  41630  cdlemh2  41631  cdlemh  41632  cdlemi1  41633  cdlemi  41635  cdlemk3  41648  cdlemk4  41649  cdlemkvcl  41657  cdlemk7  41663  cdlemk11  41664  cdlemk15  41670  cdlemk1u  41674  cdlemk7u  41685  cdlemk11u  41686  cdlemk37  41729  cdlemk39  41731  cdlemkid1  41737  cdlemkid2  41739  cdlemk48  41765  cdlemk50  41767  cdlemk51  41768  cdlemk52  41769  dia2dimlem1  41879  dia2dimlem2  41880  dia2dimlem3  41881  dia2dimlem5  41883  dia2dimlem7  41885  dia2dimlem9  41887  dia2dimlem10  41888  dia2dimlem12  41890  dia2dimlem13  41891  cdlemm10N  41933  cdlemn2  42010  cdlemn3  42012  cdlemn9  42020  cdlemn10  42021  dihjustlem  42031  dihord1  42033  dihord2pre2  42041  dihvalcqat  42054  dib2dim  42058  dih2dimb  42059  dih2dimbALTN  42060  dihord5apre  42077  dihglbcpreN  42115  dihmeetlem3N  42120  dihmeetlem6  42124  dihjatc1  42126  dihjatc2N  42127  dihjatc3  42128  dihmeetlem9N  42130  dihmeetlem10N  42131  dihmeetlem11N  42132  dihmeetlem13N  42134  dihmeetlem15N  42136  dihmeetlem16N  42137  dihmeetlem17N  42138  dihatexv2  42154  dihjatb  42231  dihjatc  42232  dihjatcclem1  42233  dihjatcclem2  42234  dihjatcclem4  42236  dihjat  42238  dihjat3  42247  dihjat5N  42252  dvh4dimat  42253