| 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. Lemma 1.3 of [Schloeder] p. 1. (Contributed by NM, 26-Oct-2003.) |
| Ref | Expression |
|---|---|
| onelon | ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eloni 6394 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
| 2 | ordelon 6408 | . 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | |
| 3 | 1, 2 | sylan 580 | 1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 Ord word 6383 Oncon0 6384 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-tr 5260 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-ord 6387 df-on 6388 |
| This theorem is referenced by: oneli 6498 ssorduni 7799 unon 7851 tfindsg2 7883 dfom2 7889 trom 7896 onfununi 8381 onnseq 8384 dfrecs3 8412 dfrecs3OLD 8413 tz7.48-2 8482 tz7.49 8485 oalim 8570 omlim 8571 oelim 8572 oaordi 8584 oalimcl 8598 oaass 8599 omordi 8604 omlimcl 8616 odi 8617 omass 8618 omeulem1 8620 omeulem2 8621 omopth2 8622 oewordri 8630 oeordsuc 8632 oelimcl 8638 oeeui 8640 oaabs2 8687 omabs 8689 naddssim 8723 naddel12 8738 naddsuc2 8739 omxpenlem 9113 hartogs 9584 card2on 9594 cantnfle 9711 cantnflt 9712 cantnfp1lem3 9720 cantnfp1 9721 oemapvali 9724 cantnflem1b 9726 cantnflem1c 9727 cantnflem1d 9728 cantnflem1 9729 cantnflem2 9730 cantnflem3 9731 cantnflem4 9732 cantnf 9733 cnfcomlem 9739 cnfcom3lem 9743 cnfcom3 9744 r1ordg 9818 r1val3 9878 tskwe 9990 iscard 10015 cardmin2 10039 infxpenlem 10053 infxpenc2lem2 10060 alephordi 10114 alephord2i 10117 alephle 10128 cardaleph 10129 cfub 10289 cfsmolem 10310 zorn2lem5 10540 zorn2lem6 10541 ttukeylem6 10554 ttukeylem7 10555 ondomon 10603 cardmin 10604 alephval2 10612 alephreg 10622 smobeth 10626 winainflem 10733 inar1 10815 inatsk 10818 sltval2 27701 sltres 27707 nosepeq 27730 nosupno 27748 nosupres 27752 nosupbnd1lem1 27753 nosupbnd2lem1 27760 nosupbnd2 27761 noinfno 27763 noinfres 27767 noinfbnd1lem1 27768 noinfbnd2lem1 27775 noinfbnd2 27776 oldlim 27925 oldbday 27939 dfrdg2 35796 dfrdg4 35952 ontopbas 36429 onpsstopbas 36431 onint1 36450 onelord 43263 cantnfresb 43337 oawordex2 43339 oacl2g 43343 omabs2 43345 omcl2 43346 tfsconcatfv2 43353 tfsconcatfv 43354 tfsconcatrn 43355 tfsconcat0i 43358 ofoafg 43367 ofoaass 43373 oaun3lem1 43387 oaun3lem2 43388 oadif1lem 43392 oadif1 43393 nadd2rabtr 43397 nadd1suc 43405 naddgeoa 43407 naddwordnexlem0 43409 naddwordnexlem1 43410 naddwordnexlem3 43412 oawordex3 43413 naddwordnexlem4 43414 omssrncard 43553 |
| Copyright terms: Public domain | W3C validator |