![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > atn0 | Structured version Visualization version GIF version |
Description: An atom is not zero. (atne0 31173 analog.) (Contributed by NM, 5-Nov-2012.) |
Ref | Expression |
---|---|
atne0.z | ⊢ 0 = (0.‘𝐾) |
atne0.a | ⊢ 𝐴 = (Atoms‘𝐾) |
Ref | Expression |
---|---|
atn0 | ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → 𝑃 ≠ 0 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2736 | . . . 4 ⊢ (Base‘𝐾) = (Base‘𝐾) | |
2 | eqid 2736 | . . . 4 ⊢ (le‘𝐾) = (le‘𝐾) | |
3 | atne0.z | . . . 4 ⊢ 0 = (0.‘𝐾) | |
4 | atne0.a | . . . 4 ⊢ 𝐴 = (Atoms‘𝐾) | |
5 | 1, 2, 3, 4 | isat3 37736 | . . 3 ⊢ (𝐾 ∈ AtLat → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ (Base‘𝐾) ∧ 𝑃 ≠ 0 ∧ ∀𝑥 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑃 → (𝑥 = 𝑃 ∨ 𝑥 = 0 ))))) |
6 | simp2 1137 | . . 3 ⊢ ((𝑃 ∈ (Base‘𝐾) ∧ 𝑃 ≠ 0 ∧ ∀𝑥 ∈ (Base‘𝐾)(𝑥(le‘𝐾)𝑃 → (𝑥 = 𝑃 ∨ 𝑥 = 0 ))) → 𝑃 ≠ 0 ) | |
7 | 5, 6 | syl6bi 252 | . 2 ⊢ (𝐾 ∈ AtLat → (𝑃 ∈ 𝐴 → 𝑃 ≠ 0 )) |
8 | 7 | imp 407 | 1 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → 𝑃 ≠ 0 ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2941 ∀wral 3062 class class class wbr 5103 ‘cfv 6493 Basecbs 17075 lecple 17132 0.cp0 18304 Atomscatm 37692 AtLatcal 37693 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5240 ax-sep 5254 ax-nul 5261 ax-pow 5318 ax-pr 5382 ax-un 7668 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3352 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-iun 4954 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6445 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7309 df-plt 18211 df-glb 18228 df-p0 18306 df-covers 37695 df-ats 37696 df-atl 37727 |
This theorem is referenced by: atncvrN 37744 atnle 37746 atlatmstc 37748 intnatN 37837 atcvrneN 37860 atcvrj2b 37862 2llnm3N 37999 pmapjat1 38283 lhpocnle 38446 lhpmatb 38461 lhp2atnle 38463 trlatn0 38602 ltrnnidn 38604 trlnidatb 38607 cdlemg33c 39138 cdlemg33e 39140 dihatexv 39768 |
Copyright terms: Public domain | W3C validator |