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. unexg
   10. unex
   11. unexOLD
   12. tpex
   13. unexb
   14. unexbOLD
   15. unexgOLD
   16. xpexg
   17. xpexd
   18. 3xpexg
   19. xpex
   20. unexd
   21. sqxpexg
   22. abnexg
   23. abnex
   24. snnex
   25. pwnex
   26. difex2
   27. difsnexi
   28. uniuni
   29. uniexr
   30. uniexb
   31. pwexr
   32. pwexb
   33. elpwpwel
   34. eldifpw
   35. elpwun
   36. pwuncl
   37. iunpw
   38. fr3nr
   39. epne3
   40. 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. ssonprc
   14. onuni
   15. orduni
   16. onint
   17. onint0
   18. onssmin
   19. onminesb
   20. onminsb
   21. oninton
   22. onintrab
   23. onintrab2
   24. onnmin
   25. onnminsb
   26. oneqmin
   27. uniordint
   28. onminex
   29. sucon
   30. sucexb
   31. sucexg
   32. sucex
   33. onmindif2
   34. ordsuci
   35. sucexeloni
   36. onsuc
   37. ordsuc
   38. ordpwsuc
   39. onpwsuc
   40. onsucb
   41. ordsucss
   42. onpsssuc
   43. ordelsuc
   44. onsucmin
   45. ordsucelsuc
   46. ordsucsssuc
   47. ordsucuniel
   48. ordsucun
   49. ordunpr
   50. ordunel
   51. onsucuni
   52. ordsucuni
   53. orduniorsuc
   54. unon
   55. ordunisuc
   56. orduniss2
   57. onsucuni2
   58. 0elsuc
   59. limon
   60. onuniorsuc
   61. onssi
   62. onsuci
   63. onuninsuci
   64. onsucssi
   65. nlimsucg
   66. orduninsuc
   67. ordunisuc2
   68. ordzsl
   69. onzsl
   70. dflim3
   71. dflim4
   72. limsuc
   73. limsssuc
   74. nlimon
   75. 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. omun
5. Peano's postulates
   1. peano1
   2. peano2
   3. peano3
   4. peano4
   5. peano5
   6. nn0suc
6. Finite induction (for finite ordinals)
   1. find
   2. finds
   3. findsg
   4. finds2
   5. finds1
   6. 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. rnexd
   16. imaexd
   17. exse2
   18. xpexr
   19. xpexr2
   20. xpexcnv
   21. soex
   22. elxp4
   23. elxp5
   24. cnvexg
   25. cnvex
   26. relcnvexb
   27. f1oexrnex
   28. f1oexbi
   29. coexg
   30. coex
   31. coexd
   32. funcnvuni
   33. fun11uni
   34. resf1extb
   35. resf1ext2b
   36. fex2
   37. fabexd
   38. fabexg
   39. fabexgOLD
   40. fabex
   41. mapex
   42. f1oabexg
   43. f1oabexgOLD
   44. fiunlem
   45. fiun
   46. f1iun
   47. fviunfun
   48. ffoss
   49. f11o
   50. resfunexgALT
   51. cofunexg
   52. cofunex2g
   53. fnexALT
   54. funexw
   55. mptexw
   56. funrnex
   57. zfrep6
   58. focdmex
   59. f1dmex
   60. f1ovv
   61. fvclex
   62. fvresex
   63. abrexexg
   64. abrexex
   65. iunexg
   66. abrexex2g
   67. opabex3d
   68. opabex3rd
   69. opabex3
   70. iunex
   71. abrexex2
   72. abexssex
   73. abexex
   74. f1oweALT
   75. wemoiso
   76. wemoiso2
   77. oprabexd
   78. oprabex
   79. oprabex3
   80. oprabrexex2
   81. ab2rexex
   82. ab2rexex2
   83. xpexgALT
   84. offval3
   85. offres
   86. ofmres
   87. ofmresex
   88. mptcnfimad
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. dmmpog
   89. mpoexxg
   90. mpoexg
   91. mpoexga
   92. mpoexw
   93. mpoex
   94. mptmpoopabbrd
   95. mptmpoopabbrdOLD
   96. mptmpoopabovd
   97. el2mpocsbcl
   98. el2mpocl
   99. fnmpoovd
   100. offval22
   101. brovpreldm
   102. bropopvvv
   103. bropfvvvvlem
   104. bropfvvvv
   105. ovmptss
   106. relmpoopab
   107. fmpoco
   108. oprabco
   109. oprab2co
   110. df1st2
   111. df2nd2
   112. 1stconst
   113. 2ndconst
   114. dfmpo
   115. mposn
   116. curry1
   117. curry1val
   118. curry1f
   119. curry2
   120. curry2f
   121. curry2val
   122. cnvf1olem
   123. cnvf1o
   124. fparlem1
   125. fparlem2
   126. fparlem3
   127. fparlem4
   128. fpar
   129. fsplit
   130. fsplitfpar
   131. offsplitfpar
   132. f2ndf
   133. fo2ndf
   134. f1o2ndf1
   135. opco1
   136. opco2
   137. opco1i
   138. frxp
   139. xporderlem
   140. poxp
   141. soxp
   142. wexp
   143. fnwelem
   144. fnwe
   145. fnse
   146. fvproj
   147. fimaproj
   148. ralxpes
   149. ralxp3f
   150. ralxp3
   151. 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. fvdifsupp
    13. cnvimadfsn
    14. suppimacnvss
    15. suppimacnv
    16. fsuppeq
    17. fsuppeqg
    18. suppssdm
    19. suppsnop
    20. snopsuppss
    21. fvn0elsupp
    22. fvn0elsuppb
    23. rexsupp
    24. ressuppss
    25. suppun
    26. ressuppssdif
    27. mptsuppdifd
    28. mptsuppd
    29. extmptsuppeq
    30. suppfnss
    31. funsssuppss
    32. fnsuppres
    33. fnsuppeq0
    34. fczsupp0
    35. suppss
    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. wrecseq123
    4. nfwrecs
    5. wrecseq1
    6. wrecseq2
    7. wrecseq3
    8. csbwrecsg
    9. wfr3g
    10. wfrrel
    11. wfrdmss
    12. wfrdmcl
    13. wfrfun
    14. wfrresex
    15. wfr2a
    16. wfr1
    17. wfr2
    18. wfr3
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. recseq
    5. nfrecs
    6. tfrlem1
    7. tfrlem3a
    8. tfrlem3
    9. tfrlem4
    10. tfrlem5
    11. recsfval
    12. tfrlem6
    13. tfrlem7
    14. tfrlem8
    15. tfrlem9
    16. tfrlem9a
    17. tfrlem10
    18. tfrlem11
    19. tfrlem12
    20. tfrlem13
    21. tfrlem14
    22. tfrlem15
    23. tfrlem16
    24. tfr1a
    25. tfr2a
    26. tfr2b
    27. tfr1
    28. tfr2
    29. tfr3
    30. tfr1ALT
    31. tfr2ALT
    32. tfr3ALT
    33. recsfnon
    34. recsval
    35. tz7.44lem1
    36. tz7.44-1
    37. tz7.44-2
    38. 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. 2on
    22. 2on0
    23. ord3
    24. 3on
    25. 4on
    26. 1n0
    27. nlim1
    28. nlim2
    29. xp01disj
    30. xp01disjl
    31. ordgt0ge1
    32. ordge1n0
    33. el1o
    34. ord1eln01
    35. ord2eln012
    36. 1ellim
    37. 2ellim
    38. dif1o
    39. ondif1
    40. ondif2
    41. 2oconcl
    42. 0lt1o
    43. dif20el
    44. 0we1
    45. brwitnlem
    46. fnoa
    47. fnom
    48. fnoe
    49. oav
    50. omv
    51. oe0lem
    52. oev
    53. oevn0
    54. oa0
    55. om0
    56. oe0m
    57. om0x
    58. oe0m0
    59. oe0m1
    60. oe0
    61. oev2
    62. oasuc
    63. oesuclem
    64. omsuc
    65. oesuc
    66. onasuc
    67. onmsuc
    68. onesuc
    69. oa1suc
    70. oalim
    71. omlim
    72. oelim
    73. oacl
    74. omcl
    75. oecl
    76. oa0r
    77. om0r
    78. o1p1e2
    79. o2p2e4
    80. om1
    81. om1r
    82. oe1
    83. oe1m
    84. oaordi
    85. oaord
    86. oacan
    87. oaword
    88. oawordri
    89. oaord1
    90. oaword1
    91. oaword2
    92. oawordeulem
    93. oawordeu
    94. oawordexr
    95. oawordex
    96. oaordex
    97. oa00
    98. oalimcl
    99. oaass
    100. oarec
    101. oaf1o
    102. oacomf1olem
    103. oacomf1o
    104. omordi
    105. omord2
    106. omord
    107. omcan
    108. omword
    109. omwordi
    110. omwordri
    111. omword1
    112. omword2
    113. om00
    114. om00el
    115. omordlim
    116. omlimcl
    117. odi
    118. omass
    119. oneo
    120. omeulem1
    121. omeulem2
    122. omopth2
    123. omeu
    124. om2
    125. oen0
    126. oeordi
    127. oeord
    128. oecan
    129. oeword
    130. oewordi
    131. oewordri
    132. oeworde
    133. oeordsuc
    134. oelim2
    135. oeoalem
    136. oeoa
    137. oeoelem
    138. oeoe
    139. oelimcl
    140. oeeulem
    141. oeeui
    142. 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. nnaordex2
    37. 1onn
    38. 1onnALT
    39. 2onn
    40. 2onnALT
    41. 3onn
    42. 4onn
    43. 1one2o
    44. oaabslem
    45. oaabs
    46. oaabs2
    47. omabslem
    48. omabs
    49. nnm1
    50. nnm2
    51. nn2m
    52. nnneo
    53. nneob
    54. omsmolem
    55. omsmo
    56. omopthlem1
    57. omopthlem2
    58. omopthi
    59. omopth
    60. nnasmo
    61. 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
    37. naddsuc2
    38. naddoa
    39. omnaddcl
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. brinxper
    34. brdifun
    35. swoer
    36. swoord1
    37. swoord2
    38. swoso
    39. eqerlem
    40. eqer
    41. ider
    42. 0er
    43. eceq1
    44. eceq1d
    45. eceq2
    46. eceq2i
    47. eceq2d
    48. elecg
    49. ecref
    50. elec
    51. relelec
    52. elecres
    53. elecreseq
    54. elecex
    55. ecss
    56. ecdmn0
    57. ereldm
    58. erth
    59. erth2
    60. erthi
    61. erdisj
    62. ecidsn
    63. qseq1
    64. qseq2
    65. qseq2i
    66. qseq1d
    67. qseq2d
    68. qseq12
    69. 0qs
    70. elqsg
    71. elqs
    72. elqsi
    73. elqsecl
    74. ecelqs
    75. ecelqsw
    76. ecelqsi
    77. ecopqsi
    78. qsexg
    79. qsex
    80. uniqs
    81. uniqsw
    82. qsss
    83. uniqs2
    84. snec
    85. ecqs
    86. ecid
    87. qsid
    88. ectocld
    89. ectocl
    90. elqsn0
    91. ecelqsdm
    92. ecelqsdmb
    93. eceldmqs
    94. xpider
    95. iiner
    96. riiner
    97. erinxp
    98. ecinxp
    99. qsinxp
    100. qsdisj
    101. qsdisj2
    102. qsel
    103. uniinqs
    104. qliftlem
    105. qliftrel
    106. qliftel
    107. qliftel1
    108. qliftfun
    109. qliftfund
    110. qliftfuns
    111. qliftf
    112. qliftval
    113. ecoptocl
    114. 2ecoptocl
    115. 3ecoptocl
    116. brecop
    117. brecop2
    118. eroveu
    119. erovlem
    120. erov
    121. eroprf
    122. erov2
    123. eroprf2
    124. ecopoveq
    125. ecopovsym
    126. ecopovtrn
    127. ecopover
    128. eceqoveq
    129. ecovcom
    130. ecovass
    131. ecovdi
27. The mapping operation
    1. cmap
    2. cpm
    3. df-map
    4. df-pm
    5. mapprc
    6. pmex
    7. mapexOLD
    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. elmapssresd
    44. fpmg
    45. pmss12g
    46. pmresg
    47. elmap
    48. mapval2
    49. elpm
    50. elpm2
    51. fpm
    52. mapsspm
    53. pmsspw
    54. mapsspw
    55. mapfvd
    56. elmapresaun
    57. fvmptmap
    58. map0e
    59. map0b
    60. map0g
    61. 0map0sn0
    62. mapsnd
    63. map0
    64. mapsn
    65. mapss
    66. fdiagfn
    67. fvdiagfn
    68. mapsnconst
    69. mapsncnv
    70. mapsnf1o2
    71. mapsnf1o3
    72. 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. brdom2g
    16. brdomg
    17. brdomi
    18. brdom
    19. domen
    20. domeng
    21. ctex
    22. f1oen4g
    23. f1dom4g
    24. f1oen3g
    25. f1dom3g
    26. f1oen2g
    27. f1dom2g
    28. f1oeng
    29. f1domg
    30. f1oen
    31. f1dom
    32. brsdom
    33. isfi
    34. enssdom
    35. enssdomOLD
    36. dfdom2
    37. endom
    38. sdomdom
    39. sdomnen
    40. brdom2
    41. bren2
    42. enrefg
    43. enref
    44. eqeng
    45. domrefg
    46. en2d
    47. en3d
    48. en2i
    49. en3i
    50. dom2lem
    51. dom2d
    52. dom3d
    53. dom2
    54. dom3
    55. idssen
    56. domssl
    57. domssr
    58. ssdomg
    59. ener
    60. ensymb
    61. ensym
    62. ensymi
    63. ensymd
    64. entr
    65. domtr
    66. entri
    67. entr2i
    68. entr3i
    69. entr4i
    70. endomtr
    71. domentr
    72. f1imaeng
    73. f1imaen2g
    74. f1imaen3g
    75. f1imaen
    76. en0
    77. en0ALT
    78. en0r
    79. ensn1
    80. ensn1g
    81. enpr1g
    82. en1
    83. en1b
    84. reuen1
    85. euen1
    86. euen1b
    87. en1uniel
    88. 2dom
    89. fundmen
    90. fundmeng
    91. cnven
    92. cnvct
    93. fndmeng
    94. mapsnend
    95. mapsnen
    96. snmapen
    97. snmapen1
    98. map1
    99. en2sn
    100. 0fi
    101. snfi
    102. fiprc
    103. unen
    104. enrefnn
    105. en2prd
    106. enpr2d
    107. ssct
    108. difsnen
    109. domdifsn
    110. xpsnen
    111. xpsneng
    112. xp1en
    113. endisj
    114. undom
    115. xpcomf1o
    116. xpcomco
    117. xpcomen
    118. xpcomeng
    119. xpsnen2g
    120. xpassen
    121. xpdom2
    122. xpdom2g
    123. xpdom1g
    124. xpdom3
    125. xpdom1
    126. domunsncan
    127. omxpenlem
    128. omxpen
    129. omf1o
    130. pw2f1olem
    131. pw2f1o
    132. pw2eng
    133. pw2en
    134. fopwdom
    135. enfixsn
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. dom0
    20. 0sdomg
    21. 0dom
    22. 0sdom
    23. sdom0
    24. sdomdomtr
    25. sdomentr
    26. domsdomtr
    27. ensdomtr
    28. sdomirr
    29. sdomtr
    30. sdomn2lp
    31. enen1
    32. enen2
    33. domen1
    34. domen2
    35. sdomen1
    36. sdomen2
    37. domtriord
    38. sdomel
    39. sdomdif
    40. onsdominel
    41. domunsn
    42. fodomr
    43. pwdom
    44. canth2
    45. canth2g
    46. 2pwuninel
    47. 2pwne
    48. disjen
    49. disjenex
    50. domss2
    51. domssex2
    52. 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. rexdif1en
    3. dif1en
    4. dif1ennn
    5. findcard
    6. findcard2
    7. findcard2s
    8. findcard2d
    9. nnfi
    10. pssnn
    11. ssnnfi
    12. unfi
    13. unfid
    14. ssfi
    15. ssfiALT
    16. diffi
    17. cnvfi
    18. pwssfi
    19. fnfi
    20. f1oenfi
    21. f1oenfirn
    22. f1domfi
    23. f1domfi2
    24. enreffi
    25. ensymfib
    26. entrfil
    27. enfii
    28. enfi
    29. enfiALT
    30. domfi
    31. entrfi
    32. entrfir
    33. domtrfil
    34. domtrfi
    35. domtrfir
    36. f1imaenfi
    37. ssdomfi
    38. ssdomfi2
    39. sbthfilem
    40. sbthfi
    41. domnsymfi
    42. sdomdomtrfi
    43. domsdomtrfi
    44. sucdom2
33. Pigeonhole Principle
    1. phplem1
    2. phplem2
    3. nneneq
    4. php
    5. php2
    6. php3
    7. php4
    8. php5
    9. phpeqd
    10. nndomog
34. Finite sets (cont.)
    1. onomeneq
    2. onfin
    3. ordfin
    4. onfin2
    5. nndomo
    6. nnsdomo
    7. sucdom
    8. snnen2o
    9. 0sdom1dom
    10. 0sdom1domALT
    11. 1sdom2
    12. 1sdom2ALT
    13. sdom1
    14. modom
    15. modom2
    16. rex2dom
    17. 1sdom2dom
    18. 1sdom
    19. unxpdomlem1
    20. unxpdomlem2
    21. unxpdomlem3
    22. unxpdom
    23. unxpdom2
    24. sucxpdom
    25. pssinf
    26. fisseneq
    27. ominf
    28. isinf
    29. fineqvlem
    30. fineqv
    31. xpfir
    32. ssfid
    33. infi
    34. rabfi
    35. finresfin
    36. f1finf1o
    37. nfielex
    38. en1eqsn
    39. en1eqsnbi
    40. dif1ennnALT
    41. enp1ilem
    42. enp1i
    43. en2
    44. en3
    45. en4
    46. findcard3
    47. ac6sfi
    48. frfi
    49. fimax2g
    50. fimaxg
    51. fisupg
    52. wofi
    53. ordunifi
    54. nnunifi
    55. unblem1
    56. unblem2
    57. unblem3
    58. unblem4
    59. unbnn
    60. unbnn2
    61. isfinite2
    62. nnsdomg
    63. isfiniteg
    64. infsdomnn
    65. infn0
    66. infn0ALT
    67. fin2inf
    68. unfilem1
    69. unfilem2
    70. unfilem3
    71. unfir
    72. unfib
    73. unfi2
    74. difinf
    75. fodomfi
    76. fofi
    77. f1fi
    78. imafi
    79. imafiOLD
    80. pwfir
    81. pwfilem
    82. pwfi
    83. xpfi
    84. 3xpfi
    85. domunfican
    86. infcntss
    87. prfi
    88. prfiALT
    89. tpfi
    90. fiint
    91. fodomfir
    92. fodomfib
    93. fodomfiOLD
    94. fodomfibOLD
    95. fofinf1o
    96. rneqdmfinf1o
    97. fidomdm
    98. dmfi
    99. fundmfibi
    100. resfnfinfin
    101. residfi
    102. cnvfiALT
    103. rnfi
    104. f1dmvrnfibi
    105. f1vrnfibi
    106. iunfi
    107. unifi
    108. unifi2
    109. infssuni
    110. unirnffid
    111. mapfi
    112. ixpfi
    113. ixpfi2
    114. mptfi
    115. abrexfi
    116. cnvimamptfin
    117. elfpw
    118. unifpw
    119. f1opwfi
    120. fissuni
    121. fipreima
    122. finsschain
    123. indexfi
    124. imafi2
    125. unifi3
    126. tfsnfin2
35. Finitely supported functions
    1. cfsupp
    2. df-fsupp
    3. relfsupp
    4. relprcnfsupp
    5. isfsupp
    6. isfsuppd
    7. funisfsupp
    8. fsuppimp
    9. fsuppimpd
    10. fsuppfund
    11. fisuppfi
    12. fidmfisupp
    13. finnzfsuppd
    14. fdmfisuppfi
    15. fdmfifsupp
    16. fsuppmptdm
    17. fndmfisuppfi
    18. fndmfifsupp
    19. suppeqfsuppbi
    20. suppssfifsupp
    21. fsuppsssupp
    22. fsuppsssuppgd
    23. fsuppss
    24. fsuppssov1
    25. fsuppxpfi
    26. fczfsuppd
    27. fsuppun
    28. fsuppunfi
    29. fsuppunbi
    30. 0fsupp
    31. snopfsupp
    32. funsnfsupp
    33. fsuppres
    34. fmptssfisupp
    35. ressuppfi
    36. resfsupp
    37. resfifsupp
    38. ffsuppbi
    39. fsuppmptif
    40. sniffsupp
    41. fsuppcolem
    42. fsuppco
    43. fsuppco2
    44. fsuppcor
    45. mapfienlem1
    46. mapfienlem2
    47. mapfienlem3
    48. mapfien
    49. 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. supssd
    25. supex
    26. sup00
    27. sup0riota
    28. sup0
    29. supmax
    30. fisup2g
    31. fisupcl
    32. supgtoreq
    33. suppr
    34. supsn
    35. supisolem
    36. supisoex
    37. supiso
    38. infeq1
    39. infeq1d
    40. infeq1i
    41. infeq2
    42. infeq3
    43. infeq123d
    44. nfinf
    45. infexd
    46. eqinf
    47. eqinfd
    48. infval
    49. infcllem
    50. infcl
    51. inflb
    52. infglb
    53. infglbb
    54. infnlb
    55. infssd
    56. infex
    57. infmin
    58. infmo
    59. infeu
    60. fimin2g
    61. fiming
    62. fiinfg
    63. fiinf2g
    64. fiinfcl
    65. infltoreq
    66. infpr
    67. infsupprpr
    68. infsn
    69. inf00
    70. infempty
    71. 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