Theorem nodmord 27717

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

Syntax hints:   → wi 4   ∈ wcel 2142  dom cdm 5647  Ord word 6345  Oncon0 6346   No csur 27704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-tr 5208  df-po 5555  df-so 5556  df-fr 5600  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-ord 6349  df-on 6350  df-fun 6523  df-fn 6524  df-f 6525  df-no 27707

This theorem is referenced by:  noseponlem  27728  nosepon  27729  noextend  27730  noextenddif  27732  noextendlt  27733  noextendgt  27734  nolesgn2ores  27736  nogesgn1ores  27738  fvnobday  27742  nosepssdm  27750  nosupres  27771  nosupbnd1lem1  27772  nosupbnd1lem3  27774  nosupbnd1lem5  27776  nosupbnd2lem1  27779  nosupbnd2  27780  noinfres  27786  noinfbnd1lem1  27787  noinfbnd1lem3  27789  noinfbnd1lem5  27791  noinfbnd2lem1  27794  noinfbnd2  27795  noetasuplem4  27800  noetainflem4  27804  noetalem1  27805