Theorem nodmon 27790

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∃wrex 3087  {cpr 4590  dom cdm 5661  Oncon0 6360  ⟶wf 6532  1_oc1o 8445  2_oc2o 8446   No csur 27780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5256  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  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 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-fun 6538  df-fn 6539  df-f 6540  df-no 27783

This theorem is referenced by:  nodmord  27793  elno2  27794  noseponlem  27804  noextend  27806  noextendseq  27807  noextenddif  27808  noextendlt  27809  noextendgt  27810  bdayfo  27817  nosepssdm  27826  nolt02olem  27834  nosupno  27843  nosupres  27847  nosupbnd1lem1  27848  nosupbnd1lem2  27849  nosupbnd1lem3  27850  nosupbnd1lem4  27851  nosupbnd1lem5  27852  nosupbnd1lem6  27853  nosupbnd1  27854  nosupbnd2lem1  27855  nosupbnd2  27856  noinfno  27858  noinfres  27862  noinfbnd1lem1  27863  noinfbnd1lem2  27864  noinfbnd1lem3  27865  noinfbnd1lem4  27866  noinfbnd1lem5  27867  noinfbnd1lem6  27868  noinfbnd1  27869  noinfbnd2lem1  27870  noinfbnd2  27871  nosupinfsep  27872  noetasuplem3  27875  noetasuplem4  27876  noetainflem3  27879  noetainflem4  27880  bdaybndex  44127