![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > onsssuc | Structured version Visualization version GIF version |
Description: A subset of an ordinal number belongs to its successor. (Contributed by NM, 15-Sep-1995.) |
Ref | Expression |
---|---|
onsssuc | ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eloni 6381 | . 2 ⊢ (𝐵 ∈ On → Ord 𝐵) | |
2 | ordsssuc 6460 | . 2 ⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | |
3 | 1, 2 | sylan2 591 | 1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∈ wcel 2098 ⊆ wss 3944 Ord word 6370 Oncon0 6371 suc csuc 6373 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ne 2930 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-pss 3964 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-tr 5267 df-eprel 5582 df-po 5590 df-so 5591 df-fr 5633 df-we 5635 df-ord 6374 df-on 6375 df-suc 6377 |
This theorem is referenced by: ordsssuc2 6462 onmindif 6463 tfindsg 7866 dfom2 7873 findsg 7905 ondif2 8523 oeeui 8623 cantnflem1 9714 rankr1bg 9828 rankr1c 9846 cofsmo 10294 cfsmolem 10295 cfcof 10299 fin1a2lem9 10433 alephreg 10607 winainflem 10718 n0sbday 28269 onsuct0 36056 onint1 36064 onintunirab 42797 cantnfresb 42895 oaun3lem4 42948 |
Copyright terms: Public domain | W3C validator |