![]() |
Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > nodmon | Structured version Visualization version GIF version |
Description: The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
Ref | Expression |
---|---|
nodmon | ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elno 32764 | . 2 ⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o}) | |
2 | fdm 6397 | . . . . 5 ⊢ (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 = 𝑥) | |
3 | 2 | eleq1d 2869 | . . . 4 ⊢ (𝐴:𝑥⟶{1o, 2o} → (dom 𝐴 ∈ On ↔ 𝑥 ∈ On)) |
4 | 3 | biimprcd 251 | . . 3 ⊢ (𝑥 ∈ On → (𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On)) |
5 | 4 | rexlimiv 3245 | . 2 ⊢ (∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o} → dom 𝐴 ∈ On) |
6 | 1, 5 | sylbi 218 | 1 ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2083 ∃wrex 3108 {cpr 4480 dom cdm 5450 Oncon0 6073 ⟶wf 6228 1oc1o 7953 2oc2o 7954 No csur 32758 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-rep 5088 ax-sep 5101 ax-nul 5108 ax-pr 5228 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-reu 3114 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-sn 4479 df-pr 4481 df-op 4485 df-uni 4752 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-id 5355 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-no 32761 |
This theorem is referenced by: nodmord 32771 elno2 32772 noseponlem 32782 noextend 32784 noextendseq 32785 noextenddif 32786 noextendlt 32787 noextendgt 32788 bdayfo 32793 nosepssdm 32801 nolt02olem 32809 nosupno 32814 nosupres 32818 nosupbnd1lem1 32819 nosupbnd1lem2 32820 nosupbnd1lem3 32821 nosupbnd1lem4 32822 nosupbnd1lem5 32823 nosupbnd1lem6 32824 nosupbnd1 32825 nosupbnd2lem1 32826 nosupbnd2 32827 noetalem2 32829 noetalem3 32830 |
Copyright terms: Public domain | W3C validator |