![]() |
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 5927 | . . . . . . . 8 ⊢ (𝐴 ∈ On → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) | |
2 | velsn 4337 | . . . . . . . . . 10 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴) | |
3 | eqimss 3798 | . . . . . . . . . 10 ⊢ (𝑥 = 𝐴 → 𝑥 ⊆ 𝐴) | |
4 | 2, 3 | sylbi 207 | . . . . . . . . 9 ⊢ (𝑥 ∈ {𝐴} → 𝑥 ⊆ 𝐴) |
5 | 4 | a1i 11 | . . . . . . . 8 ⊢ (𝐴 ∈ On → (𝑥 ∈ {𝐴} → 𝑥 ⊆ 𝐴)) |
6 | 1, 5 | orim12d 919 | . . . . . . 7 ⊢ (𝐴 ∈ On → ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴}) → (𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐴))) |
7 | df-suc 5890 | . . . . . . . . 9 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴}) | |
8 | 7 | eleq2i 2831 | . . . . . . . 8 ⊢ (𝑥 ∈ suc 𝐴 ↔ 𝑥 ∈ (𝐴 ∪ {𝐴})) |
9 | elun 3896 | . . . . . . . 8 ⊢ (𝑥 ∈ (𝐴 ∪ {𝐴}) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴})) | |
10 | 8, 9 | bitr2i 265 | . . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ {𝐴}) ↔ 𝑥 ∈ suc 𝐴) |
11 | oridm 537 | . . . . . . 7 ⊢ ((𝑥 ⊆ 𝐴 ∨ 𝑥 ⊆ 𝐴) ↔ 𝑥 ⊆ 𝐴) | |
12 | 6, 10, 11 | 3imtr3g 284 | . . . . . 6 ⊢ (𝐴 ∈ On → (𝑥 ∈ suc 𝐴 → 𝑥 ⊆ 𝐴)) |
13 | sssucid 5963 | . . . . . 6 ⊢ 𝐴 ⊆ suc 𝐴 | |
14 | sstr2 3751 | . . . . . 6 ⊢ (𝑥 ⊆ 𝐴 → (𝐴 ⊆ suc 𝐴 → 𝑥 ⊆ suc 𝐴)) | |
15 | 12, 13, 14 | syl6mpi 67 | . . . . 5 ⊢ (𝐴 ∈ On → (𝑥 ∈ suc 𝐴 → 𝑥 ⊆ suc 𝐴)) |
16 | 15 | ralrimiv 3103 | . . . 4 ⊢ (𝐴 ∈ On → ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴) |
17 | dftr3 4908 | . . . 4 ⊢ (Tr suc 𝐴 ↔ ∀𝑥 ∈ suc 𝐴𝑥 ⊆ suc 𝐴) | |
18 | 16, 17 | sylibr 224 | . . 3 ⊢ (𝐴 ∈ On → Tr suc 𝐴) |
19 | onss 7155 | . . . . 5 ⊢ (𝐴 ∈ On → 𝐴 ⊆ On) | |
20 | snssi 4484 | . . . . 5 ⊢ (𝐴 ∈ On → {𝐴} ⊆ On) | |
21 | 19, 20 | unssd 3932 | . . . 4 ⊢ (𝐴 ∈ On → (𝐴 ∪ {𝐴}) ⊆ On) |
22 | 7, 21 | syl5eqss 3790 | . . 3 ⊢ (𝐴 ∈ On → suc 𝐴 ⊆ On) |
23 | ordon 7147 | . . . 4 ⊢ Ord On | |
24 | trssord 5901 | . . . . 5 ⊢ ((Tr suc 𝐴 ∧ suc 𝐴 ⊆ On ∧ Ord On) → Ord suc 𝐴) | |
25 | 24 | 3exp 1113 | . . . 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 7175 | . . 3 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ V) | |
29 | elong 5892 | . . 3 ⊢ (suc 𝐴 ∈ V → (suc 𝐴 ∈ On ↔ Ord suc 𝐴)) | |
30 | 28, 29 | syl 17 | . 2 ⊢ (𝐴 ∈ On → (suc 𝐴 ∈ On ↔ Ord suc 𝐴)) |
31 | 27, 30 | mpbird 247 | 1 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∨ wo 382 = wceq 1632 ∈ wcel 2139 ∀wral 3050 Vcvv 3340 ∪ cun 3713 ⊆ wss 3715 {csn 4321 Tr wtr 4904 Ord word 5883 Oncon0 5884 suc csuc 5886 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pr 5055 ax-un 7114 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ne 2933 df-ral 3055 df-rex 3056 df-rab 3059 df-v 3342 df-sbc 3577 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-pss 3731 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-tp 4326 df-op 4328 df-uni 4589 df-br 4805 df-opab 4865 df-tr 4905 df-eprel 5179 df-po 5187 df-so 5188 df-fr 5225 df-we 5227 df-ord 5887 df-on 5888 df-suc 5890 |
This theorem is referenced by: ordsuc 7179 unon 7196 onsuci 7203 ordunisuc2 7209 ordzsl 7210 onzsl 7211 tfindsg 7225 dfom2 7232 findsg 7258 tfrlem12 7654 oasuc 7773 omsuc 7775 onasuc 7777 oacl 7784 oneo 7830 omeulem1 7831 omeulem2 7832 oeordi 7836 oeworde 7842 oelim2 7844 oelimcl 7849 oeeulem 7850 oeeui 7851 oaabs2 7894 omxpenlem 8226 card2inf 8625 cantnflt 8742 cantnflem1d 8758 cnfcom 8770 r1ordg 8814 bndrank 8877 r1pw 8881 r1pwALT 8882 tcrank 8920 onssnum 9053 dfac12lem2 9158 cfsuc 9271 cfsmolem 9284 fin1a2lem1 9414 fin1a2lem2 9415 ttukeylem7 9529 alephreg 9596 gch2 9689 winainflem 9707 winalim2 9710 r1wunlim 9751 nqereu 9943 noextend 32125 noresle 32152 nosupno 32155 ontgval 32736 ontgsucval 32737 onsuctop 32738 sucneqond 33524 onsetreclem2 42962 |
Copyright terms: Public domain | W3C validator |