![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ordelon | Structured version Visualization version GIF version |
Description: An element of an ordinal class is an ordinal number. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.) |
Ref | Expression |
---|---|
ordelon | ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordelord 6337 | . 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) | |
2 | elong 6323 | . . 3 ⊢ (𝐵 ∈ 𝐴 → (𝐵 ∈ On ↔ Ord 𝐵)) | |
3 | 2 | adantl 482 | . 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ∈ On ↔ Ord 𝐵)) |
4 | 1, 3 | mpbird 256 | 1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∈ wcel 2106 Ord word 6314 Oncon0 6315 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5254 ax-nul 5261 ax-pr 5382 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ne 2942 df-ral 3063 df-rab 3406 df-v 3445 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-br 5104 df-opab 5166 df-tr 5221 df-eprel 5535 df-po 5543 df-so 5544 df-fr 5586 df-we 5588 df-ord 6318 df-on 6319 |
This theorem is referenced by: onelon 6340 ordunidif 6364 ordpwsuc 7746 ordsucun 7756 ordunel 7758 ordunisuc2 7776 oesuclem 8467 odi 8522 oelim2 8538 oeoalem 8539 oeoelem 8541 limenpsi 9092 ordtypelem9 9458 oismo 9472 cantnflt 9604 cantnfp1lem3 9612 cantnflem1b 9618 cantnflem1 9621 rankr1bg 9735 rankr1clem 9752 rankr1c 9753 rankonidlem 9760 infxpenlem 9945 coflim 10193 fin23lem26 10257 fpwwe2lem7 10569 onsuct0 34880 ordnexbtwnsuc 41540 orddif0suc 41541 omord2lim 41572 iunord 47053 |
Copyright terms: Public domain | W3C validator |