![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > onsuc | Structured version Visualization version GIF version |
Description: The successor of an ordinal number is an ordinal number. Closed form of onsuci 7814. Forward implication of onsucb 7792. Proposition 7.24 of [TakeutiZaring] p. 41. Remark 1.5 of [Schloeder] p. 1. (Contributed by NM, 6-Jun-1994.) (Proof shortened by BTernaryTau, 30-Nov-2024.) |
Ref | Expression |
---|---|
onsuc | ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sucexg 7780 | . 2 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ V) | |
2 | sucexeloni 7784 | . 2 ⊢ ((𝐴 ∈ On ∧ suc 𝐴 ∈ V) → suc 𝐴 ∈ On) | |
3 | 1, 2 | mpdan 686 | 1 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 Vcvv 3475 Oncon0 6356 suc csuc 6358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5295 ax-nul 5302 ax-pr 5423 ax-un 7712 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-pss 3965 df-nul 4321 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4905 df-br 5145 df-opab 5207 df-tr 5262 df-eprel 5576 df-po 5584 df-so 5585 df-fr 5627 df-we 5629 df-ord 6359 df-on 6360 df-suc 6362 |
This theorem is referenced by: ordsucOLD 7789 unon 7806 onsuci 7814 ordunisuc2 7820 ordzsl 7821 onzsl 7822 tfindsg 7837 dfom2 7844 findsg 7877 tfrlem12 8376 oasuc 8511 omsuc 8513 onasuc 8515 oacl 8522 oneo 8569 omeulem1 8570 omeulem2 8571 oeordi 8575 oeworde 8581 oelim2 8583 oelimcl 8588 oeeulem 8589 oeeui 8590 oaabs2 8636 omxpenlem 9061 card2inf 9537 cantnflt 9654 cantnflem1d 9670 cnfcom 9682 r1ordg 9760 bndrank 9823 r1pw 9827 r1pwALT 9828 tcrank 9866 onssnum 10022 dfac12lem2 10126 cfsuc 10239 cfsmolem 10252 fin1a2lem1 10382 fin1a2lem2 10383 ttukeylem7 10497 alephreg 10564 gch2 10657 winainflem 10675 winalim2 10678 r1wunlim 10719 nqereu 10911 noextend 27136 noresle 27167 nosupno 27173 madeoldsuc 27346 ontgval 35221 ontgsucval 35222 onsuctop 35223 sucneqond 36151 onexgt 41860 onexomgt 41861 onexoegt 41864 onepsuc 41872 onsucelab 41884 ordnexbtwnsuc 41888 onsucrn 41892 cantnftermord 41941 cantnfub2 41943 omabs2 41953 onsucunipr 41993 onsucunitp 41994 nadd1suc 42013 naddsuc2 42014 naddwordnexlem0 42018 naddwordnexlem1 42019 minregex 42156 onsetreclem2 47591 |
Copyright terms: Public domain | W3C validator |