![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 2on | Structured version Visualization version Unicode version |
Description: Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) |
Ref | Expression |
---|---|
2on |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-2o 7188 |
. 2
![]() ![]() ![]() ![]() ![]() | |
2 | 1on 7194 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | onsuci 6670 |
. 2
![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | eqeltri 2527 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-8 1891 ax-9 1898 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 ax-sep 4528 ax-nul 4537 ax-pr 4642 ax-un 6588 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 987 df-3an 988 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-eu 2305 df-mo 2306 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-ne 2626 df-ral 2744 df-rex 2745 df-rab 2748 df-v 3049 df-sbc 3270 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-pss 3422 df-nul 3734 df-if 3884 df-pw 3955 df-sn 3971 df-pr 3973 df-tp 3975 df-op 3977 df-uni 4202 df-br 4406 df-opab 4465 df-tr 4501 df-eprel 4748 df-po 4758 df-so 4759 df-fr 4796 df-we 4798 df-ord 5429 df-on 5430 df-suc 5432 df-1o 7187 df-2o 7188 |
This theorem is referenced by: 3on 7197 oneo 7287 infxpenc 8454 infxpenc2 8458 mappwen 8548 pwcdaen 8620 sdom2en01 8737 fin1a2lem4 8838 xpslem 15491 xpsadd 15494 xpsmul 15495 xpsvsca 15497 xpsle 15499 xpsmnd 16588 xpsgrp 16817 efgval 17379 efgtf 17384 frgpcpbl 17421 frgp0 17422 frgpeccl 17423 frgpadd 17425 frgpmhm 17427 vrgpf 17430 vrgpinv 17431 frgpupf 17435 frgpup1 17437 frgpup2 17438 frgpup3lem 17439 frgpnabllem1 17521 frgpnabllem2 17522 xpstopnlem1 20836 xpstps 20837 xpstopnlem2 20838 xpsxmetlem 21406 xpsdsval 21408 nofv 30556 sltres 30563 noxp2o 30566 nobndup 30601 ssoninhaus 31120 onint1 31121 1oequni2o 31783 finxpreclem4 31798 pw2f1ocnv 35904 frlmpwfi 35968 |
Copyright terms: Public domain | W3C validator |