Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > suceloni | Structured version Visualization version GIF version |
Description: The successor of an ordinal number is an ordinal number. Proposition 7.24 of [TakeutiZaring] p. 41. (Contributed by NM, 6-Jun-1994.) |
Ref | Expression |
---|---|
suceloni | ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | onelss 6226 | . . . . . . . 8 ⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) | |
2 | velsn 4573 | . . . . . . . . . 10 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
3 | eqimss 4020 | . . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → 𝑥 ⊆ 𝐴) | |
4 | 2, 3 | sylbi 218 | . . . . . . . . 9 ⊢ (𝑥 ∈ {𝐴} → 𝑥 ⊆ 𝐴) |
5 | 4 | a1i 11 | . . . . . . . 8 ⊢ (𝐴 ∈ On → (𝑥 ∈ {𝐴} → 𝑥 ⊆ 𝐴)) |
6 | 1, 5 | orim12d 958 | . . . . . . 7 ⊢ (𝐴 ∈ On → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴}) → (𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐴))) |
7 | df-suc 6190 | . . . . . . . . 9 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
8 | 7 | eleq2i 2901 | . . . . . . . 8 ⊢ (𝑥 ∈ suc 𝐴 ↔ 𝑥 ∈ (𝐴 ∪ {𝐴})) |
9 | elun 4122 | . . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∪ {𝐴}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴})) | |
10 | 8, 9 | bitr2i 277 | . . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴}) ↔ 𝑥 ∈ suc 𝐴) |
11 | oridm 898 | . . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐴) ↔ 𝑥 ⊆ 𝐴) | |
12 | 6, 10, 11 | 3imtr3g 296 | . . . . . 6 ⊢ (𝐴 ∈ On → (𝑥 ∈ suc 𝐴 → 𝑥 ⊆ 𝐴)) |
13 | sssucid 6261 | . . . . . 6 ⊢ 𝐴 ⊆ suc 𝐴 | |
14 | sstr2 3971 | . . . . . 6 ⊢ (𝑥 ⊆ 𝐴 → (𝐴 ⊆ suc 𝐴 → 𝑥 ⊆ suc 𝐴)) | |
15 | 12, 13, 14 | syl6mpi 67 | . . . . 5 ⊢ (𝐴 ∈ On → (𝑥 ∈ suc 𝐴 → 𝑥 ⊆ suc 𝐴)) |
16 | 15 | ralrimiv 3178 | . . . 4 ⊢ (𝐴 ∈ On → ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴) |
17 | dftr3 5167 | . . . 4 ⊢ (Tr suc 𝐴 ↔ ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴) | |
18 | 16, 17 | sylibr 235 | . . 3 ⊢ (𝐴 ∈ On → Tr suc 𝐴) |
19 | onss 7494 | . . . . 5 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On) | |
20 | snssi 4733 | . . . . 5 ⊢ (𝐴 ∈ On → {𝐴} ⊆ On) | |
21 | 19, 20 | unssd 4159 | . . . 4 ⊢ (𝐴 ∈ On → (𝐴 ∪ {𝐴}) ⊆ On) |
22 | 7, 21 | eqsstrid 4012 | . . 3 ⊢ (𝐴 ∈ On → suc 𝐴 ⊆ On) |
23 | ordon 7487 | . . . 4 ⊢ Ord On | |
24 | trssord 6201 | . . . . 5 ⊢ ((Tr suc 𝐴 ∧ suc 𝐴 ⊆ On ∧ Ord On) → Ord suc 𝐴) | |
25 | 24 | 3exp 1111 | . . . 4 ⊢ (Tr suc 𝐴 → (suc 𝐴 ⊆ On → (Ord On → Ord suc 𝐴))) |
26 | 23, 25 | mpii 46 | . . 3 ⊢ (Tr suc 𝐴 → (suc 𝐴 ⊆ On → Ord suc 𝐴)) |
27 | 18, 22, 26 | sylc 65 | . 2 ⊢ (𝐴 ∈ On → Ord suc 𝐴) |
28 | sucexg 7514 | . . 3 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ V) | |
29 | elong 6192 | . . 3 ⊢ (suc 𝐴 ∈ V → (suc 𝐴 ∈ On ↔ Ord suc 𝐴)) | |
30 | 28, 29 | syl 17 | . 2 ⊢ (𝐴 ∈ On → (suc 𝐴 ∈ On ↔ Ord suc 𝐴)) |
31 | 27, 30 | mpbird 258 | 1 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∨ wo 841 = wceq 1528 ∈ wcel 2105 ∀wral 3135 Vcvv 3492 ∪ cun 3931 ⊆ wss 3933 {csn 4557 Tr wtr 5163 Ord word 6183 Oncon0 6184 suc csuc 6186 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 ax-un 7450 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3or 1080 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-mo 2615 df-eu 2647 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ne 3014 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-sbc 3770 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-pss 3951 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4831 df-br 5058 df-opab 5120 df-tr 5164 df-eprel 5458 df-po 5467 df-so 5468 df-fr 5507 df-we 5509 df-ord 6187 df-on 6188 df-suc 6190 |
This theorem is referenced by: ordsuc 7518 unon 7535 onsuci 7542 ordunisuc2 7548 ordzsl 7549 onzsl 7550 tfindsg 7564 dfom2 7571 findsg 7598 tfrlem12 8014 oasuc 8138 omsuc 8140 onasuc 8142 oacl 8149 oneo 8196 omeulem1 8197 omeulem2 8198 oeordi 8202 oeworde 8208 oelim2 8210 oelimcl 8215 oeeulem 8216 oeeui 8217 oaabs2 8261 omxpenlem 8606 card2inf 9007 cantnflt 9123 cantnflem1d 9139 cnfcom 9151 r1ordg 9195 bndrank 9258 r1pw 9262 r1pwALT 9263 tcrank 9301 onssnum 9454 dfac12lem2 9558 cfsuc 9667 cfsmolem 9680 fin1a2lem1 9810 fin1a2lem2 9811 ttukeylem7 9925 alephreg 9992 gch2 10085 winainflem 10103 winalim2 10106 r1wunlim 10147 nqereu 10339 noextend 33070 noresle 33097 nosupno 33100 ontgval 33676 ontgsucval 33677 onsuctop 33678 sucneqond 34528 onsetreclem2 44736 |
Copyright terms: Public domain | W3C validator |