Theorem nodmon 27825

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ∃wrex 3088  {cpr 4590  dom cdm 5660  Oncon0 6360  ⟶wf 6532  1_oc1o 8444  2_oc2o 8445   No csur 27815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5256  ax-pow 5335  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-fun 6538  df-fn 6539  df-f 6540  df-no 27818

This theorem is used by:  nodmord  27828  elno2  27829  noseponlem  27839  noextend  27841  noextendseq  27842  noextenddif  27843  noextendlt  27844  noextendgt  27845  bdayfo  27852  nosepssdm  27861  nolt02olem  27869  nosupno  27878  nosupres  27882  nosupbnd1lem1  27883  nosupbnd1lem2  27884  nosupbnd1lem3  27885  nosupbnd1lem4  27886  nosupbnd1lem5  27887  nosupbnd1lem6  27888  nosupbnd1  27889  nosupbnd2lem1  27890  nosupbnd2  27891  noinfno  27893  noinfres  27897  noinfbnd1lem1  27898  noinfbnd1lem2  27899  noinfbnd1lem3  27900  noinfbnd1lem4  27901  noinfbnd1lem5  27902  noinfbnd1lem6  27903  noinfbnd1  27904  noinfbnd2lem1  27905  noinfbnd2  27906  nosupinfsep  27907  noetasuplem3  27910  noetasuplem4  27911  noetainflem3  27914  noetainflem4  27915  bdaybndex  44185