![]() |
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 5986 | . 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) | |
2 | elong 5972 | . . 3 ⊢ (𝐵 ∈ 𝐴 → (𝐵 ∈ On ↔ Ord 𝐵)) | |
3 | 2 | adantl 475 | . 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ∈ On ↔ Ord 𝐵)) |
4 | 1, 3 | mpbird 249 | 1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 ∈ wcel 2166 Ord word 5963 Oncon0 5964 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2391 ax-ext 2804 ax-sep 5006 ax-nul 5014 ax-pr 5128 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2606 df-eu 2641 df-clab 2813 df-cleq 2819 df-clel 2822 df-nfc 2959 df-ne 3001 df-ral 3123 df-rex 3124 df-rab 3127 df-v 3417 df-dif 3802 df-un 3804 df-in 3806 df-ss 3813 df-nul 4146 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4660 df-br 4875 df-opab 4937 df-tr 4977 df-eprel 5256 df-po 5264 df-so 5265 df-fr 5302 df-we 5304 df-ord 5967 df-on 5968 |
This theorem is referenced by: onelon 5989 ordunidif 6012 ordpwsuc 7277 ordsucun 7287 ordunel 7289 ordunisuc2 7306 oesuclem 7873 odi 7927 oelim2 7943 oeoalem 7944 oeoelem 7946 limenpsi 8405 ordtypelem9 8701 oismo 8715 cantnflt 8847 cantnfp1lem3 8855 cantnflem1b 8861 cantnflem1 8864 rankr1bg 8944 rankr1clem 8961 rankr1c 8962 rankonidlem 8969 infxpenlem 9150 coflim 9399 fin23lem26 9463 fpwwe2lem8 9775 onsuct0 32974 iunord 43318 |
Copyright terms: Public domain | W3C validator |