Theorem nodmon 27639

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 27634	. 2 ⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
2		fdm 6671	. . . . 5 ⊢ (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 = 𝑥)
3	2	eleq1d 2825	. . . 4 ⊢ (𝐴:𝑥⟶{1o, 2o} → (dom 𝐴 ∈ On ↔ 𝑥 ∈ On))
4	3	biimprcd 251	. . 3 ⊢ (𝑥 ∈ On → (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On))
5	4	rexlimiv 3134	. 2 ⊢ (∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On)
6	1, 5	sylbi 218	1 ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3064  {cpr 4564  dom cdm 5625  Oncon0 6317  ⟶wf 6488  1_oc1o 8395  2_oc2o 8396   No csur 27628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6494  df-fn 6495  df-f 6496  df-no 27631

This theorem is referenced by:  nodmord  27642  elno2  27643  noseponlem  27653  noextend  27655  noextendseq  27656  noextenddif  27657  noextendlt  27658  noextendgt  27659  bdayfo  27666  nosepssdm  27675  nolt02olem  27683  nosupno  27692  nosupres  27696  nosupbnd1lem1  27697  nosupbnd1lem2  27698  nosupbnd1lem3  27699  nosupbnd1lem4  27700  nosupbnd1lem5  27701  nosupbnd1lem6  27702  nosupbnd1  27703  nosupbnd2lem1  27704  nosupbnd2  27705  noinfno  27707  noinfres  27711  noinfbnd1lem1  27712  noinfbnd1lem2  27713  noinfbnd1lem3  27714  noinfbnd1lem4  27715  noinfbnd1lem5  27716  noinfbnd1lem6  27717  noinfbnd1  27718  noinfbnd2lem1  27719  noinfbnd2  27720  nosupinfsep  27721  noetasuplem3  27724  noetasuplem4  27725  noetainflem3  27728  noetainflem4  27729  bdaybndex  43876