![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > r1fnon | Structured version Visualization version Unicode version |
Description: The cumulative hierarchy of sets function is a function on the class of ordinal numbers. (Contributed by NM, 5-Oct-2003.) (Revised by Mario Carneiro, 10-Sep-2013.) |
Ref | Expression |
---|---|
r1fnon |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rdgfnon 7161 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | df-r1 8260 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | fneq1i 5691 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | mpbir 214 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-8 1899 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-rep 4528 ax-sep 4538 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6609 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-reu 2755 df-rab 2757 df-v 3058 df-sbc 3279 df-csb 3375 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-pss 3431 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-tp 3984 df-op 3986 df-uni 4212 df-iun 4293 df-br 4416 df-opab 4475 df-mpt 4476 df-tr 4511 df-eprel 4763 df-id 4767 df-po 4773 df-so 4774 df-fr 4811 df-we 4813 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-pred 5398 df-ord 5444 df-on 5445 df-suc 5447 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-f1 5605 df-fo 5606 df-f1o 5607 df-fv 5608 df-wrecs 7053 df-recs 7115 df-rdg 7153 df-r1 8260 |
This theorem is referenced by: r1suc 8266 r1lim 8268 r111 8271 r1ord 8276 r1ord3 8278 r1elss 8302 jech9.3 8310 onwf 8326 ssrankr1 8331 r1val3 8334 r1pw 8341 rankuni 8359 rankr1b 8360 r1om 8699 hsmexlem6 8886 smobeth 9036 wunr1om 9169 r1limwun 9186 r1wunlim 9187 tskr1om 9217 tskr1om2 9218 inar1 9225 rankcf 9227 inatsk 9228 r1tskina 9232 grur1 9270 grothomex 9279 aomclem4 35959 |
Copyright terms: Public domain | W3C validator |