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. epweonOLD
   3. ordon
   4. onprc
   5. ssorduni
   6. ssonuni
   7. ssonunii
   8. ordeleqon
   9. ordsson
   10. onss
   11. predon
   12. predonOLD
   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. sucexeloni
   35. suceloni
   36. suceloniOLD
   37. ordsuc
   38. ordpwsuc
   39. onpwsuc
   40. sucelon
   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. onssi
   61. onsuci
   62. onuniorsuci
   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. tfis
   3. tfis2f
   4. tfis2
   5. tfis3
   6. tfisi
   7. tfinds
   8. tfindsg
   9. tfindsg2
   10. tfindes
   11. tfinds2
   12. 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
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. fornex
   50. f1dmex
   51. f1ovv
   52. fvclex
   53. fvresex
   54. abrexexg
   55. abrexex
   56. iunexg
   57. abrexex2g
   58. opabex3d
   59. opabex3rd
   60. opabex3
   61. iunex
   62. abrexex2
   63. abexssex
   64. abexex
   65. f1oweALT
   66. wemoiso
   67. wemoiso2
   68. oprabexd
   69. oprabex
   70. oprabex3
   71. oprabrexex2
   72. ab2rexex
   73. ab2rexex2
   74. xpexgALT
   75. offval3
   76. offres
   77. ofmres
   78. 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. 2nd1st
   52. 1st2nd
   53. 1stdm
   54. 2ndrn
   55. 1st2ndbr
   56. releldm2
   57. reldm
   58. releldmdifi
   59. funfv1st2nd
   60. funelss
   61. funeldmdif
   62. sbcopeq1a
   63. csbopeq1a
   64. dfopab2
   65. dfoprab3s
   66. dfoprab3
   67. dfoprab4
   68. dfoprab4f
   69. opabex2
   70. opabn1stprc
   71. opiota
   72. cnvoprab
   73. dfxp3
   74. elopabi
   75. eloprabi
   76. mpomptsx
   77. mpompts
   78. dmmpossx
   79. fmpox
   80. fmpo
   81. fnmpo
   82. fnmpoi
   83. dmmpo
   84. ovmpoelrn
   85. dmmpoga
   86. dmmpogaOLD
   87. dmmpog
   88. mpoexxg
   89. mpoexg
   90. mpoexga
   91. mpoexw
   92. mpoex
   93. mptmpoopabbrd
   94. mptmpoopabovd
   95. el2mpocsbcl
   96. el2mpocl
   97. fnmpoovd
   98. offval22
   99. brovpreldm
   100. bropopvvv
   101. bropfvvvvlem
   102. bropfvvvv
   103. ovmptss
   104. relmpoopab
   105. fmpoco
   106. oprabco
   107. oprab2co
   108. df1st2
   109. df2nd2
   110. 1stconst
   111. 2ndconst
   112. dfmpo
   113. mposn
   114. curry1
   115. curry1val
   116. curry1f
   117. curry2
   118. curry2f
   119. curry2val
   120. cnvf1olem
   121. cnvf1o
   122. fparlem1
   123. fparlem2
   124. fparlem3
   125. fparlem4
   126. fpar
   127. fsplit
   128. fsplitOLD
   129. fsplitfpar
   130. offsplitfpar
   131. f2ndf
   132. fo2ndf
   133. f1o2ndf1
   134. opco1
   135. opco2
   136. opco1i
   137. frxp
   138. xporderlem
   139. poxp
   140. soxp
   141. wexp
   142. fnwelem
   143. fnwe
   144. fnse
   145. fvproj
   146. fimaproj
9. 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. frnsuppeq
   16. frnsuppeqg
   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. suppssof1
   40. suppss2
   41. suppsssn
   42. suppssfv
   43. suppofssd
   44. suppofss1d
   45. suppofss2d
   46. suppco
   47. suppcoss
   48. supp0cosupp0
   49. imacosupp
10. 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
11. 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
12. Curry and uncurry
    1. ccur
    2. cunc
    3. df-cur
    4. df-unc
    5. mpocurryd
    6. mpocurryvald
    7. fvmpocurryd
13. Undefined values
    1. cund
    2. df-undef
    3. pwuninel2
    4. pwuninel
    5. undefval
    6. undefnel2
    7. undefnel
    8. undefne0
14. 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
15. 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
16. 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. smorndom
    31. smoiso2
17. "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
18. 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
19. 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
20. 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. 3on
    26. 4on
    27. 1oexOLD
    28. 2oexOLD
    29. 1n0
    30. xp01disj
    31. xp01disjl
    32. ordgt0ge1
    33. ordge1n0
    34. el1o
    35. dif1o
    36. ondif1
    37. ondif2
    38. 2oconcl
    39. 0lt1o
    40. dif20el
    41. 0we1
    42. brwitnlem
    43. fnoa
    44. fnom
    45. fnoe
    46. oav
    47. omv
    48. oe0lem
    49. oev
    50. oevn0
    51. oa0
    52. om0
    53. oe0m
    54. om0x
    55. oe0m0
    56. oe0m1
    57. oe0
    58. oev2
    59. oasuc
    60. oesuclem
    61. omsuc
    62. oesuc
    63. onasuc
    64. onmsuc
    65. onesuc
    66. oa1suc
    67. oalim
    68. omlim
    69. oelim
    70. oacl
    71. omcl
    72. oecl
    73. oa0r
    74. om0r
    75. o1p1e2
    76. o2p2e4
    77. o2p2e4OLD
    78. om1
    79. om1r
    80. oe1
    81. oe1m
    82. oaordi
    83. oaord
    84. oacan
    85. oaword
    86. oawordri
    87. oaord1
    88. oaword1
    89. oaword2
    90. oawordeulem
    91. oawordeu
    92. oawordexr
    93. oawordex
    94. oaordex
    95. oa00
    96. oalimcl
    97. oaass
    98. oarec
    99. oaf1o
    100. oacomf1olem
    101. oacomf1o
    102. omordi
    103. omord2
    104. omord
    105. omcan
    106. omword
    107. omwordi
    108. omwordri
    109. omword1
    110. omword2
    111. om00
    112. om00el
    113. omordlim
    114. omlimcl
    115. odi
    116. omass
    117. oneo
    118. omeulem1
    119. omeulem2
    120. omopth2
    121. omeu
    122. oen0
    123. oeordi
    124. oeord
    125. oecan
    126. oeword
    127. oewordi
    128. oewordri
    129. oeworde
    130. oeordsuc
    131. oelim2
    132. oeoalem
    133. oeoa
    134. oeoelem
    135. oeoe
    136. oelimcl
    137. oeeulem
    138. oeeui
    139. oeeu
21. 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. 2onn
    38. 3onn
    39. 4onn
    40. 1one2o
    41. oaabslem
    42. oaabs
    43. oaabs2
    44. omabslem
    45. omabs
    46. nnm1
    47. nnm2
    48. nn2m
    49. nnneo
    50. nneob
    51. omsmolem
    52. omsmo
    53. omopthlem1
    54. omopthlem2
    55. omopthi
    56. omopth
    57. nnasmo
    58. eldifsucnn
22. 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
23. 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. mapdm0
    17. elpmg
    18. elpm2g
    19. elpm2r
    20. elpmi
    21. pmfun
    22. elmapex
    23. elmapi
    24. mapfset
    25. mapssfset
    26. mapfoss
    27. fsetsspwxp
    28. fset0
    29. fsetdmprc0
    30. fsetex
    31. f1setex
    32. fosetex
    33. f1osetex
    34. fsetfcdm
    35. fsetfocdm
    36. fsetprcnex
    37. fsetcdmex
    38. fsetexb
    39. elmapfn
    40. elmapfun
    41. elmapssres
    42. fpmg
    43. pmss12g
    44. pmresg
    45. elmap
    46. mapval2
    47. elpm
    48. elpm2
    49. fpm
    50. mapsspm
    51. pmsspw
    52. mapsspw
    53. mapfvd
    54. elmapresaun
    55. fvmptmap
    56. map0e
    57. map0b
    58. map0g
    59. 0map0sn0
    60. mapsnd
    61. map0
    62. mapsn
    63. mapss
    64. fdiagfn
    65. fvdiagfn
    66. mapsnconst
    67. mapsncnv
    68. mapsnf1o2
    69. mapsnf1o3
    70. ralxpmap
24. 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
25. 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. f1oen3g
    26. f1dom3g
    27. f1oen2g
    28. f1dom2g
    29. f1dom2gOLD
    30. f1oeng
    31. f1domg
    32. f1oen
    33. f1dom
    34. brsdom
    35. isfi
    36. enssdom
    37. dfdom2
    38. endom
    39. sdomdom
    40. sdomnen
    41. brdom2
    42. bren2
    43. enrefg
    44. enref
    45. eqeng
    46. domrefg
    47. en2d
    48. en3d
    49. en2i
    50. en3i
    51. dom2lem
    52. dom2d
    53. dom3d
    54. dom2
    55. dom3
    56. idssen
    57. ssdomg
    58. ener
    59. ensymb
    60. ensym
    61. ensymi
    62. ensymd
    63. entr
    64. domtr
    65. entri
    66. entr2i
    67. entr3i
    68. entr4i
    69. endomtr
    70. domentr
    71. f1imaeng
    72. f1imaen2g
    73. f1imaen
    74. en0
    75. en0OLD
    76. en0ALT
    77. en0r
    78. ensn1
    79. ensn1OLD
    80. ensn1g
    81. enpr1g
    82. en1
    83. en1OLD
    84. en1b
    85. en1bOLD
    86. reuen1
    87. euen1
    88. euen1b
    89. en1uniel
    90. en1unielOLD
    91. 2dom
    92. fundmen
    93. fundmeng
    94. cnven
    95. cnvct
    96. fndmeng
    97. mapsnend
    98. mapsnen
    99. snmapen
    100. snmapen1
    101. map1
    102. en2sn
    103. en2snOLD
    104. en2snOLDOLD
    105. snfi
    106. fiprc
    107. unen
    108. enrefnn
    109. enpr2d
    110. ssct
    111. difsnen
    112. domdifsn
    113. xpsnen
    114. xpsneng
    115. xp1en
    116. endisj
    117. undom
    118. xpcomf1o
    119. xpcomco
    120. xpcomen
    121. xpcomeng
    122. xpsnen2g
    123. xpassen
    124. xpdom2
    125. xpdom2g
    126. xpdom1g
    127. xpdom3
    128. xpdom1
    129. domunsncan
    130. omxpenlem
    131. omxpen
    132. omf1o
    133. pw2f1olem
    134. pw2f1o
    135. pw2eng
    136. pw2en
    137. fopwdom
    138. enfixsn
    139. sucdom2
26. 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
27. 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
28. Finite sets
    1. dif1enlem
    2. rexdif1en
    3. dif1en
    4. findcard
    5. findcard2
    6. findcard2s
    7. findcard2d
    8. nnfi
    9. pssnn
    10. ssnnfi
    11. ssnnfiOLD
    12. 0fin
    13. unfi
    14. ssfi
    15. ssfiALT
    16. imafi
    17. pwfir
    18. pwfilem
    19. pwfi
    20. diffi
    21. cnvfi
    22. fnfi
    23. f1oenfi
    24. f1oenfirn
    25. f1domfi
    26. f1domfi2
    27. enreffi
    28. ensymfib
    29. entrfil
    30. enfii
    31. enfi
    32. enfiALT
    33. domfi
    34. entrfi
    35. entrfir
    36. domtrfil
    37. domtrfi
    38. domtrfir
    39. f1imaenfi
    40. ssdomfi
    41. ssdomfi2
    42. sbthfilem
    43. sbthfi
    44. domnsymfi
    45. sdomdomtrfi
    46. domsdomtrfi
29. Pigeonhole Principle
    1. phplem1
    2. phplem2
    3. nneneq
    4. php
    5. php2
    6. php3
    7. php4
    8. php5
    9. phpeqd
    10. snnen2o
    11. nndomog
    12. phplem1OLD
    13. phplem2OLD
    14. phplem3OLD
    15. phplem4OLD
    16. nneneqOLD
    17. phpOLD
    18. php2OLD
    19. php3OLD
    20. phpeqdOLD
    21. nndomogOLD
30. Finite sets (cont.)
    1. onomeneq
    2. onfin
    3. onfin2
    4. nnfiOLD
    5. nndomo
    6. nnsdomo
    7. sucdom
    8. 0sdom1dom
    9. 1sdom2
    10. sdom1
    11. modom
    12. modom2
    13. 1sdom
    14. unxpdomlem1
    15. unxpdomlem2
    16. unxpdomlem3
    17. unxpdom
    18. unxpdom2
    19. sucxpdom
    20. pssinf
    21. fisseneq
    22. ominf
    23. isinf
    24. fineqvlem
    25. fineqv
    26. enfiiOLD
    27. pssnnOLD
    28. xpfir
    29. ssfid
    30. infi
    31. rabfi
    32. finresfin
    33. f1finf1o
    34. nfielex
    35. en1eqsn
    36. en1eqsnbi
    37. dif1enALT
    38. enp1ilem
    39. enp1i
    40. en2
    41. en3
    42. en4
    43. findcard2OLD
    44. findcard3
    45. ac6sfi
    46. frfi
    47. fimax2g
    48. fimaxg
    49. fisupg
    50. wofi
    51. ordunifi
    52. nnunifi
    53. unblem1
    54. unblem2
    55. unblem3
    56. unblem4
    57. unbnn
    58. unbnn2
    59. isfinite2
    60. nnsdomg
    61. isfiniteg
    62. infsdomnn
    63. infn0
    64. fin2inf
    65. unfilem1
    66. unfilem2
    67. unfilem3
    68. unfiOLD
    69. unfir
    70. unfi2
    71. difinf
    72. xpfi
    73. 3xpfi
    74. domunfican
    75. infcntss
    76. prfi
    77. tpfi
    78. fiint
    79. fodomfi
    80. fodomfib
    81. fofinf1o
    82. rneqdmfinf1o
    83. fidomdm
    84. dmfi
    85. fundmfibi
    86. resfnfinfin
    87. residfi
    88. cnvfiALT
    89. rnfi
    90. f1dmvrnfibi
    91. f1vrnfibi
    92. fofi
    93. f1fi
    94. iunfi
    95. unifi
    96. unifi2
    97. infssuni
    98. unirnffid
    99. imafiALT
    100. pwfilemOLD
    101. pwfiOLD
    102. mapfi
    103. ixpfi
    104. ixpfi2
    105. mptfi
    106. abrexfi
    107. cnvimamptfin
    108. elfpw
    109. unifpw
    110. f1opwfi
    111. fissuni
    112. fipreima
    113. finsschain
    114. indexfi
31. Finitely supported functions
    1. cfsupp
    2. df-fsupp
    3. relfsupp
    4. relprcnfsupp
    5. isfsupp
    6. funisfsupp
    7. fsuppimp
    8. fsuppimpd
    9. fisuppfi
    10. fdmfisuppfi
    11. fdmfifsupp
    12. fsuppmptdm
    13. fndmfisuppfi
    14. fndmfifsupp
    15. suppeqfsuppbi
    16. suppssfifsupp
    17. fsuppsssupp
    18. fsuppxpfi
    19. fczfsuppd
    20. fsuppun
    21. fsuppunfi
    22. fsuppunbi
    23. 0fsupp
    24. snopfsupp
    25. funsnfsupp
    26. fsuppres
    27. ressuppfi
    28. resfsupp
    29. resfifsupp
    30. frnfsuppbi
    31. fsuppmptif
    32. sniffsupp
    33. fsuppcolem
    34. fsuppco
    35. fsuppco2
    36. fsuppcor
    37. mapfienlem1
    38. mapfienlem2
    39. mapfienlem3
    40. mapfien
    41. mapfien2
32. 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
33. Hall's marriage theorem
    1. marypha1lem
    2. marypha1
    3. marypha2lem1
    4. marypha2lem2
    5. marypha2lem3
    6. marypha2lem4
    7. marypha2
34. 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
35. 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
36. Hartogs function
    1. char
    2. df-har
    3. harf
    4. harcl
    5. harval
    6. elharval
    7. harndom
    8. harword
37. 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