Theorem nodmon 27684

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 27680	. 2 ⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
2		fdm 6690	. . . . 5 ⊢ (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 = 𝑥)
3	2	eleq1d 2841	. . . 4 ⊢ (𝐴:𝑥⟶{1o, 2o} → (dom 𝐴 ∈ On ↔ 𝑥 ∈ On))
4	3	biimprcd 252	. . 3 ⊢ (𝑥 ∈ On → (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On))
5	4	rexlimiv 3150	. 2 ⊢ (∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On)
6	1, 5	sylbi 219	1 ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2136  ∃wrex 3080  {cpr 4578  dom cdm 5640  Oncon0 6335  ⟶wf 6506  1_oc1o 8418  2_oc2o 8419   No csur 27674

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-sep 5240  ax-pow 5316  ax-pr 5384  ax-un 7707

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ral 3071  df-rex 3081  df-rab 3409  df-v 3450  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-fun 6512  df-fn 6513  df-f 6514  df-no 27677

This theorem is referenced by:  nodmord  27687  elno2  27688  noseponlem  27698  noextend  27700  noextendseq  27701  noextenddif  27702  noextendlt  27703  noextendgt  27704  bdayfo  27711  nosepssdm  27720  nolt02olem  27728  nosupno  27737  nosupres  27741  nosupbnd1lem1  27742  nosupbnd1lem2  27743  nosupbnd1lem3  27744  nosupbnd1lem4  27745  nosupbnd1lem5  27746  nosupbnd1lem6  27747  nosupbnd1  27748  nosupbnd2lem1  27749  nosupbnd2  27750  noinfno  27752  noinfres  27756  noinfbnd1lem1  27757  noinfbnd1lem2  27758  noinfbnd1lem3  27759  noinfbnd1lem4  27760  noinfbnd1lem5  27761  noinfbnd1lem6  27762  noinfbnd1  27763  noinfbnd2lem1  27764  noinfbnd2  27765  nosupinfsep  27766  noetasuplem3  27769  noetasuplem4  27770  noetainflem3  27773  noetainflem4  27774  bdaybndex  43955