Metamath Proof Explorer

Table of Contents - 21.47. Mathbox for Eric Schmidt

1. Miscellany
   1. rspesbcd
   2. rext0
   3. cocanss2
   4. cocan2g
   5. cocanss1
   6. cocan1g
   7. dmstructnn
   8. dmstructfi
   9. rnstructfi
2. Study of dfbi1ALT
   1. dfbi1ALTa
   2. simprimi
   3. dfbi1ALTb
3. Relation-preserving functions
   1. wrelp
   2. df-relp
   3. relpeq1
   4. relpeq2
   5. relpeq3
   6. relpeq4
   7. relpeq5
   8. nfrelp
   9. relpf
   10. relprel
   11. relpmin
   12. relpfrlem
   13. relpfr
4. Orbits
   1. orbitex
   2. orbitinit
   3. orbitcl
   4. orbitclmpt
5. Well-founded sets
   1. trwf
   2. rankrelp
   3. wffr
   4. trfr
   5. tcfr
   6. xpwf
   7. dmwf
   8. rnwf
   9. relwf
6. Absoluteness in transitive models
   1. ralabso
   2. rexabso
   3. ralabsod
   4. rexabsod
   5. ralabsobidv
   6. rexabsobidv
   7. ssabso
   8. disjabso
   9. n0abso
7. Lemmas for showing axioms hold in models
   1. traxext
   2. modelaxreplem1
   3. modelaxreplem2
   4. modelaxreplem3
   5. modelaxrep
   6. ssclaxsep
   7. 0elaxnul
   8. pwclaxpow
   9. prclaxpr
   10. uniclaxun
   11. sswfaxreg
   12. omssaxinf2
   13. omelaxinf2
   14. dfac5prim
   15. ac8prim
   16. modelac8prim
8. The class of well-founded sets is a model for ZFC
   1. wfaxext
   2. wfaxrep
   3. wfaxsep
   4. wfaxnul
   5. wfaxpow
   6. wfaxpr
   7. wfaxun
   8. wfaxreg
   9. wfaxinf2
   10. wfac8prim
9. Permutation models
   1. brpermmodel
   2. brpermmodelcnv
   3. permaxext
   4. permaxrep
   5. permaxsep
   6. permaxnul
   7. permaxpow
   8. permaxpr
   9. permaxun
   10. permaxinf2lem
   11. permaxinf2
   12. permac8prim
   13. nregmodelf1o
   14. nregmodellem
   15. nregmodel
   16. nregmodelaxext
10. Isomorphism of finite ordinals and non-negative integers
    1. hashnna
    2. hashnnsuc
    3. hashnnm
    4. hashnnlt
    5. hashnnltb
    6. hashomf1o
    7. hashomiso
11. Hereditarily finite sets
    1. hfpr
    2. hfxp
    3. hfdm
    4. hfrn
    5. hfrel
    6. omhf
    7. omsshf
12. Hereditarily finite structures
    1. chfstruct
    2. df-hfstruct
    3. hfstructstruct
    4. hfstructfun
    5. rnhfstructsshf
    6. ishfstruct
    7. rnhfstructhf
    8. hfstructhf
    9. hfstructcan