![]() |
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 6036 | . 2 ⊢ (𝐵 ∈ On → Ord 𝐵) | |
2 | ordsssuc 6112 | . 2 ⊢ ((𝐴 ∈ On ∧ Ord 𝐵) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) | |
3 | 1, 2 | sylan2 584 | 1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∈ wcel 2051 ⊆ wss 3822 Ord word 6025 Oncon0 6026 suc csuc 6028 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2743 ax-sep 5056 ax-nul 5063 ax-pr 5182 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2752 df-cleq 2764 df-clel 2839 df-nfc 2911 df-ne 2961 df-ral 3086 df-rex 3087 df-rab 3090 df-v 3410 df-sbc 3675 df-dif 3825 df-un 3827 df-in 3829 df-ss 3836 df-pss 3838 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-tr 5027 df-eprel 5313 df-po 5322 df-so 5323 df-fr 5362 df-we 5364 df-ord 6029 df-on 6030 df-suc 6032 |
This theorem is referenced by: ordsssuc2 6114 onmindif 6115 tfindsg 7389 dfom2 7396 findsg 7422 ondif2 7927 oeeui 8027 cantnflem1 8944 rankr1bg 9024 rankr1c 9042 cofsmo 9487 cfsmolem 9488 cfcof 9492 fin1a2lem9 9626 alephreg 9800 winainflem 9911 onsuct0 33346 onint1 33354 |
Copyright terms: Public domain | W3C validator |