![]() |
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 6201 | . . . . . . . 8 ⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) | |
2 | velsn 4541 | . . . . . . . . . 10 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
3 | eqimss 3971 | . . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → 𝑥 ⊆ 𝐴) | |
4 | 2, 3 | sylbi 220 | . . . . . . . . 9 ⊢ (𝑥 ∈ {𝐴} → 𝑥 ⊆ 𝐴) |
5 | 4 | a1i 11 | . . . . . . . 8 ⊢ (𝐴 ∈ On → (𝑥 ∈ {𝐴} → 𝑥 ⊆ 𝐴)) |
6 | 1, 5 | orim12d 962 | . . . . . . 7 ⊢ (𝐴 ∈ On → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴}) → (𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐴))) |
7 | df-suc 6165 | . . . . . . . . 9 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
8 | 7 | eleq2i 2881 | . . . . . . . 8 ⊢ (𝑥 ∈ suc 𝐴 ↔ 𝑥 ∈ (𝐴 ∪ {𝐴})) |
9 | elun 4076 | . . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∪ {𝐴}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴})) | |
10 | 8, 9 | bitr2i 279 | . . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴}) ↔ 𝑥 ∈ suc 𝐴) |
11 | oridm 902 | . . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐴) ↔ 𝑥 ⊆ 𝐴) | |
12 | 6, 10, 11 | 3imtr3g 298 | . . . . . 6 ⊢ (𝐴 ∈ On → (𝑥 ∈ suc 𝐴 → 𝑥 ⊆ 𝐴)) |
13 | sssucid 6236 | . . . . . 6 ⊢ 𝐴 ⊆ suc 𝐴 | |
14 | sstr2 3922 | . . . . . 6 ⊢ (𝑥 ⊆ 𝐴 → (𝐴 ⊆ suc 𝐴 → 𝑥 ⊆ suc 𝐴)) | |
15 | 12, 13, 14 | syl6mpi 67 | . . . . 5 ⊢ (𝐴 ∈ On → (𝑥 ∈ suc 𝐴 → 𝑥 ⊆ suc 𝐴)) |
16 | 15 | ralrimiv 3148 | . . . 4 ⊢ (𝐴 ∈ On → ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴) |
17 | dftr3 5140 | . . . 4 ⊢ (Tr suc 𝐴 ↔ ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴) | |
18 | 16, 17 | sylibr 237 | . . 3 ⊢ (𝐴 ∈ On → Tr suc 𝐴) |
19 | onss 7485 | . . . . 5 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On) | |
20 | snssi 4701 | . . . . 5 ⊢ (𝐴 ∈ On → {𝐴} ⊆ On) | |
21 | 19, 20 | unssd 4113 | . . . 4 ⊢ (𝐴 ∈ On → (𝐴 ∪ {𝐴}) ⊆ On) |
22 | 7, 21 | eqsstrid 3963 | . . 3 ⊢ (𝐴 ∈ On → suc 𝐴 ⊆ On) |
23 | ordon 7478 | . . . 4 ⊢ Ord On | |
24 | trssord 6176 | . . . . 5 ⊢ ((Tr suc 𝐴 ∧ suc 𝐴 ⊆ On ∧ Ord On) → Ord suc 𝐴) | |
25 | 24 | 3exp 1116 | . . . 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 7505 | . . 3 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ V) | |
29 | elong 6167 | . . 3 ⊢ (suc 𝐴 ∈ V → (suc 𝐴 ∈ On ↔ Ord suc 𝐴)) | |
30 | 28, 29 | syl 17 | . 2 ⊢ (𝐴 ∈ On → (suc 𝐴 ∈ On ↔ Ord suc 𝐴)) |
31 | 27, 30 | mpbird 260 | 1 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∨ wo 844 = wceq 1538 ∈ wcel 2111 ∀wral 3106 Vcvv 3441 ∪ cun 3879 ⊆ wss 3881 {csn 4525 Tr wtr 5136 Ord word 6158 Oncon0 6159 suc csuc 6161 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 ax-un 7441 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ne 2988 df-ral 3111 df-rex 3112 df-rab 3115 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-pss 3900 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-tr 5137 df-eprel 5430 df-po 5438 df-so 5439 df-fr 5478 df-we 5480 df-ord 6162 df-on 6163 df-suc 6165 |
This theorem is referenced by: ordsuc 7509 unon 7526 onsuci 7533 ordunisuc2 7539 ordzsl 7540 onzsl 7541 tfindsg 7555 dfom2 7562 findsg 7590 tfrlem12 8008 oasuc 8132 omsuc 8134 onasuc 8136 oacl 8143 oneo 8190 omeulem1 8191 omeulem2 8192 oeordi 8196 oeworde 8202 oelim2 8204 oelimcl 8209 oeeulem 8210 oeeui 8211 oaabs2 8255 omxpenlem 8601 card2inf 9003 cantnflt 9119 cantnflem1d 9135 cnfcom 9147 r1ordg 9191 bndrank 9254 r1pw 9258 r1pwALT 9259 tcrank 9297 onssnum 9451 dfac12lem2 9555 cfsuc 9668 cfsmolem 9681 fin1a2lem1 9811 fin1a2lem2 9812 ttukeylem7 9926 alephreg 9993 gch2 10086 winainflem 10104 winalim2 10107 r1wunlim 10148 nqereu 10340 noextend 33286 noresle 33313 nosupno 33316 ontgval 33892 ontgsucval 33893 onsuctop 33894 sucneqond 34782 onsetreclem2 45235 |
Copyright terms: Public domain | W3C validator |