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. (Contributed by NM, 26-Oct-2003.) |
Ref | Expression |
---|---|
ordelon | ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordelord 6207 | . 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) | |
2 | elong 6193 | . . 3 ⊢ (𝐵 ∈ 𝐴 → (𝐵 ∈ On ↔ Ord 𝐵)) | |
3 | 2 | adantl 482 | . 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ∈ On ↔ Ord 𝐵)) |
4 | 1, 3 | mpbird 258 | 1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∈ wcel 2105 Ord word 6184 Oncon0 6185 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2793 ax-sep 5195 ax-nul 5202 ax-pr 5321 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 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 3497 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4466 df-sn 4560 df-pr 4562 df-op 4566 df-uni 4833 df-br 5059 df-opab 5121 df-tr 5165 df-eprel 5459 df-po 5468 df-so 5469 df-fr 5508 df-we 5510 df-ord 6188 df-on 6189 |
This theorem is referenced by: onelon 6210 ordunidif 6233 ordpwsuc 7518 ordsucun 7528 ordunel 7530 ordunisuc2 7547 oesuclem 8141 odi 8195 oelim2 8211 oeoalem 8212 oeoelem 8214 limenpsi 8681 ordtypelem9 8979 oismo 8993 cantnflt 9124 cantnfp1lem3 9132 cantnflem1b 9138 cantnflem1 9141 rankr1bg 9221 rankr1clem 9238 rankr1c 9239 rankonidlem 9246 infxpenlem 9428 coflim 9672 fin23lem26 9736 fpwwe2lem8 10048 onsuct0 33687 iunord 44677 |
Copyright terms: Public domain | W3C validator |