Theorem o1p1e2 4306

Description: 1 + 1 = 2 for ordinal numbers.

Assertion

Ref	Expression
o1p1e2	|- (1o +o 1o) = 2o

Proof of Theorem o1p1e2

Step	Hyp	Ref	Expression
1		1on 4269	. . 3 |- 1o e. On
2		oa1suc 4295	. . 3 |- (1o e. On -> (1o +o 1o) = suc 1o)
3	1, 2	ax-mp 7	. 2 |- (1o +o 1o) = suc 1o
4		df-2o 4265	. 2 |- 2o = suc 1o
5	3, 4	eqtr4i 1539	1 |- (1o +o 1o) = 2o

Syntax hints:   = wceq 989   e. wcel 991  Oncon0 2972  suc csuc 2974  (class class class)co 4016  1oc1o 4259  2oc2o 4260   +o coa 4261

This theorem is referenced by:  nneob 4390

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 995  ax-gen 996  ax-8 997  ax-9 998  ax-10 999  ax-11 1000  ax-12 1001  ax-13 1002  ax-14 1003  ax-17 1004  ax-4 1006  ax-5o 1008  ax-6o 1011  ax-9o 1156  ax-10o 1174  ax-16 1244  ax-11o 1252  ax-ext 1498  ax-rep 2763  ax-sep 2773  ax-nul 2780  ax-pow 2813  ax-pr 2851  ax-un 3086

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3or 779  df-3an 780  df-ex 1014  df-sb 1206  df-eu 1419  df-mo 1420  df-clab 1504  df-cleq 1509  df-clel 1512  df-ne 1628  df-ral 1693  df-rex 1694  df-rab 1696  df-v 1856  df-sbc 1985  df-csb 2050  df-dif 2099  df-un 2100  df-in 2101  df-ss 2103  df-nul 2331  df-if 2414  df-pw 2454  df-sn 2465  df-pr 2466  df-tp 2468  df-op 2469  df-uni 2565  df-iun 2630  df-br 2688  df-opab 2736  df-tr 2750  df-eprel 2906  df-id 2909  df-po 2914  df-so 2926  df-fr 2944  df-we 2959  df-ord 2975  df-on 2976  df-lim 2977  df-suc 2978  df-xp 3262  df-rel 3263  df-cnv 3264  df-co 3265  df-dm 3266  df-rn 3267  df-res 3268  df-ima 3269  df-fun 3270  df-fn 3271  df-fv 3276  df-opr 4018  df-oprab 4019  df-rdg 4228  df-1o 4264  df-2o 4265  df-oadd 4266

Copyright terms: Public domain