Theorem nodmon 28037

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∃wrex 3090  {cpr 4590  dom cdm 5655  Oncon0 6380  ⟶wf 6554  1_oc1o 8497  2_oc2o 8498  Nocsur 28027

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pow 5331  ax-pr 5395  ax-un 7775

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-fun 6560  df-fn 6561  df-f 6562  df-no 28030

This theorem is used by:  nodmord  28040  elno2  28041  noseponlem  28051  noextend  28053  noextendseq  28054  noextenddif  28055  noextendlt  28056  noextendgt  28057  bdayfo  28064  nosepssdm  28073  nolt02olem  28081  nosupno  28090  nosupres  28094  nosupbnd1lem1  28095  nosupbnd1lem2  28096  nosupbnd1lem3  28097  nosupbnd1lem4  28098  nosupbnd1lem5  28099  nosupbnd1lem6  28100  nosupbnd1  28101  nosupbnd2lem1  28102  nosupbnd2  28103  noinfno  28105  noinfres  28109  noinfbnd1lem1  28110  noinfbnd1lem2  28111  noinfbnd1lem3  28112  noinfbnd1lem4  28113  noinfbnd1lem5  28114  noinfbnd1lem6  28115  noinfbnd1  28116  noinfbnd2lem1  28117  noinfbnd2  28118  nosupinfsep  28119  noetasuplem3  28122  noetasuplem4  28123  noetainflem3  28126  noetainflem4  28127  bdaybndex  44624