Theorem nodmon 28008

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

Assertion

Ref	Expression
nodmon	⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)

Proof of Theorem nodmon

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elno 28004	. 2 ⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
2		fdm 6719	. . . . 5 ⊢ (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 = 𝑥)
3	2	eleq1d 2845	. . . 4 ⊢ (𝐴:𝑥⟶{1o, 2o} → (dom 𝐴 ∈ On ↔ 𝑥 ∈ On))
4	3	biimprcd 253	. . 3 ⊢ (𝑥 ∈ On → (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On))
5	4	rexlimiv 3156	. 2 ⊢ (∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On)
6	1, 5	sylbi 220	1 ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∃wrex 3086  {cpr 4585  dom cdm 5650  Oncon0 6362  ⟶wf 6534  1_oc1o 8470  2_oc2o 8471  Nocsur 27998

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pow 5326  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6540  df-fn 6541  df-f 6542  df-no 28001

This theorem is used by:  nodmord  28011  elno2  28012  noseponlem  28022  noextend  28024  noextendseq  28025  noextenddif  28026  noextendlt  28027  noextendgt  28028  bdayfo  28035  nosepssdm  28044  nolt02olem  28052  nosupno  28061  nosupres  28065  nosupbnd1lem1  28066  nosupbnd1lem2  28067  nosupbnd1lem3  28068  nosupbnd1lem4  28069  nosupbnd1lem5  28070  nosupbnd1lem6  28071  nosupbnd1  28072  nosupbnd2lem1  28073  nosupbnd2  28074  noinfno  28076  noinfres  28080  noinfbnd1lem1  28081  noinfbnd1lem2  28082  noinfbnd1lem3  28083  noinfbnd1lem4  28084  noinfbnd1lem5  28085  noinfbnd1lem6  28086  noinfbnd1  28087  noinfbnd2lem1  28088  noinfbnd2  28089  nosupinfsep  28090  noetasuplem3  28093  noetasuplem4  28094  noetainflem3  28097  noetainflem4  28098  bdaybndex  44508