Theorem nodmon 27568

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 27563	. 2 ⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
2		fdm 6699	. . . . 5 ⊢ (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 = 𝑥)
3	2	eleq1d 2814	. . . 4 ⊢ (𝐴:𝑥⟶{1o, 2o} → (dom 𝐴 ∈ On ↔ 𝑥 ∈ On))
4	3	biimprcd 250	. . 3 ⊢ (𝑥 ∈ On → (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On))
5	4	rexlimiv 3128	. 2 ⊢ (∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On)
6	1, 5	sylbi 217	1 ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3054  {cpr 4593  dom cdm 5640  Oncon0 6334  ⟶wf 6509  1_oc1o 8429  2_oc2o 8430   No csur 27557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5253  ax-nul 5263  ax-pow 5322  ax-pr 5389  ax-un 7713

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3919  df-un 3921  df-in 3923  df-ss 3933  df-nul 4299  df-if 4491  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5110  df-opab 5172  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-fun 6515  df-fn 6516  df-f 6517  df-no 27560

This theorem is referenced by:  nodmord  27571  elno2  27572  noseponlem  27582  noextend  27584  noextendseq  27585  noextenddif  27586  noextendlt  27587  noextendgt  27588  bdayfo  27595  nosepssdm  27604  nolt02olem  27612  nosupno  27621  nosupres  27625  nosupbnd1lem1  27626  nosupbnd1lem2  27627  nosupbnd1lem3  27628  nosupbnd1lem4  27629  nosupbnd1lem5  27630  nosupbnd1lem6  27631  nosupbnd1  27632  nosupbnd2lem1  27633  nosupbnd2  27634  noinfno  27636  noinfres  27640  noinfbnd1lem1  27641  noinfbnd1lem2  27642  noinfbnd1lem3  27643  noinfbnd1lem4  27644  noinfbnd1lem5  27645  noinfbnd1lem6  27646  noinfbnd1  27647  noinfbnd2lem1  27648  noinfbnd2  27649  nosupinfsep  27650  noetasuplem3  27653  noetasuplem4  27654  noetainflem3  27657  noetainflem4  27658  bdaybndex  43413