Theorem nodmord 28010

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 28007	. 2 ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)
2		eloni 6372	. 2 ⊢ (dom 𝐴 ∈ On → Ord dom 𝐴)
3	1, 2	syl 18	1 ⊢ (𝐴 ∈ No → Ord dom 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  dom cdm 5651  Ord word 6361  Oncon0 6362  Nocsur 27997

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-tr 5213  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-ord 6365  df-on 6366  df-fun 6540  df-fn 6541  df-f 6542  df-no 28000

This theorem is used by:  noseponlem  28021  nosepon  28022  noextend  28023  noextenddif  28025  noextendlt  28026  noextendgt  28027  nolesgn2ores  28029  nogesgn1ores  28031  fvnobday  28035  nosepssdm  28043  nosupres  28064  nosupbnd1lem1  28065  nosupbnd1lem3  28067  nosupbnd1lem5  28069  nosupbnd2lem1  28072  nosupbnd2  28073  noinfres  28079  noinfbnd1lem1  28080  noinfbnd1lem3  28082  noinfbnd1lem5  28084  noinfbnd2lem1  28087  noinfbnd2  28088  noetasuplem4  28093  noetainflem4  28097  noetalem1  28098