Theorem nodmon 27595

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3056  {cpr 4577  dom cdm 5619  Oncon0 6312  ⟶wf 6483  1_oc1o 8384  2_oc2o 8385   No csur 27584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-fun 6489  df-fn 6490  df-f 6491  df-no 27587

This theorem is referenced by:  nodmord  27598  elno2  27599  noseponlem  27609  noextend  27611  noextendseq  27612  noextenddif  27613  noextendlt  27614  noextendgt  27615  bdayfo  27622  nosepssdm  27631  nolt02olem  27639  nosupno  27648  nosupres  27652  nosupbnd1lem1  27653  nosupbnd1lem2  27654  nosupbnd1lem3  27655  nosupbnd1lem4  27656  nosupbnd1lem5  27657  nosupbnd1lem6  27658  nosupbnd1  27659  nosupbnd2lem1  27660  nosupbnd2  27661  noinfno  27663  noinfres  27667  noinfbnd1lem1  27668  noinfbnd1lem2  27669  noinfbnd1lem3  27670  noinfbnd1lem4  27671  noinfbnd1lem5  27672  noinfbnd1lem6  27673  noinfbnd1  27674  noinfbnd2lem1  27675  noinfbnd2  27676  nosupinfsep  27677  noetasuplem3  27680  noetasuplem4  27681  noetainflem3  27684  noetainflem4  27685  bdaybndex  43529