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 7695 | . . 3 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴)) | |
2 | suceq 6331 | . . . . . 6 ⊢ (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵) | |
3 | 2 | eleq1d 2823 | . . . . 5 ⊢ (𝑥 = 𝐵 → (suc 𝑥 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) |
4 | 3 | rspccv 3558 | . . . 4 ⊢ (∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴)) |
5 | 4 | 3ad2ant3 1134 | . . 3 ⊢ ((Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 suc 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴)) |
6 | 1, 5 | sylbi 216 | . 2 ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 → suc 𝐵 ∈ 𝐴)) |
7 | limord 6325 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
8 | ordtr 6280 | . . 3 ⊢ (Ord 𝐴 → Tr 𝐴) | |
9 | trsuc 6350 | . . . 4 ⊢ ((Tr 𝐴 ∧ suc 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴) | |
10 | 9 | ex 413 | . . 3 ⊢ (Tr 𝐴 → (suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴)) |
11 | 7, 8, 10 | 3syl 18 | . 2 ⊢ (Lim 𝐴 → (suc 𝐵 ∈ 𝐴 → 𝐵 ∈ 𝐴)) |
12 | 6, 11 | impbid 211 | 1 ⊢ (Lim 𝐴 → (𝐵 ∈ 𝐴 ↔ suc 𝐵 ∈ 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ∀wral 3064 ∅c0 4256 Tr wtr 5191 Ord word 6265 Lim wlim 6267 suc csuc 6268 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-pss 3906 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-tr 5192 df-eprel 5495 df-po 5503 df-so 5504 df-fr 5544 df-we 5546 df-ord 6269 df-on 6270 df-lim 6271 df-suc 6272 |
This theorem is referenced by: limsssuc 7697 limuni3 7699 peano2b 7729 rdgsucg 8254 rdgsucmptnf 8260 oesuclem 8355 oaordi 8377 omordi 8397 oeordi 8418 oelim2 8426 limenpsi 8939 r1tr 9534 r1ordg 9536 r1pwss 9542 r1val1 9544 rankdmr1 9559 rankr1bg 9561 pwwf 9565 rankr1c 9579 rankonidlem 9586 ranklim 9602 r1pwcl 9605 rankxplim3 9639 infxpenlem 9769 alephordi 9830 cflm 10006 cfslb2n 10024 alephreg 10338 r1limwun 10492 rankcf 10533 inatsk 10534 oldlim 34069 |
Copyright terms: Public domain | W3C validator |