ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pinn Structured version   GIF version

Theorem pinn 6155
Description: A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.)
Assertion
Ref Expression
pinn (A NA 𝜔)

Proof of Theorem pinn
StepHypRef Expression
1 df-ni 6150 . . 3 N = (𝜔 ∖ {∅})
2 difss 3038 . . 3 (𝜔 ∖ {∅}) ⊆ 𝜔
31, 2eqsstri 2943 . 2 N ⊆ 𝜔
43sseli 2909 1 (A NA 𝜔)
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1366  cdif 2882  c0 3192  {csn 3339  𝜔com 4228  Ncnpi 6118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995
This theorem depends on definitions:  df-bi 110  df-tru 1226  df-nf 1323  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-v 2528  df-dif 2888  df-in 2892  df-ss 2899  df-ni 6150
This theorem is referenced by:  pion  6156  piord  6157  elni2  6160  mulidpi  6164  ltsopi  6166  pitric  6167  pitri3or  6168  ltdcpi  6169  addclpi  6173  mulclpi  6174  addcompig  6175  addasspig  6176  mulcompig  6177  mulasspig  6178  distrpig  6179  addcanpig  6180  mulcanpig  6181  addnidpig  6182  ltexpi  6183  ltapig  6184  ltmpig  6185  nnppipi  6188  enqdc  6206  archnqq  6260  prarloclemarch2  6262  enq0enq  6272  enq0sym  6273  enq0ref  6274  enq0tr  6275  nqnq0pi  6279  nqnq0  6282  addcmpblnq0  6284  mulcmpblnq0  6285  mulcanenq0ec  6286  addclnq0  6292  nqpnq0nq  6294  nqnq0a  6295  nqnq0m  6296  nq0m0r  6297  nq0a0  6298  nnanq0  6299  distrnq0  6300  mulcomnq0  6301  addassnq0lemcl  6302  addassnq0  6303  nq02m  6305  prarloclemlt  6333  prarloclemn  6339
  Copyright terms: Public domain W3C validator