Metamath Proof Explorer

Table of Contents - 2.4. ZF Set Theory - add the Axiom of Union

1. Introduce the Axiom of Union
   1. ax-un
   2. zfun
   3. axun2
   4. uniex2
   5. vuniex
   6. uniexg
   7. uniex
   8. uniexd
   9. unex
   10. tpex
   11. unexb
   12. unexg
   13. xpexg
   14. xpexd
   15. 3xpexg
   16. xpex
   17. unexd
   18. sqxpexg
   19. abnexg
   20. abnex
   21. snnex
   22. pwnex
   23. difex2
   24. difsnexi
   25. uniuni
   26. uniexr
   27. uniexb
   28. pwexr
   29. pwexb
   30. elpwpwel
   31. eldifpw
   32. elpwun
   33. pwuncl
   34. iunpw
   35. fr3nr
   36. epne3
   37. dfwe2
2. Ordinals (continued)
   1. epweon
   2. epweonALT
   3. ordon
   4. onprc
   5. ssorduni
   6. ssonuni
   7. ssonunii
   8. ordeleqon
   9. ordsson
   10. dford5
   11. onss
   12. predon
   13. predonOLD
   14. ssonprc
   15. onuni
   16. orduni
   17. onint
   18. onint0
   19. onssmin
   20. onminesb
   21. onminsb
   22. oninton
   23. onintrab
   24. onintrab2
   25. onnmin
   26. onnminsb
   27. oneqmin
   28. uniordint
   29. onminex
   30. sucon
   31. sucexb
   32. sucexg
   33. sucex
   34. onmindif2
   35. ordsuci
   36. sucexeloni
   37. sucexeloniOLD
   38. onsuc
   39. suceloniOLD
   40. ordsuc
   41. ordsucOLD
   42. ordpwsuc
   43. onpwsuc
   44. onsucb
   45. ordsucss
   46. onpsssuc
   47. ordelsuc
   48. onsucmin
   49. ordsucelsuc
   50. ordsucsssuc
   51. ordsucuniel
   52. ordsucun
   53. ordunpr
   54. ordunel
   55. onsucuni
   56. ordsucuni
   57. orduniorsuc
   58. unon
   59. ordunisuc
   60. orduniss2
   61. onsucuni2
   62. 0elsuc
   63. limon
   64. onuniorsuc
   65. onssi
   66. onsuci
   67. onuniorsuciOLD
   68. onuninsuci
   69. onsucssi
   70. nlimsucg
   71. orduninsuc
   72. ordunisuc2
   73. ordzsl
   74. onzsl
   75. dflim3
   76. dflim4
   77. limsuc
   78. limsssuc
   79. nlimon
   80. limuni3
3. Transfinite induction
   1. tfi
   2. tfisg
   3. tfis
   4. tfis2f
   5. tfis2
   6. tfis3
   7. tfisi
   8. tfinds
   9. tfindsg
   10. tfindsg2
   11. tfindes
   12. tfinds2
   13. tfinds3
4. The natural numbers (i.e., finite ordinals)
   1. com
   2. df-om
   3. dfom2
   4. elom
   5. omsson
   6. limomss
   7. nnon
   8. nnoni
   9. nnord
   10. trom
   11. ordom
   12. elnn
   13. omon
   14. omelon2
   15. nnlim
   16. omssnlim
   17. limom
   18. peano2b
   19. nnsuc
   20. omsucne
   21. ssnlim
   22. omsinds
   23. omsindsOLD
   24. omun
5. Peano's postulates
   1. peano1
   2. peano1OLD
   3. peano2
   4. peano3
   5. peano4
   6. peano5
   7. peano5OLD
   8. nn0suc
6. Finite induction (for finite ordinals)
   1. find
   2. findOLD
   3. finds
   4. findsg
   5. finds2
   6. finds1
   7. findes
7. Relations and functions (cont.)
   1. dmexg
   2. rnexg
   3. dmexd
   4. fndmexd
   5. dmfex
   6. fndmexb
   7. fdmexb
   8. dmfexALT
   9. dmex
   10. rnex
   11. iprc
   12. resiexg
   13. imaexg
   14. imaex
   15. exse2
   16. xpexr
   17. xpexr2
   18. xpexcnv
   19. soex
   20. elxp4
   21. elxp5
   22. cnvexg
   23. cnvex
   24. relcnvexb
   25. f1oexrnex
   26. f1oexbi
   27. coexg
   28. coex
   29. funcnvuni
   30. fun11uni
   31. fex2
   32. fabexg
   33. fabex
   34. f1oabexg
   35. fiunlem
   36. fiun
   37. f1iun
   38. fviunfun
   39. ffoss
   40. f11o
   41. resfunexgALT
   42. cofunexg
   43. cofunex2g
   44. fnexALT
   45. funexw
   46. mptexw
   47. funrnex
   48. zfrep6
   49. focdmex
   50. f1dmex
   51. f1ovv
   52. fvclex
   53. fvresex
   54. abrexexg
   55. abrexexgOLD
   56. abrexex
   57. iunexg
   58. abrexex2g
   59. opabex3d
   60. opabex3rd
   61. opabex3
   62. iunex
   63. abrexex2
   64. abexssex
   65. abexex
   66. f1oweALT
   67. wemoiso
   68. wemoiso2
   69. oprabexd
   70. oprabex
   71. oprabex3
   72. oprabrexex2
   73. ab2rexex
   74. ab2rexex2
   75. xpexgALT
   76. offval3
   77. offres
   78. ofmres
   79. ofmresex
8. First and second members of an ordered pair
   1. c1st
   2. c2nd
   3. df-1st
   4. df-2nd
   5. 1stval
   6. 2ndval
   7. 1stnpr
   8. 2ndnpr
   9. 1st0
   10. 2nd0
   11. op1st
   12. op2nd
   13. op1std
   14. op2ndd
   15. op1stg
   16. op2ndg
   17. ot1stg
   18. ot2ndg
   19. ot3rdg
   20. 1stval2
   21. 2ndval2
   22. oteqimp
   23. fo1st
   24. fo2nd
   25. br1steqg
   26. br2ndeqg
   27. f1stres
   28. f2ndres
   29. fo1stres
   30. fo2ndres
   31. 1st2val
   32. 2nd2val
   33. 1stcof
   34. 2ndcof
   35. xp1st
   36. xp2nd
   37. elxp6
   38. elxp7
   39. eqopi
   40. xp2
   41. unielxp
   42. 1st2nd2
   43. 1st2ndb
   44. xpopth
   45. eqop
   46. eqop2
   47. op1steq
   48. opreuopreu
   49. el2xptp
   50. el2xptp0
   51. el2xpss
   52. 2nd1st
   53. 1st2nd
   54. 1stdm
   55. 2ndrn
   56. 1st2ndbr
   57. releldm2
   58. reldm
   59. releldmdifi
   60. funfv1st2nd
   61. funelss
   62. funeldmdif
   63. sbcopeq1a
   64. csbopeq1a
   65. sbcoteq1a
   66. dfopab2
   67. dfoprab3s
   68. dfoprab3
   69. dfoprab4
   70. dfoprab4f
   71. opabex2
   72. opabn1stprc
   73. opiota
   74. cnvoprab
   75. dfxp3
   76. elopabi
   77. eloprabi
   78. mpomptsx
   79. mpompts
   80. dmmpossx
   81. fmpox
   82. fmpo
   83. fnmpo
   84. fnmpoi
   85. dmmpo
   86. ovmpoelrn
   87. dmmpoga
   88. dmmpogaOLD
   89. dmmpog
   90. mpoexxg
   91. mpoexg
   92. mpoexga
   93. mpoexw
   94. mpoex
   95. mptmpoopabbrd
   96. mptmpoopabbrdOLD
   97. mptmpoopabovd
   98. mptmpoopabbrdOLDOLD
   99. mptmpoopabovdOLD
   100. el2mpocsbcl
   101. el2mpocl
   102. fnmpoovd
   103. offval22
   104. brovpreldm
   105. bropopvvv
   106. bropfvvvvlem
   107. bropfvvvv
   108. ovmptss
   109. relmpoopab
   110. fmpoco
   111. oprabco
   112. oprab2co
   113. df1st2
   114. df2nd2
   115. 1stconst
   116. 2ndconst
   117. dfmpo
   118. mposn
   119. curry1
   120. curry1val
   121. curry1f
   122. curry2
   123. curry2f
   124. curry2val
   125. cnvf1olem
   126. cnvf1o
   127. fparlem1
   128. fparlem2
   129. fparlem3
   130. fparlem4
   131. fpar
   132. fsplit
   133. fsplitfpar
   134. offsplitfpar
   135. f2ndf
   136. fo2ndf
   137. f1o2ndf1
   138. opco1
   139. opco2
   140. opco1i
   141. frxp
   142. xporderlem
   143. poxp
   144. soxp
   145. wexp
   146. fnwelem
   147. fnwe
   148. fnse
   149. fvproj
   150. fimaproj
   151. ralxpes
   152. ralxp3f
   153. ralxp3
   154. ralxp3es
9. Induction on Cartesian products
   1. frpoins3xpg
   2. frpoins3xp3g
10. Ordering on Cartesian products
    1. xpord2lem
    2. poxp2
    3. frxp2
    4. xpord2pred
    5. sexp2
    6. xpord2indlem
    7. xpord2ind
    8. xpord3lem
    9. poxp3
    10. frxp3
    11. xpord3pred
    12. sexp3
    13. xpord3inddlem
    14. xpord3indd
    15. xpord3ind
11. Ordering Ordinal Sequences
    1. orderseqlem
    2. poseq
    3. soseq
12. The support of functions
    1. csupp
    2. df-supp
    3. suppval
    4. supp0prc
    5. suppvalbr
    6. supp0
    7. suppval1
    8. suppvalfng
    9. suppvalfn
    10. elsuppfng
    11. elsuppfn
    12. cnvimadfsn
    13. suppimacnvss
    14. suppimacnv
    15. fsuppeq
    16. fsuppeqg
    17. suppssdm
    18. suppsnop
    19. snopsuppss
    20. fvn0elsupp
    21. fvn0elsuppb
    22. rexsupp
    23. ressuppss
    24. suppun
    25. ressuppssdif
    26. mptsuppdifd
    27. mptsuppd
    28. extmptsuppeq
    29. suppfnss
    30. funsssuppss
    31. fnsuppres
    32. fnsuppeq0
    33. fczsupp0
    34. suppss
    35. suppssOLD
    36. suppssr
    37. suppssrg
    38. suppssov1
    39. suppssov2
    40. suppssof1
    41. suppss2
    42. suppsssn
    43. suppssfv
    44. suppofssd
    45. suppofss1d
    46. suppofss2d
    47. suppco
    48. suppcoss
    49. supp0cosupp0
    50. imacosupp
13. Special maps-to operations
    1. opeliunxp2f
    2. mpoxeldm
    3. mpoxneldm
    4. mpoxopn0yelv
    5. mpoxopynvov0g
    6. mpoxopxnop0
    7. mpoxopx0ov0
    8. mpoxopxprcov0
    9. mpoxopynvov0
    10. mpoxopoveq
    11. mpoxopovel
    12. mpoxopoveqd
    13. brovex
    14. brovmpoex
    15. sprmpod
14. Function transposition
    1. ctpos
    2. df-tpos
    3. tposss
    4. tposeq
    5. tposeqd
    6. tposssxp
    7. reltpos
    8. brtpos2
    9. brtpos0
    10. reldmtpos
    11. brtpos
    12. ottpos
    13. relbrtpos
    14. dmtpos
    15. rntpos
    16. tposexg
    17. ovtpos
    18. tposfun
    19. dftpos2
    20. dftpos3
    21. dftpos4
    22. tpostpos
    23. tpostpos2
    24. tposfn2
    25. tposfo2
    26. tposf2
    27. tposf12
    28. tposf1o2
    29. tposfo
    30. tposf
    31. tposfn
    32. tpos0
    33. tposco
    34. tpossym
    35. tposeqi
    36. tposex
    37. nftpos
    38. tposoprab
    39. tposmpo
    40. tposconst
15. Curry and uncurry
    1. ccur
    2. cunc
    3. df-cur
    4. df-unc
    5. mpocurryd
    6. mpocurryvald
    7. fvmpocurryd
16. Undefined values
    1. cund
    2. df-undef
    3. pwuninel2
    4. pwuninel
    5. undefval
    6. undefnel2
    7. undefnel
    8. undefne0
17. Well-founded recursion
    1. cfrecs
    2. df-frecs
    3. frecseq123
    4. nffrecs
    5. csbfrecsg
    6. fpr3g
    7. frrlem1
    8. frrlem2
    9. frrlem3
    10. frrlem4
    11. frrlem5
    12. frrlem6
    13. frrlem7
    14. frrlem8
    15. frrlem9
    16. frrlem10
    17. frrlem11
    18. frrlem12
    19. frrlem13
    20. frrlem14
    21. fprlem1
    22. fprlem2
    23. fpr2a
    24. fpr1
    25. fpr2
    26. fpr3
    27. frrrel
    28. frrdmss
    29. frrdmcl
    30. fprfung
    31. fprresex
18. Well-ordered recursion
    1. cwrecs
    2. df-wrecs
    3. dfwrecsOLD
    4. wrecseq123
    5. wrecseq123OLD
    6. nfwrecs
    7. nfwrecsOLD
    8. wrecseq1
    9. wrecseq2
    10. wrecseq3
    11. csbwrecsg
    12. wfr3g
    13. wfrlem1OLD
    14. wfrlem2OLD
    15. wfrlem3OLD
    16. wfrlem3OLDa
    17. wfrlem4OLD
    18. wfrlem5OLD
    19. wfrrelOLD
    20. wfrdmssOLD
    21. wfrlem8OLD
    22. wfrdmclOLD
    23. wfrlem10OLD
    24. wfrfunOLD
    25. wfrlem12OLD
    26. wfrlem13OLD
    27. wfrlem14OLD
    28. wfrlem15OLD
    29. wfrlem16OLD
    30. wfrlem17OLD
    31. wfr2aOLD
    32. wfr1OLD
    33. wfr2OLD
    34. wfrrel
    35. wfrdmss
    36. wfrdmcl
    37. wfrfun
    38. wfrresex
    39. wfr2a
    40. wfr1
    41. wfr2
    42. wfr3
    43. wfr3OLD
19. Functions on ordinals; strictly monotone ordinal functions
    1. iunon
    2. iinon
    3. onfununi
    4. onovuni
    5. onoviun
    6. onnseq
    7. wsmo
    8. df-smo
    9. dfsmo2
    10. issmo
    11. issmo2
    12. smoeq
    13. smodm
    14. smores
    15. smores3
    16. smores2
    17. smodm2
    18. smofvon2
    19. iordsmo
    20. smo0
    21. smofvon
    22. smoel
    23. smoiun
    24. smoiso
    25. smoel2
    26. smo11
    27. smoord
    28. smoword
    29. smogt
    30. smocdmdom
    31. smoiso2
20. "Strong" transfinite recursion
    1. crecs
    2. df-recs
    3. dfrecs3
    4. dfrecs3OLD
    5. recseq
    6. nfrecs
    7. tfrlem1
    8. tfrlem3a
    9. tfrlem3
    10. tfrlem4
    11. tfrlem5
    12. recsfval
    13. tfrlem6
    14. tfrlem7
    15. tfrlem8
    16. tfrlem9
    17. tfrlem9a
    18. tfrlem10
    19. tfrlem11
    20. tfrlem12
    21. tfrlem13
    22. tfrlem14
    23. tfrlem15
    24. tfrlem16
    25. tfr1a
    26. tfr2a
    27. tfr2b
    28. tfr1
    29. tfr2
    30. tfr3
    31. tfr1ALT
    32. tfr2ALT
    33. tfr3ALT
    34. recsfnon
    35. recsval
    36. tz7.44lem1
    37. tz7.44-1
    38. tz7.44-2
    39. tz7.44-3
21. Recursive definition generator
    1. crdg
    2. df-rdg
    3. rdgeq1
    4. rdgeq2
    5. rdgeq12
    6. nfrdg
    7. rdglem1
    8. rdgfun
    9. rdgdmlim
    10. rdgfnon
    11. rdgvalg
    12. rdgval
    13. rdg0
    14. rdgseg
    15. rdgsucg
    16. rdgsuc
    17. rdglimg
    18. rdglim
    19. rdg0g
    20. rdgsucmptf
    21. rdgsucmptnf
    22. rdgsucmpt2
    23. rdgsucmpt
    24. rdglim2
    25. rdglim2a
    26. rdg0n
22. Finite recursion
    1. frfnom
    2. fr0g
    3. frsuc
    4. frsucmpt
    5. frsucmptn
    6. frsucmpt2
    7. tz7.48lem
    8. tz7.48-2
    9. tz7.48-1
    10. tz7.48-3
    11. tz7.49
    12. tz7.49c
    13. cseqom
    14. df-seqom
    15. seqomlem0
    16. seqomlem1
    17. seqomlem2
    18. seqomlem3
    19. seqomlem4
    20. seqomeq12
    21. fnseqom
    22. seqom0g
    23. seqomsuc
    24. omsucelsucb
23. Ordinal arithmetic
    1. c1o
    2. c2o
    3. c3o
    4. c4o
    5. coa
    6. comu
    7. coe
    8. df-1o
    9. df-2o
    10. df-3o
    11. df-4o
    12. df-oadd
    13. df-omul
    14. df-oexp
    15. df1o2
    16. df2o3
    17. df2o2
    18. 1oex
    19. 2oex
    20. 1on
    21. 1onOLD
    22. 2on
    23. 2onOLD
    24. 2on0
    25. ord3
    26. 3on
    27. 4on
    28. 1oexOLD
    29. 2oexOLD
    30. 1n0
    31. nlim1
    32. nlim2
    33. xp01disj
    34. xp01disjl
    35. ordgt0ge1
    36. ordge1n0
    37. el1o
    38. ord1eln01
    39. ord2eln012
    40. 1ellim
    41. 2ellim
    42. dif1o
    43. ondif1
    44. ondif2
    45. 2oconcl
    46. 0lt1o
    47. dif20el
    48. 0we1
    49. brwitnlem
    50. fnoa
    51. fnom
    52. fnoe
    53. oav
    54. omv
    55. oe0lem
    56. oev
    57. oevn0
    58. oa0
    59. om0
    60. oe0m
    61. om0x
    62. oe0m0
    63. oe0m1
    64. oe0
    65. oev2
    66. oasuc
    67. oesuclem
    68. omsuc
    69. oesuc
    70. onasuc
    71. onmsuc
    72. onesuc
    73. oa1suc
    74. oalim
    75. omlim
    76. oelim
    77. oacl
    78. omcl
    79. oecl
    80. oa0r
    81. om0r
    82. o1p1e2
    83. o2p2e4
    84. om1
    85. om1r
    86. oe1
    87. oe1m
    88. oaordi
    89. oaord
    90. oacan
    91. oaword
    92. oawordri
    93. oaord1
    94. oaword1
    95. oaword2
    96. oawordeulem
    97. oawordeu
    98. oawordexr
    99. oawordex
    100. oaordex
    101. oa00
    102. oalimcl
    103. oaass
    104. oarec
    105. oaf1o
    106. oacomf1olem
    107. oacomf1o
    108. omordi
    109. omord2
    110. omord
    111. omcan
    112. omword
    113. omwordi
    114. omwordri
    115. omword1
    116. omword2
    117. om00
    118. om00el
    119. omordlim
    120. omlimcl
    121. odi
    122. omass
    123. oneo
    124. omeulem1
    125. omeulem2
    126. omopth2
    127. omeu
    128. oen0
    129. oeordi
    130. oeord
    131. oecan
    132. oeword
    133. oewordi
    134. oewordri
    135. oeworde
    136. oeordsuc
    137. oelim2
    138. oeoalem
    139. oeoa
    140. oeoelem
    141. oeoe
    142. oelimcl
    143. oeeulem
    144. oeeui
    145. oeeu
24. Natural number arithmetic
    1. nna0
    2. nnm0
    3. nnasuc
    4. nnmsuc
    5. nnesuc
    6. nna0r
    7. nnm0r
    8. nnacl
    9. nnmcl
    10. nnecl
    11. nnacli
    12. nnmcli
    13. nnarcl
    14. nnacom
    15. nnaordi
    16. nnaord
    17. nnaordr
    18. nnawordi
    19. nnaass
    20. nndi
    21. nnmass
    22. nnmsucr
    23. nnmcom
    24. nnaword
    25. nnacan
    26. nnaword1
    27. nnaword2
    28. nnmordi
    29. nnmord
    30. nnmword
    31. nnmcan
    32. nnmwordi
    33. nnmwordri
    34. nnawordex
    35. nnaordex
    36. 1onn
    37. 1onnALT
    38. 2onn
    39. 2onnALT
    40. 3onn
    41. 4onn
    42. 1one2o
    43. oaabslem
    44. oaabs
    45. oaabs2
    46. omabslem
    47. omabs
    48. nnm1
    49. nnm2
    50. nn2m
    51. nnneo
    52. nneob
    53. omsmolem
    54. omsmo
    55. omopthlem1
    56. omopthlem2
    57. omopthi
    58. omopth
    59. nnasmo
    60. eldifsucnn
25. Natural addition
    1. cnadd
    2. df-nadd
    3. on2recsfn
    4. on2recsov
    5. on2ind
    6. on3ind
    7. coflton
    8. cofon1
    9. cofon2
    10. cofonr
    11. naddfn
    12. naddcllem
    13. naddcl
    14. naddov
    15. naddov2
    16. naddov3
    17. naddf
    18. naddcom
    19. naddrid
    20. naddlid
    21. naddssim
    22. naddelim
    23. naddel1
    24. naddel2
    25. naddss1
    26. naddss2
    27. naddword1
    28. naddword2
    29. naddunif
    30. naddasslem1
    31. naddasslem2
    32. naddass
    33. nadd32
    34. nadd4
    35. nadd42
    36. naddel12
26. Equivalence relations and classes
    1. wer
    2. cec
    3. cqs
    4. df-er
    5. dfer2
    6. df-ec
    7. dfec2
    8. ecexg
    9. ecexr
    10. df-qs
    11. ereq1
    12. ereq2
    13. errel
    14. erdm
    15. ercl
    16. ersym
    17. ercl2
    18. ersymb
    19. ertr
    20. ertrd
    21. ertr2d
    22. ertr3d
    23. ertr4d
    24. erref
    25. ercnv
    26. errn
    27. erssxp
    28. erex
    29. erexb
    30. iserd
    31. iseri
    32. iseriALT
    33. brdifun
    34. swoer
    35. swoord1
    36. swoord2
    37. swoso
    38. eqerlem
    39. eqer
    40. ider
    41. 0er
    42. eceq1
    43. eceq1d
    44. eceq2
    45. eceq2i
    46. eceq2d
    47. elecg
    48. elec
    49. relelec
    50. ecss
    51. ecdmn0
    52. ereldm
    53. erth
    54. erth2
    55. erthi
    56. erdisj
    57. ecidsn
    58. qseq1
    59. qseq2
    60. qseq2i
    61. qseq2d
    62. qseq12
    63. elqsg
    64. elqs
    65. elqsi
    66. elqsecl
    67. ecelqsg
    68. ecelqsi
    69. ecopqsi
    70. qsexg
    71. qsex
    72. uniqs
    73. qsss
    74. uniqs2
    75. snec
    76. ecqs
    77. ecid
    78. qsid
    79. ectocld
    80. ectocl
    81. elqsn0
    82. ecelqsdm
    83. xpider
    84. iiner
    85. riiner
    86. erinxp
    87. ecinxp
    88. qsinxp
    89. qsdisj
    90. qsdisj2
    91. qsel
    92. uniinqs
    93. qliftlem
    94. qliftrel
    95. qliftel
    96. qliftel1
    97. qliftfun
    98. qliftfund
    99. qliftfuns
    100. qliftf
    101. qliftval
    102. ecoptocl
    103. 2ecoptocl
    104. 3ecoptocl
    105. brecop
    106. brecop2
    107. eroveu
    108. erovlem
    109. erov
    110. eroprf
    111. erov2
    112. eroprf2
    113. ecopoveq
    114. ecopovsym
    115. ecopovtrn
    116. ecopover
    117. eceqoveq
    118. ecovcom
    119. ecovass
    120. ecovdi
27. The mapping operation
    1. cmap
    2. cpm
    3. df-map
    4. df-pm
    5. mapprc
    6. pmex
    7. mapex
    8. fnmap
    9. fnpm
    10. reldmmap
    11. mapvalg
    12. pmvalg
    13. mapval
    14. elmapg
    15. elmapd
    16. elmapdd
    17. mapdm0
    18. elpmg
    19. elpm2g
    20. elpm2r
    21. elpmi
    22. pmfun
    23. elmapex
    24. elmapi
    25. mapfset
    26. mapssfset
    27. mapfoss
    28. fsetsspwxp
    29. fset0
    30. fsetdmprc0
    31. fsetex
    32. f1setex
    33. fosetex
    34. f1osetex
    35. fsetfcdm
    36. fsetfocdm
    37. fsetprcnex
    38. fsetcdmex
    39. fsetexb
    40. elmapfn
    41. elmapfun
    42. elmapssres
    43. fpmg
    44. pmss12g
    45. pmresg
    46. elmap
    47. mapval2
    48. elpm
    49. elpm2
    50. fpm
    51. mapsspm
    52. pmsspw
    53. mapsspw
    54. mapfvd
    55. elmapresaun
    56. fvmptmap
    57. map0e
    58. map0b
    59. map0g
    60. 0map0sn0
    61. mapsnd
    62. map0
    63. mapsn
    64. mapss
    65. fdiagfn
    66. fvdiagfn
    67. mapsnconst
    68. mapsncnv
    69. mapsnf1o2
    70. mapsnf1o3
    71. ralxpmap
28. Infinite Cartesian products
    1. cixp
    2. df-ixp
    3. dfixp
    4. ixpsnval
    5. elixp2
    6. fvixp
    7. ixpfn
    8. elixp
    9. elixpconst
    10. ixpconstg
    11. ixpconst
    12. ixpeq1
    13. ixpeq1d
    14. ss2ixp
    15. ixpeq2
    16. ixpeq2dva
    17. ixpeq2dv
    18. cbvixp
    19. cbvixpv
    20. nfixpw
    21. nfixp
    22. nfixp1
    23. ixpprc
    24. ixpf
    25. uniixp
    26. ixpexg
    27. ixpin
    28. ixpiin
    29. ixpint
    30. ixp0x
    31. ixpssmap2g
    32. ixpssmapg
    33. 0elixp
    34. ixpn0
    35. ixp0
    36. ixpssmap
    37. resixp
    38. undifixp
    39. mptelixpg
    40. resixpfo
    41. elixpsn
    42. ixpsnf1o
    43. mapsnf1o
    44. boxriin
    45. boxcutc
29. Equinumerosity
    1. cen
    2. cdom
    3. csdm
    4. cfn
    5. df-en
    6. df-dom
    7. df-sdom
    8. df-fin
    9. relen
    10. reldom
    11. relsdom
    12. encv
    13. breng
    14. bren
    15. brenOLD
    16. brdom2g
    17. brdomg
    18. brdomgOLD
    19. brdomi
    20. brdomiOLD
    21. brdom
    22. domen
    23. domeng
    24. ctex
    25. f1oen4g
    26. f1dom4g
    27. f1oen3g
    28. f1dom3g
    29. f1oen2g
    30. f1dom2g
    31. f1dom2gOLD
    32. f1oeng
    33. f1domg
    34. f1oen
    35. f1dom
    36. brsdom
    37. isfi
    38. enssdom
    39. dfdom2
    40. endom
    41. sdomdom
    42. sdomnen
    43. brdom2
    44. bren2
    45. enrefg
    46. enref
    47. eqeng
    48. domrefg
    49. en2d
    50. en3d
    51. en2i
    52. en3i
    53. dom2lem
    54. dom2d
    55. dom3d
    56. dom2
    57. dom3
    58. idssen
    59. domssl
    60. domssr
    61. ssdomg
    62. ener
    63. ensymb
    64. ensym
    65. ensymi
    66. ensymd
    67. entr
    68. domtr
    69. entri
    70. entr2i
    71. entr3i
    72. entr4i
    73. endomtr
    74. domentr
    75. f1imaeng
    76. f1imaen2g
    77. f1imaen
    78. en0
    79. en0OLD
    80. en0ALT
    81. en0r
    82. ensn1
    83. ensn1OLD
    84. ensn1g
    85. enpr1g
    86. en1
    87. en1OLD
    88. en1b
    89. en1bOLD
    90. reuen1
    91. euen1
    92. euen1b
    93. en1uniel
    94. en1unielOLD
    95. 2dom
    96. fundmen
    97. fundmeng
    98. cnven
    99. cnvct
    100. fndmeng
    101. mapsnend
    102. mapsnen
    103. snmapen
    104. snmapen1
    105. map1
    106. en2sn
    107. en2snOLD
    108. en2snOLDOLD
    109. snfi
    110. fiprc
    111. unen
    112. enrefnn
    113. en2prd
    114. enpr2d
    115. enpr2dOLD
    116. ssct
    117. ssctOLD
    118. difsnen
    119. domdifsn
    120. xpsnen
    121. xpsneng
    122. xp1en
    123. endisj
    124. undom
    125. undomOLD
    126. xpcomf1o
    127. xpcomco
    128. xpcomen
    129. xpcomeng
    130. xpsnen2g
    131. xpassen
    132. xpdom2
    133. xpdom2g
    134. xpdom1g
    135. xpdom3
    136. xpdom1
    137. domunsncan
    138. omxpenlem
    139. omxpen
    140. omf1o
    141. pw2f1olem
    142. pw2f1o
    143. pw2eng
    144. pw2en
    145. fopwdom
    146. enfixsn
    147. sucdom2OLD
30. Schroeder-Bernstein Theorem
    1. sbthlem1
    2. sbthlem2
    3. sbthlem3
    4. sbthlem4
    5. sbthlem5
    6. sbthlem6
    7. sbthlem7
    8. sbthlem8
    9. sbthlem9
    10. sbthlem10
    11. sbth
    12. sbthb
    13. sbthcl
    14. dfsdom2
    15. brsdom2
    16. sdomnsym
    17. domnsym
    18. 0domg
    19. 0domgOLD
    20. dom0
    21. dom0OLD
    22. 0sdomg
    23. 0sdomgOLD
    24. 0dom
    25. 0sdom
    26. sdom0
    27. sdom0OLD
    28. sdomdomtr
    29. sdomentr
    30. domsdomtr
    31. ensdomtr
    32. sdomirr
    33. sdomtr
    34. sdomn2lp
    35. enen1
    36. enen2
    37. domen1
    38. domen2
    39. sdomen1
    40. sdomen2
    41. domtriord
    42. sdomel
    43. sdomdif
    44. onsdominel
    45. domunsn
    46. fodomr
    47. pwdom
    48. canth2
    49. canth2g
    50. 2pwuninel
    51. 2pwne
    52. disjen
    53. disjenex
    54. domss2
    55. domssex2
    56. domssex
31. Equinumerosity (cont.)
    1. xpf1o
    2. xpen
    3. mapen
    4. mapdom1
    5. mapxpen
    6. xpmapenlem
    7. xpmapen
    8. mapunen
    9. map2xp
    10. mapdom2
    11. mapdom3
    12. pwen
    13. ssenen
    14. limenpsi
    15. limensuci
    16. limensuc
    17. infensuc
32. Finite sets
    1. dif1enlem
    2. dif1enlemOLD
    3. rexdif1en
    4. rexdif1enOLD
    5. dif1en
    6. dif1ennn
    7. dif1enOLD
    8. findcard
    9. findcard2
    10. findcard2s
    11. findcard2d
    12. nnfi
    13. pssnn
    14. ssnnfi
    15. ssnnfiOLD
    16. 0fin
    17. unfi
    18. ssfi
    19. ssfiALT
    20. imafi
    21. pwfir
    22. pwfilem
    23. pwfi
    24. diffi
    25. cnvfi
    26. fnfi
    27. f1oenfi
    28. f1oenfirn
    29. f1domfi
    30. f1domfi2
    31. enreffi
    32. ensymfib
    33. entrfil
    34. enfii
    35. enfi
    36. enfiALT
    37. domfi
    38. entrfi
    39. entrfir
    40. domtrfil
    41. domtrfi
    42. domtrfir
    43. f1imaenfi
    44. ssdomfi
    45. ssdomfi2
    46. sbthfilem
    47. sbthfi
    48. domnsymfi
    49. sdomdomtrfi
    50. domsdomtrfi
    51. sucdom2
33. Pigeonhole Principle
    1. phplem1
    2. phplem2
    3. nneneq
    4. php
    5. php2
    6. php3
    7. php4
    8. php5
    9. phpeqd
    10. nndomog
    11. phplem1OLD
    12. phplem2OLD
    13. phplem3OLD
    14. phplem4OLD
    15. nneneqOLD
    16. phpOLD
    17. php2OLD
    18. php3OLD
    19. phpeqdOLD
    20. nndomogOLD
    21. snnen2oOLD
34. Finite sets (cont.)
    1. onomeneq
    2. onomeneqOLD
    3. onfin
    4. onfin2
    5. nnfiOLD
    6. nndomo
    7. nnsdomo
    8. sucdom
    9. sucdomOLD
    10. snnen2o
    11. 0sdom1dom
    12. 0sdom1domALT
    13. 1sdom2
    14. 1sdom2ALT
    15. sdom1
    16. sdom1OLD
    17. modom
    18. modom2
    19. rex2dom
    20. 1sdom2dom
    21. 1sdom
    22. 1sdomOLD
    23. unxpdomlem1
    24. unxpdomlem2
    25. unxpdomlem3
    26. unxpdom
    27. unxpdom2
    28. sucxpdom
    29. pssinf
    30. fisseneq
    31. ominf
    32. ominfOLD
    33. isinf
    34. isinfOLD
    35. fineqvlem
    36. fineqv
    37. enfiiOLD
    38. pssnnOLD
    39. xpfir
    40. ssfid
    41. infi
    42. rabfi
    43. finresfin
    44. f1finf1o
    45. f1finf1oOLD
    46. nfielex
    47. en1eqsn
    48. en1eqsnOLD
    49. en1eqsnbi
    50. dif1ennnALT
    51. enp1ilem
    52. enp1i
    53. enp1iOLD
    54. en2
    55. en3
    56. en4
    57. findcard2OLD
    58. findcard3
    59. findcard3OLD
    60. ac6sfi
    61. frfi
    62. fimax2g
    63. fimaxg
    64. fisupg
    65. wofi
    66. ordunifi
    67. nnunifi
    68. unblem1
    69. unblem2
    70. unblem3
    71. unblem4
    72. unbnn
    73. unbnn2
    74. isfinite2
    75. nnsdomg
    76. nnsdomgOLD
    77. isfiniteg
    78. infsdomnn
    79. infsdomnnOLD
    80. infn0
    81. infn0ALT
    82. fin2inf
    83. unfilem1
    84. unfilem2
    85. unfilem3
    86. unfiOLD
    87. unfir
    88. unfi2
    89. difinf
    90. xpfi
    91. xpfiOLD
    92. 3xpfi
    93. domunfican
    94. infcntss
    95. prfi
    96. tpfi
    97. fiint
    98. fodomfi
    99. fodomfib
    100. fofinf1o
    101. rneqdmfinf1o
    102. fidomdm
    103. dmfi
    104. fundmfibi
    105. resfnfinfin
    106. residfi
    107. cnvfiALT
    108. rnfi
    109. f1dmvrnfibi
    110. f1vrnfibi
    111. fofi
    112. f1fi
    113. iunfi
    114. unifi
    115. unifi2
    116. infssuni
    117. unirnffid
    118. imafiALT
    119. pwfilemOLD
    120. pwfiOLD
    121. mapfi
    122. ixpfi
    123. ixpfi2
    124. mptfi
    125. abrexfi
    126. cnvimamptfin
    127. elfpw
    128. unifpw
    129. f1opwfi
    130. fissuni
    131. fipreima
    132. finsschain
    133. indexfi
35. Finitely supported functions
    1. cfsupp
    2. df-fsupp
    3. relfsupp
    4. relprcnfsupp
    5. isfsupp
    6. isfsuppd
    7. funisfsupp
    8. fsuppimp
    9. fsuppimpd
    10. fisuppfi
    11. fidmfisupp
    12. fdmfisuppfi
    13. fdmfifsupp
    14. fsuppmptdm
    15. fndmfisuppfi
    16. fndmfifsupp
    17. suppeqfsuppbi
    18. suppssfifsupp
    19. fsuppsssupp
    20. fsuppxpfi
    21. fczfsuppd
    22. fsuppun
    23. fsuppunfi
    24. fsuppunbi
    25. 0fsupp
    26. snopfsupp
    27. funsnfsupp
    28. fsuppres
    29. fmptssfisupp
    30. ressuppfi
    31. resfsupp
    32. resfifsupp
    33. ffsuppbi
    34. fsuppmptif
    35. sniffsupp
    36. fsuppcolem
    37. fsuppco
    38. fsuppco2
    39. fsuppcor
    40. mapfienlem1
    41. mapfienlem2
    42. mapfienlem3
    43. mapfien
    44. mapfien2
36. Finite intersections
    1. cfi
    2. df-fi
    3. fival
    4. elfi
    5. elfi2
    6. elfir
    7. intrnfi
    8. iinfi
    9. inelfi
    10. ssfii
    11. fi0
    12. fieq0
    13. fiin
    14. dffi2
    15. fiss
    16. inficl
    17. fipwuni
    18. fisn
    19. fiuni
    20. fipwss
    21. elfiun
    22. dffi3
    23. fifo
37. Hall's marriage theorem
    1. marypha1lem
    2. marypha1
    3. marypha2lem1
    4. marypha2lem2
    5. marypha2lem3
    6. marypha2lem4
    7. marypha2
38. Supremum and infimum
    1. csup
    2. cinf
    3. df-sup
    4. df-inf
    5. dfsup2
    6. supeq1
    7. supeq1d
    8. supeq1i
    9. supeq2
    10. supeq3
    11. supeq123d
    12. nfsup
    13. supmo
    14. supexd
    15. supeu
    16. supval2
    17. eqsup
    18. eqsupd
    19. supcl
    20. supub
    21. suplub
    22. suplub2
    23. supnub
    24. supex
    25. sup00
    26. sup0riota
    27. sup0
    28. supmax
    29. fisup2g
    30. fisupcl
    31. supgtoreq
    32. suppr
    33. supsn
    34. supisolem
    35. supisoex
    36. supiso
    37. infeq1
    38. infeq1d
    39. infeq1i
    40. infeq2
    41. infeq3
    42. infeq123d
    43. nfinf
    44. infexd
    45. eqinf
    46. eqinfd
    47. infval
    48. infcllem
    49. infcl
    50. inflb
    51. infglb
    52. infglbb
    53. infnlb
    54. infex
    55. infmin
    56. infmo
    57. infeu
    58. fimin2g
    59. fiming
    60. fiinfg
    61. fiinf2g
    62. fiinfcl
    63. infltoreq
    64. infpr
    65. infsupprpr
    66. infsn
    67. inf00
    68. infempty
    69. infiso
39. Ordinal isomorphism, Hartogs's theorem
    1. coi
    2. df-oi
    3. dfoi
    4. oieq1
    5. oieq2
    6. nfoi
    7. ordiso2
    8. ordiso
    9. ordtypecbv
    10. ordtypelem1
    11. ordtypelem2
    12. ordtypelem3
    13. ordtypelem4
    14. ordtypelem5
    15. ordtypelem6
    16. ordtypelem7
    17. ordtypelem8
    18. ordtypelem9
    19. ordtypelem10
    20. oi0
    21. oicl
    22. oif
    23. oiiso2
    24. ordtype
    25. oiiniseg
    26. ordtype2
    27. oiexg
    28. oion
    29. oiiso
    30. oien
    31. oieu
    32. oismo
    33. oiid
    34. hartogslem1
    35. hartogslem2
    36. hartogs
    37. wofib
    38. wemaplem1
    39. wemaplem2
    40. wemaplem3
    41. wemappo
    42. wemapsolem
    43. wemapso
    44. wemapso2lem
    45. wemapso2
    46. card2on
    47. card2inf
40. Hartogs function
    1. char
    2. df-har
    3. harf
    4. harcl
    5. harval
    6. elharval
    7. harndom
    8. harword
41. Weak dominance
    1. cwdom
    2. df-wdom
    3. relwdom
    4. brwdom
    5. brwdomi
    6. brwdomn0
    7. 0wdom
    8. fowdom
    9. wdomref
    10. brwdom2
    11. domwdom
    12. wdomtr
    13. wdomen1
    14. wdomen2
    15. wdompwdom
    16. canthwdom
    17. wdom2d
    18. wdomd
    19. brwdom3
    20. brwdom3i
    21. unwdomg
    22. xpwdomg
    23. wdomima2g
    24. wdomimag
    25. unxpwdom2
    26. unxpwdom
    27. ixpiunwdom
    28. harwdom