![]() |
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 6386 | . 2 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
2 | ordelon 6400 | . 2 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | |
3 | 1, 2 | sylan 578 | 1 ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∈ wcel 2099 Ord word 6375 Oncon0 6376 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ne 2931 df-ral 3052 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-opab 5216 df-tr 5271 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-we 5639 df-ord 6379 df-on 6380 |
This theorem is referenced by: oneli 6490 ssorduni 7787 unon 7840 tfindsg2 7872 dfom2 7878 trom 7885 onfununi 8371 onnseq 8374 dfrecs3 8402 dfrecs3OLD 8403 tz7.48-2 8472 tz7.49 8475 oalim 8562 omlim 8563 oelim 8564 oaordi 8576 oalimcl 8590 oaass 8591 omordi 8596 omlimcl 8608 odi 8609 omass 8610 omeulem1 8612 omeulem2 8613 omopth2 8614 oewordri 8622 oeordsuc 8624 oelimcl 8630 oeeui 8632 oaabs2 8679 omabs 8681 naddssim 8715 naddel12 8730 omxpenlem 9111 hartogs 9587 card2on 9597 cantnfle 9714 cantnflt 9715 cantnfp1lem3 9723 cantnfp1 9724 oemapvali 9727 cantnflem1b 9729 cantnflem1c 9730 cantnflem1d 9731 cantnflem1 9732 cantnflem2 9733 cantnflem3 9734 cantnflem4 9735 cantnf 9736 cnfcomlem 9742 cnfcom3lem 9746 cnfcom3 9747 r1ordg 9821 r1val3 9881 tskwe 9993 iscard 10018 cardmin2 10042 infxpenlem 10056 infxpenc2lem2 10063 alephordi 10117 alephord2i 10120 alephle 10131 cardaleph 10132 cfub 10292 cfsmolem 10313 zorn2lem5 10543 zorn2lem6 10544 ttukeylem6 10557 ttukeylem7 10558 ondomon 10606 cardmin 10607 alephval2 10615 alephreg 10625 smobeth 10629 winainflem 10736 inar1 10818 inatsk 10821 sltval2 27686 sltres 27692 nosepeq 27715 nosupno 27733 nosupres 27737 nosupbnd1lem1 27738 nosupbnd2lem1 27745 nosupbnd2 27746 noinfno 27748 noinfres 27752 noinfbnd1lem1 27753 noinfbnd2lem1 27760 noinfbnd2 27761 oldlim 27910 oldbday 27924 dfrdg2 35619 dfrdg4 35775 ontopbas 36140 onpsstopbas 36142 onint1 36161 onelord 42916 cantnfresb 42990 oawordex2 42992 oacl2g 42996 omabs2 42998 omcl2 42999 tfsconcatfv2 43006 tfsconcatfv 43007 tfsconcatrn 43008 tfsconcat0i 43011 ofoafg 43020 ofoaass 43026 oaun3lem1 43040 oaun3lem2 43041 oadif1lem 43045 oadif1 43046 nadd2rabtr 43050 nadd1suc 43058 naddsuc2 43059 naddgeoa 43061 naddwordnexlem0 43063 naddwordnexlem1 43064 naddwordnexlem3 43066 oawordex3 43067 naddwordnexlem4 43068 omssrncard 43207 |
Copyright terms: Public domain | W3C validator |