Theorem 1pi 7688

Description: Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)

Assertion

Ref	Expression
1pi	|- 1o e. N.

Proof of Theorem 1pi

Step	Hyp	Ref	Expression
1		1onn 6797	. 2 |- 1o e. om
2		1n0 6709	. 2 |- 1o =/= (/)
3		elni 7681	. 2 |- ( 1o e. N. <-> ( 1o e. om /\ 1o =/= (/) ) )
4	1, 2, 3	mpbir2an 955	1 |- 1o e. N.

This proof depends on syntax axioms:   e. wcel 2209   =/= wne 2420   (/)c0 3520   omcom 4739   1oc1o 6684   N.cnpi 7645

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-nul 4261  ax-pow 4313  ax-pr 4348  ax-un 4580

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-v 2823  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-pw 3690  df-sn 3715  df-pr 3716  df-uni 3936  df-int 3971  df-suc 4518  df-iom 4740  df-1o 6691  df-ni 7677

This theorem is used by:  mulidpi  7691  1lt2pi  7713  nlt1pig  7714  indpi  7715  1nq  7739  1qec  7761  mulidnq  7762  1lt2nq  7779  archnqq  7790  prarloclemarch  7791  prarloclemarch2  7792  nnnq  7795  ltnnnq  7796  nq0m0r  7829  nq0a0  7830  addpinq1  7837  nq02m  7838  prarloclemlt  7866  prarloclemlo  7867  prarloclemn  7872  prarloclemcalc  7875  nqprm  7915  caucvgprlemm  8041  caucvgprprlemml  8067  caucvgprprlemmu  8068  caucvgsrlemasr  8163  caucvgsr  8175  nntopi  8267