Theorem nodmord 27619

Description: The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.)

Assertion

Ref	Expression
nodmord	⊢ (𝐴 ∈ No → Ord dom 𝐴)

Proof of Theorem nodmord

Step	Hyp	Ref	Expression
1		nodmon 27616	. 2 ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)
2		eloni 6325	. 2 ⊢ (dom 𝐴 ∈ On → Ord dom 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐴 ∈ No → Ord dom 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2113  dom cdm 5622  Ord word 6314  Oncon0 6315   No csur 27605

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-tr 5204  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-ord 6318  df-on 6319  df-fun 6492  df-fn 6493  df-f 6494  df-no 27608

This theorem is referenced by:  noseponlem  27630  nosepon  27631  noextend  27632  noextenddif  27634  noextendlt  27635  noextendgt  27636  nolesgn2ores  27638  nogesgn1ores  27640  fvnobday  27644  nosepssdm  27652  nosupres  27673  nosupbnd1lem1  27674  nosupbnd1lem3  27676  nosupbnd1lem5  27678  nosupbnd2lem1  27681  nosupbnd2  27682  noinfres  27688  noinfbnd1lem1  27689  noinfbnd1lem3  27691  noinfbnd1lem5  27693  noinfbnd2lem1  27696  noinfbnd2  27697  noetasuplem4  27702  noetainflem4  27706  noetalem1  27707