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. ordon
   3. onprc
   4. ssorduni
   5. ssonuni
   6. ssonunii
   7. ordeleqon
   8. ordsson
   9. onss
   10. predon
   11. ssonprc
   12. onuni
   13. orduni
   14. onint
   15. onint0
   16. onssmin
   17. onminesb
   18. onminsb
   19. oninton
   20. onintrab
   21. onintrab2
   22. onnmin
   23. onnminsb
   24. oneqmin
   25. uniordint
   26. onminex
   27. sucon
   28. sucexb
   29. sucexg
   30. sucex
   31. onmindif2
   32. suceloni
   33. ordsuc
   34. ordpwsuc
   35. onpwsuc
   36. sucelon
   37. ordsucss
   38. onpsssuc
   39. ordelsuc
   40. onsucmin
   41. ordsucelsuc
   42. ordsucsssuc
   43. ordsucuniel
   44. ordsucun
   45. ordunpr
   46. ordunel
   47. onsucuni
   48. ordsucuni
   49. orduniorsuc
   50. unon
   51. ordunisuc
   52. orduniss2
   53. onsucuni2
   54. 0elsuc
   55. limon
   56. onssi
   57. onsuci
   58. onuniorsuci
   59. onuninsuci
   60. onsucssi
   61. nlimsucg
   62. orduninsuc
   63. ordunisuc2
   64. ordzsl
   65. onzsl
   66. dflim3
   67. dflim4
   68. limsuc
   69. limsssuc
   70. nlimon
   71. 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. ordom
   11. elnn
   12. omon
   13. omelon2
   14. nnlim
   15. omssnlim
   16. limom
   17. peano2b
   18. nnsuc
   19. omsucne
   20. ssnlim
   21. omsinds
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. 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. algrflem
   135. frxp
   136. xporderlem
   137. poxp
   138. soxp
   139. wexp
   140. fnwelem
   141. fnwe
   142. fnse
   143. fvproj
   144. 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. cwrecs
    2. df-wrecs
    3. wrecseq123
    4. nfwrecs
    5. wrecseq1
    6. wrecseq2
    7. wrecseq3
    8. wfr3g
    9. wfrlem1
    10. wfrlem2
    11. wfrlem3
    12. wfrlem3a
    13. wfrlem4
    14. wfrlem5
    15. wfrrel
    16. wfrdmss
    17. wfrlem8
    18. wfrdmcl
    19. wfrlem10
    20. wfrfun
    21. wfrlem12
    22. wfrlem13
    23. wfrlem14
    24. wfrlem15
    25. wfrlem16
    26. wfrlem17
    27. wfr2a
    28. wfr1
    29. wfr2
    30. wfr3
15. 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
16. "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
17. 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
18. Finite recursion
    1. frfnom
    2. fr0g
    3. frsuc
    4. frsucmpt
    5. frsucmptn
    6. frsucmpt2w
    7. frsucmpt2
    8. tz7.48lem
    9. tz7.48-2
    10. tz7.48-1
    11. tz7.48-3
    12. tz7.49
    13. tz7.49c
    14. cseqom
    15. df-seqom
    16. seqomlem0
    17. seqomlem1
    18. seqomlem2
    19. seqomlem3
    20. seqomlem4
    21. seqomeq12
    22. fnseqom
    23. seqom0g
    24. seqomsuc
    25. omsucelsucb
19. 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. 1on
    16. 2on
    17. 2on0
    18. 3on
    19. 4on
    20. df1o2
    21. 1oex
    22. 1oexOLD
    23. df2o3
    24. df2o2
    25. 2oex
    26. 2oexOLD
    27. 1n0
    28. xp01disj
    29. xp01disjl
    30. ordgt0ge1
    31. ordge1n0
    32. el1o
    33. dif1o
    34. ondif1
    35. ondif2
    36. 2oconcl
    37. 0lt1o
    38. dif20el
    39. 0we1
    40. brwitnlem
    41. fnoa
    42. fnom
    43. fnoe
    44. oav
    45. omv
    46. oe0lem
    47. oev
    48. oevn0
    49. oa0
    50. om0
    51. oe0m
    52. om0x
    53. oe0m0
    54. oe0m1
    55. oe0
    56. oev2
    57. oasuc
    58. oesuclem
    59. omsuc
    60. oesuc
    61. onasuc
    62. onmsuc
    63. onesuc
    64. oa1suc
    65. oalim
    66. omlim
    67. oelim
    68. oacl
    69. omcl
    70. oecl
    71. oa0r
    72. om0r
    73. o1p1e2
    74. o2p2e4
    75. o2p2e4OLD
    76. om1
    77. om1r
    78. oe1
    79. oe1m
    80. oaordi
    81. oaord
    82. oacan
    83. oaword
    84. oawordri
    85. oaord1
    86. oaword1
    87. oaword2
    88. oawordeulem
    89. oawordeu
    90. oawordexr
    91. oawordex
    92. oaordex
    93. oa00
    94. oalimcl
    95. oaass
    96. oarec
    97. oaf1o
    98. oacomf1olem
    99. oacomf1o
    100. omordi
    101. omord2
    102. omord
    103. omcan
    104. omword
    105. omwordi
    106. omwordri
    107. omword1
    108. omword2
    109. om00
    110. om00el
    111. omordlim
    112. omlimcl
    113. odi
    114. omass
    115. oneo
    116. omeulem1
    117. omeulem2
    118. omopth2
    119. omeu
    120. oen0
    121. oeordi
    122. oeord
    123. oecan
    124. oeword
    125. oewordi
    126. oewordri
    127. oeworde
    128. oeordsuc
    129. oelim2
    130. oeoalem
    131. oeoa
    132. oeoelem
    133. oeoe
    134. oelimcl
    135. oeeulem
    136. oeeui
    137. oeeu
20. 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
21. 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
22. 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
23. 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
24. 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. bren
    14. brdomg
    15. brdomi
    16. brdom
    17. domen
    18. domeng
    19. ctex
    20. f1oen3g
    21. f1oen2g
    22. f1dom2g
    23. f1oeng
    24. f1domg
    25. f1oen
    26. f1dom
    27. brsdom
    28. isfi
    29. enssdom
    30. dfdom2
    31. endom
    32. sdomdom
    33. sdomnen
    34. brdom2
    35. bren2
    36. enrefg
    37. enref
    38. eqeng
    39. domrefg
    40. en2d
    41. en3d
    42. en2i
    43. en3i
    44. dom2lem
    45. dom2d
    46. dom3d
    47. dom2
    48. dom3
    49. idssen
    50. ssdomg
    51. ener
    52. ensymb
    53. ensym
    54. ensymi
    55. ensymd
    56. entr
    57. domtr
    58. entri
    59. entr2i
    60. entr3i
    61. entr4i
    62. endomtr
    63. domentr
    64. f1imaeng
    65. f1imaen2g
    66. f1imaen
    67. en0
    68. en0OLD
    69. ensn1
    70. ensn1g
    71. enpr1g
    72. en1
    73. en1b
    74. reuen1
    75. euen1
    76. euen1b
    77. en1uniel
    78. 2dom
    79. fundmen
    80. fundmeng
    81. cnven
    82. cnvct
    83. fndmeng
    84. mapsnend
    85. mapsnen
    86. snmapen
    87. snmapen1
    88. map1
    89. en2sn
    90. en2snOLD
    91. snfi
    92. fiprc
    93. unen
    94. enrefnn
    95. enpr2d
    96. ssct
    97. difsnen
    98. domdifsn
    99. xpsnen
    100. xpsneng
    101. xp1en
    102. endisj
    103. undom
    104. xpcomf1o
    105. xpcomco
    106. xpcomen
    107. xpcomeng
    108. xpsnen2g
    109. xpassen
    110. xpdom2
    111. xpdom2g
    112. xpdom1g
    113. xpdom3
    114. xpdom1
    115. domunsncan
    116. omxpenlem
    117. omxpen
    118. omf1o
    119. pw2f1olem
    120. pw2f1o
    121. pw2eng
    122. pw2en
    123. fopwdom
    124. enfixsn
    125. sucdom2
25. 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
26. 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
27. Pigeonhole Principle
    1. phplem1
    2. phplem2
    3. phplem3
    4. phplem4
    5. nneneq
    6. php
    7. php2
    8. php3
    9. php4
    10. php5
    11. phpeqd
    12. snnen2o
    13. nndomog
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. imafi
    16. pwfir
    17. pwfilem
    18. pwfi
    19. cnvfi
    20. fnfi
    21. f1oenfi
    22. f1oenfirn
    23. enreffi
    24. ensymfib
    25. entrfil
    26. enfii
    27. enfi
    28. entrfi
    29. entrfir
    30. onomeneq
    31. onfin
    32. onfin2
    33. nnfiOLD
    34. nndomo
    35. nnsdomo
    36. sucdom
    37. 0sdom1dom
    38. 1sdom2
    39. sdom1
    40. modom
    41. modom2
    42. 1sdom
    43. unxpdomlem1
    44. unxpdomlem2
    45. unxpdomlem3
    46. unxpdom
    47. unxpdom2
    48. sucxpdom
    49. pssinf
    50. fisseneq
    51. ominf
    52. isinf
    53. fineqvlem
    54. fineqv
    55. enfiOLD
    56. enfiiOLD
    57. pssnnOLD
    58. ssfiOLD
    59. domfi
    60. xpfir
    61. ssfid
    62. infi
    63. rabfi
    64. finresfin
    65. f1finf1o
    66. nfielex
    67. en1eqsn
    68. en1eqsnbi
    69. diffi
    70. dif1enOLD
    71. enp1ilem
    72. enp1i
    73. en2
    74. en3
    75. en4
    76. findcard2OLD
    77. findcard3
    78. ac6sfi
    79. frfi
    80. fimax2g
    81. fimaxg
    82. fisupg
    83. wofi
    84. ordunifi
    85. nnunifi
    86. unblem1
    87. unblem2
    88. unblem3
    89. unblem4
    90. unbnn
    91. unbnn2
    92. isfinite2
    93. nnsdomg
    94. isfiniteg
    95. infsdomnn
    96. infn0
    97. fin2inf
    98. unfilem1
    99. unfilem2
    100. unfilem3
    101. unfiOLD
    102. unfir
    103. unfi2
    104. difinf
    105. xpfi
    106. 3xpfi
    107. domunfican
    108. infcntss
    109. prfi
    110. tpfi
    111. fiint
    112. fodomfi
    113. fodomfib
    114. fofinf1o
    115. rneqdmfinf1o
    116. fidomdm
    117. dmfi
    118. fundmfibi
    119. resfnfinfin
    120. residfi
    121. cnvfiALT
    122. rnfi
    123. f1dmvrnfibi
    124. f1vrnfibi
    125. fofi
    126. f1fi
    127. iunfi
    128. unifi
    129. unifi2
    130. infssuni
    131. unirnffid
    132. imafiOLD
    133. pwfilemOLD
    134. pwfiOLD
    135. mapfi
    136. ixpfi
    137. ixpfi2
    138. mptfi
    139. abrexfi
    140. cnvimamptfin
    141. elfpw
    142. unifpw
    143. f1opwfi
    144. fissuni
    145. fipreima
    146. finsschain
    147. indexfi
29. 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
30. 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
31. Hall's marriage theorem
    1. marypha1lem
    2. marypha1
    3. marypha2lem1
    4. marypha2lem2
    5. marypha2lem3
    6. marypha2lem4
    7. marypha2
32. 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
33. 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
34. Hartogs function
    1. char
    2. df-har
    3. harf
    4. harcl
    5. harval
    6. elharval
    7. harndom
    8. harword
35. 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