![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > onelon | Structured version Visualization version GIF version |
Description: An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.) |
Ref | Expression |
---|---|
onelon | ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eloni 6033 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | ordelon 6047 | . 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | |
3 | 1, 2 | sylan 572 | 1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∈ wcel 2048 Ord word 6022 Oncon0 6023 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pr 5180 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-br 4924 df-opab 4986 df-tr 5025 df-eprel 5310 df-po 5319 df-so 5320 df-fr 5359 df-we 5361 df-ord 6026 df-on 6027 |
This theorem is referenced by: oneli 6130 ssorduni 7310 unon 7356 tfindsg2 7386 dfom2 7392 ordom 7399 onfununi 7775 onnseq 7778 dfrecs3 7806 tz7.48-2 7874 tz7.49 7877 oalim 7951 omlim 7952 oelim 7953 oaordi 7965 oalimcl 7979 oaass 7980 omordi 7985 omlimcl 7997 odi 7998 omass 7999 omeulem1 8001 omeulem2 8002 omopth2 8003 oewordri 8011 oeordsuc 8013 oelimcl 8019 oeeui 8021 oaabs2 8064 omabs 8066 omxpenlem 8406 hartogs 8795 card2on 8805 cantnfle 8920 cantnflt 8921 cantnfp1lem3 8929 cantnfp1 8930 oemapvali 8933 cantnflem1b 8935 cantnflem1c 8936 cantnflem1d 8937 cantnflem1 8938 cantnflem2 8939 cantnflem3 8940 cantnflem4 8941 cantnf 8942 cnfcomlem 8948 cnfcom3lem 8952 cnfcom3 8953 r1ordg 8993 r1val3 9053 tskwe 9165 iscard 9190 cardmin2 9213 infxpenlem 9225 infxpenc2lem2 9232 alephordi 9286 alephord2i 9289 alephle 9300 cardaleph 9301 cfub 9461 cfsmolem 9482 zorn2lem5 9712 zorn2lem6 9713 ttukeylem6 9726 ttukeylem7 9727 ondomon 9775 cardmin 9776 alephval2 9784 alephreg 9794 smobeth 9798 winainflem 9905 inar1 9987 inatsk 9990 dfrdg2 32501 sltval2 32624 sltres 32630 nosepeq 32650 nosupno 32664 nosupres 32668 nosupbnd1lem1 32669 nosupbnd2lem1 32676 nosupbnd2 32677 dfrdg4 32873 ontopbas 33236 onpsstopbas 33238 onint1 33257 |
Copyright terms: Public domain | W3C validator |