Theorem 1onn 4311

Description: One is a natural number.

Assertion

Ref	Expression
1onn	|- 1o e. om

Proof of Theorem 1onn

Step	Hyp	Ref	Expression
1		df-1o 4191	. 2 |- 1o = suc (/)
2		peano1 3206	. . 3 |- (/) e. om
3		peano2 3207	. . 3 |- ((/) e. om -> suc (/) e. om)
4	2, 3	ax-mp 7	. 2 |- suc (/) e. om
5	1, 4	eqeltri 1591	1 |- 1o e. om

Syntax hints:   e. wcel 999  (/)c0 2331  suc csuc 3007  omcom 3188  1oc1o 4186

This theorem is referenced by:  2onn 4312  nneob 4313  snfi 4493  pwfi 4631  oancom 4695  card1 4896  unxpdomlem 4908  unxpdom2 4910  1pi 5076  1lt2pi 5097  indpi 5099  infxpidmlem1 7644  infxpidmlem12 7655  infpss 7666  infmap2 7673  setwoe 10640  top2usne 10643

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-1o 4191

Copyright terms: Public domain