Theorem nodmon 27829

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 27825	. 2 ⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
2		fdm 6719	. . . . 5 ⊢ (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 = 𝑥)
3	2	eleq1d 2851	. . . 4 ⊢ (𝐴:𝑥⟶{1o, 2o} → (dom 𝐴 ∈ On ↔ 𝑥 ∈ On))
4	3	biimprcd 253	. . 3 ⊢ (𝑥 ∈ On → (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On))
5	4	rexlimiv 3162	. 2 ⊢ (∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On)
6	1, 5	sylbi 220	1 ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3092  {cpr 4594  dom cdm 5664  Oncon0 6364  ⟶wf 6536  1_oc1o 8448  2_oc2o 8449   No csur 27819

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5260  ax-pow 5339  ax-pr 5407  ax-un 7738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-br 5113  df-opab 5177  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-fun 6542  df-fn 6543  df-f 6544  df-no 27822

This theorem is used by:  nodmord  27832  elno2  27833  noseponlem  27843  noextend  27845  noextendseq  27846  noextenddif  27847  noextendlt  27848  noextendgt  27849  bdayfo  27856  nosepssdm  27865  nolt02olem  27873  nosupno  27882  nosupres  27886  nosupbnd1lem1  27887  nosupbnd1lem2  27888  nosupbnd1lem3  27889  nosupbnd1lem4  27890  nosupbnd1lem5  27891  nosupbnd1lem6  27892  nosupbnd1  27893  nosupbnd2lem1  27894  nosupbnd2  27895  noinfno  27897  noinfres  27901  noinfbnd1lem1  27902  noinfbnd1lem2  27903  noinfbnd1lem3  27904  noinfbnd1lem4  27905  noinfbnd1lem5  27906  noinfbnd1lem6  27907  noinfbnd1  27908  noinfbnd2lem1  27909  noinfbnd2  27910  nosupinfsep  27911  noetasuplem3  27914  noetasuplem4  27915  noetainflem3  27918  noetainflem4  27919  bdaybndex  44189