Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > limsuc | Structured version Visualization version GIF version |
Description: The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003.) |
Ref | Expression |
---|---|
limsuc | ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dflim4 7562 | . . 3 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) | |
2 | suceq 6255 | . . . . . 6 ⊢ (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵) | |
3 | 2 | eleq1d 2897 | . . . . 5 ⊢ (𝑥 = 𝐵 → (suc 𝑥 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) |
4 | 3 | rspccv 3619 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴)) |
5 | 4 | 3ad2ant3 1131 | . . 3 ⊢ ((Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴)) |
6 | 1, 5 | sylbi 219 | . 2 ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴)) |
7 | limord 6249 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
8 | ordtr 6204 | . . 3 ⊢ (Ord 𝐴 → Tr 𝐴) | |
9 | trsuc 6274 | . . . 4 ⊢ ((Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴) | |
10 | 9 | ex 415 | . . 3 ⊢ (Tr 𝐴 → (suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴)) |
11 | 7, 8, 10 | 3syl 18 | . 2 ⊢ (Lim 𝐴 → (suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴)) |
12 | 6, 11 | impbid 214 | 1 ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ w3a 1083 = wceq 1533 ∈ wcel 2110 ∀wral 3138 ∅c0 4290 Tr wtr 5171 Ord word 6189 Lim wlim 6191 suc csuc 6192 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 ax-sep 5202 ax-nul 5209 ax-pr 5329 ax-un 7460 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3496 df-sbc 3772 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-pss 3953 df-nul 4291 df-if 4467 df-pw 4540 df-sn 4567 df-pr 4569 df-tp 4571 df-op 4573 df-uni 4838 df-br 5066 df-opab 5128 df-tr 5172 df-eprel 5464 df-po 5473 df-so 5474 df-fr 5513 df-we 5515 df-ord 6193 df-on 6194 df-lim 6195 df-suc 6196 |
This theorem is referenced by: limsssuc 7564 limuni3 7566 peano2b 7595 rdgsucg 8058 rdgsucmptnf 8064 oesuclem 8149 oaordi 8171 omordi 8191 oeordi 8212 oelim2 8220 limenpsi 8691 r1tr 9204 r1ordg 9206 r1pwss 9212 r1val1 9214 rankdmr1 9229 rankr1bg 9231 pwwf 9235 rankr1c 9249 rankonidlem 9256 ranklim 9272 r1pwcl 9275 rankxplim3 9309 infxpenlem 9438 alephordi 9499 cflm 9671 cfslb2n 9689 alephreg 10003 r1limwun 10157 rankcf 10198 inatsk 10199 |
Copyright terms: Public domain | W3C validator |