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. sqxpexg
    18. abnexg
    19. abnex
    20. snnex
    21. pwnex
    22. difex2
    23. difsnexi
    24. uniuni
    25. uniexr
    26. uniexb
    27. pwexr
    28. pwexb
    29. elpwpwel
    30. eldifpw
    31. elpwun
    32. pwuncl
    33. iunpw
    34. fr3nr
    35. epne3
    36. 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. dmex
    6. rnex
    7. iprc
    8. resiexg
    9. imaexg
    10. imaex
    11. exse2
    12. xpexr
    13. xpexr2
    14. xpexcnv
    15. soex
    16. elxp4
    17. elxp5
    18. cnvexg
    19. cnvex
    20. relcnvexb
    21. f1oexrnex
    22. f1oexbi
    23. coexg
    24. coex
    25. funcnvuni
    26. fun11uni
    27. fex2
    28. fabexg
    29. fabex
    30. dmfex
    31. f1oabexg
    32. fiunlem
    33. fiun
    34. f1iun
    35. fviunfun
    36. ffoss
    37. f11o
    38. resfunexgALT
    39. cofunexg
    40. cofunex2g
    41. fnexALT
    42. funexw
    43. mptexw
    44. funrnex
    45. zfrep6
    46. fornex
    47. f1dmex
    48. f1ovv
    49. fvclex
    50. fvresex
    51. abrexexg
    52. abrexex
    53. iunexg
    54. abrexex2g
    55. opabex3d
    56. opabex3rd
    57. opabex3
    58. iunex
    59. abrexex2
    60. abexssex
    61. abexex
    62. f1oweALT
    63. wemoiso
    64. wemoiso2
    65. oprabexd
    66. oprabex
    67. oprabex3
    68. oprabrexex2
    69. ab2rexex
    70. ab2rexex2
    71. xpexgALT
    72. offval3
    73. offres
    74. ofmres
    75. 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. suppvalfn
    9. elsuppfn
    10. cnvimadfsn
    11. suppimacnvss
    12. suppimacnv
    13. frnsuppeq
    14. suppssdm
    15. suppsnop
    16. snopsuppss
    17. fvn0elsupp
    18. fvn0elsuppb
    19. rexsupp
    20. ressuppss
    21. suppun
    22. ressuppssdif
    23. mptsuppdifd
    24. mptsuppd
    25. extmptsuppeq
    26. suppfnss
    27. funsssuppss
    28. fnsuppres
    29. fnsuppeq0
    30. fczsupp0
    31. suppss
    32. suppssr
    33. suppssov1
    34. suppssof1
    35. suppss2
    36. suppsssn
    37. suppssfv
    38. suppofssd
    39. suppofss1d
    40. suppofss2d
    41. suppco
    42. suppcoss
    43. supp0cosupp0
    44. supp0cosupp0OLD
    45. imacosupp
    46. imacosuppOLD
  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. 1oex
    17. 2on
    18. 2oex
    19. 2on0
    20. 3on
    21. 4on
    22. df1o2
    23. df2o3
    24. df2o2
    25. 1n0
    26. xp01disj
    27. xp01disjl
    28. ordgt0ge1
    29. ordge1n0
    30. el1o
    31. dif1o
    32. ondif1
    33. ondif2
    34. 2oconcl
    35. 0lt1o
    36. dif20el
    37. 0we1
    38. brwitnlem
    39. fnoa
    40. fnom
    41. fnoe
    42. oav
    43. omv
    44. oe0lem
    45. oev
    46. oevn0
    47. oa0
    48. om0
    49. oe0m
    50. om0x
    51. oe0m0
    52. oe0m1
    53. oe0
    54. oev2
    55. oasuc
    56. oesuclem
    57. omsuc
    58. oesuc
    59. onasuc
    60. onmsuc
    61. onesuc
    62. oa1suc
    63. oalim
    64. omlim
    65. oelim
    66. oacl
    67. omcl
    68. oecl
    69. oa0r
    70. om0r
    71. o1p1e2
    72. o2p2e4
    73. o2p2e4OLD
    74. om1
    75. om1r
    76. oe1
    77. oe1m
    78. oaordi
    79. oaord
    80. oacan
    81. oaword
    82. oawordri
    83. oaord1
    84. oaword1
    85. oaword2
    86. oawordeulem
    87. oawordeu
    88. oawordexr
    89. oawordex
    90. oaordex
    91. oa00
    92. oalimcl
    93. oaass
    94. oarec
    95. oaf1o
    96. oacomf1olem
    97. oacomf1o
    98. omordi
    99. omord2
    100. omord
    101. omcan
    102. omword
    103. omwordi
    104. omwordri
    105. omword1
    106. omword2
    107. om00
    108. om00el
    109. omordlim
    110. omlimcl
    111. odi
    112. omass
    113. oneo
    114. omeulem1
    115. omeulem2
    116. omopth2
    117. omeu
    118. oen0
    119. oeordi
    120. oeord
    121. oecan
    122. oeword
    123. oewordi
    124. oewordri
    125. oeworde
    126. oeordsuc
    127. oelim2
    128. oeoalem
    129. oeoa
    130. oeoelem
    131. oeoe
    132. oelimcl
    133. oeeulem
    134. oeeui
    135. 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. elmapfn
    25. elmapfun
    26. elmapssres
    27. fpmg
    28. pmss12g
    29. pmresg
    30. elmap
    31. mapval2
    32. elpm
    33. elpm2
    34. fpm
    35. mapsspm
    36. pmsspw
    37. mapsspw
    38. mapfvd
    39. elmapresaun
    40. fvmptmap
    41. map0e
    42. map0b
    43. map0g
    44. 0map0sn0
    45. mapsnd
    46. map0
    47. mapsn
    48. mapss
    49. fdiagfn
    50. fvdiagfn
    51. mapsnconst
    52. mapsncnv
    53. mapsnf1o2
    54. mapsnf1o3
    55. 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. ensn1
    69. ensn1g
    70. enpr1g
    71. en1
    72. en1b
    73. reuen1
    74. euen1
    75. euen1b
    76. en1uniel
    77. 2dom
    78. fundmen
    79. fundmeng
    80. cnven
    81. cnvct
    82. fndmeng
    83. mapsnend
    84. mapsnen
    85. snmapen
    86. snmapen1
    87. map1
    88. en2sn
    89. snfi
    90. fiprc
    91. unen
    92. enpr2d
    93. ssct
    94. difsnen
    95. domdifsn
    96. xpsnen
    97. xpsneng
    98. xp1en
    99. endisj
    100. undom
    101. xpcomf1o
    102. xpcomco
    103. xpcomen
    104. xpcomeng
    105. xpsnen2g
    106. xpassen
    107. xpdom2
    108. xpdom2g
    109. xpdom1g
    110. xpdom3
    111. xpdom1
    112. domunsncan
    113. omxpenlem
    114. omxpen
    115. omf1o
    116. pw2f1olem
    117. pw2f1o
    118. pw2eng
    119. pw2en
    120. fopwdom
    121. enfixsn
    122. 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. onomeneq
    2. onfin
    3. onfin2
    4. nnfi
    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. enfi
    27. enfii
    28. pssnn
    29. ssnnfi
    30. ssfi
    31. domfi
    32. xpfir
    33. ssfid
    34. infi
    35. rabfi
    36. finresfin
    37. f1finf1o
    38. 0fin
    39. nfielex
    40. en1eqsn
    41. en1eqsnbi
    42. diffi
    43. dif1en
    44. enp1ilem
    45. enp1i
    46. en2
    47. en3
    48. en4
    49. findcard
    50. findcard2
    51. findcard2s
    52. findcard2d
    53. findcard3
    54. ac6sfi
    55. frfi
    56. fimax2g
    57. fimaxg
    58. fisupg
    59. wofi
    60. ordunifi
    61. nnunifi
    62. unblem1
    63. unblem2
    64. unblem3
    65. unblem4
    66. unbnn
    67. unbnn2
    68. isfinite2
    69. nnsdomg
    70. isfiniteg
    71. infsdomnn
    72. infn0
    73. fin2inf
    74. unfilem1
    75. unfilem2
    76. unfilem3
    77. unfi
    78. unfir
    79. unfi2
    80. difinf
    81. xpfi
    82. 3xpfi
    83. domunfican
    84. infcntss
    85. prfi
    86. tpfi
    87. fiint
    88. fnfi
    89. fodomfi
    90. fodomfib
    91. fofinf1o
    92. rneqdmfinf1o
    93. fidomdm
    94. dmfi
    95. fundmfibi
    96. resfnfinfin
    97. residfi
    98. cnvfi
    99. rnfi
    100. f1dmvrnfibi
    101. f1vrnfibi
    102. fofi
    103. f1fi
    104. iunfi
    105. unifi
    106. unifi2
    107. infssuni
    108. unirnffid
    109. imafi
    110. pwfilem
    111. pwfi
    112. mapfi
    113. ixpfi
    114. ixpfi2
    115. mptfi
    116. abrexfi
    117. cnvimamptfin
    118. elfpw
    119. unifpw
    120. f1opwfi
    121. fissuni
    122. fipreima
    123. finsschain
    124. 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. fsuppcolem
    33. fsuppco
    34. fsuppco2
    35. fsuppcor
    36. mapfienlem1
    37. mapfienlem2
    38. mapfienlem3
    39. mapfien
    40. mapfien2
    41. sniffsupp
  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