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. finds
   3. findsg
   4. finds2
   5. finds1
   6. findes
7. Relations and functions (cont.)
   1. dmexg
   2. rnexg
   3. dmexd
   4. dmex
   5. rnex
   6. iprc
   7. resiexg
   8. imaexg
   9. imaex
   10. exse2
   11. xpexr
   12. xpexr2
   13. xpexcnv
   14. soex
   15. elxp4
   16. elxp5
   17. cnvexg
   18. cnvex
   19. relcnvexb
   20. f1oexrnex
   21. f1oexbi
   22. coexg
   23. coex
   24. funcnvuni
   25. fun11uni
   26. fex2
   27. fabexg
   28. fabex
   29. dmfex
   30. f1oabexg
   31. fiunlem
   32. fiun
   33. f1iun
   34. fviunfun
   35. ffoss
   36. f11o
   37. resfunexgALT
   38. cofunexg
   39. cofunex2g
   40. fnexALT
   41. funexw
   42. mptexw
   43. funrnex
   44. zfrep6
   45. fornex
   46. f1dmex
   47. f1ovv
   48. fvclex
   49. fvresex
   50. abrexexg
   51. abrexex
   52. iunexg
   53. abrexex2g
   54. opabex3d
   55. opabex3rd
   56. opabex3
   57. iunex
   58. abrexex2
   59. abexssex
   60. abexex
   61. f1oweALT
   62. wemoiso
   63. wemoiso2
   64. oprabexd
   65. oprabex
   66. oprabex3
   67. oprabrexex2
   68. ab2rexex
   69. ab2rexex2
   70. xpexgALT
   71. offval3
   72. offres
   73. ofmres
   74. 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. dmmpog
   87. mpoexxg
   88. mpoexg
   89. mpoexga
   90. mpoexw
   91. mpoex
   92. mptmpoopabbrd
   93. mptmpoopabovd
   94. el2mpocsbcl
   95. el2mpocl
   96. fnmpoovd
   97. offval22
   98. brovpreldm
   99. bropopvvv
   100. bropfvvvvlem
   101. bropfvvvv
   102. ovmptss
   103. relmpoopab
   104. fmpoco
   105. oprabco
   106. oprab2co
   107. df1st2
   108. df2nd2
   109. 1stconst
   110. 2ndconst
   111. dfmpo
   112. mposn
   113. curry1
   114. curry1val
   115. curry1f
   116. curry2
   117. curry2f
   118. curry2val
   119. cnvf1olem
   120. cnvf1o
   121. fparlem1
   122. fparlem2
   123. fparlem3
   124. fparlem4
   125. fpar
   126. fsplit
   127. fsplitOLD
   128. fsplitfpar
   129. offsplitfpar
   130. f2ndf
   131. fo2ndf
   132. f1o2ndf1
   133. algrflem
   134. frxp
   135. xporderlem
   136. poxp
   137. soxp
   138. wexp
   139. fnwelem
   140. fnwe
   141. fnse
   142. fvproj
   143. 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. suppcofnd
   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
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
28. Finite sets
    1. onomeneq
    2. onfin
    3. onfin2
    4. nnfi
    5. nndomo
    6. nnsdomo
    7. sucdom2
    8. sucdom
    9. 0sdom1dom
    10. 1sdom2
    11. sdom1
    12. modom
    13. modom2
    14. 1sdom
    15. unxpdomlem1
    16. unxpdomlem2
    17. unxpdomlem3
    18. unxpdom
    19. unxpdom2
    20. sucxpdom
    21. pssinf
    22. fisseneq
    23. ominf
    24. isinf
    25. fineqvlem
    26. fineqv
    27. enfi
    28. enfii
    29. pssnn
    30. ssnnfi
    31. ssfi
    32. domfi
    33. xpfir
    34. ssfid
    35. infi
    36. rabfi
    37. finresfin
    38. f1finf1o
    39. 0fin
    40. nfielex
    41. en1eqsn
    42. en1eqsnbi
    43. diffi
    44. dif1en
    45. enp1ilem
    46. enp1i
    47. en2
    48. en3
    49. en4
    50. findcard
    51. findcard2
    52. findcard2s
    53. findcard2d
    54. findcard3
    55. ac6sfi
    56. frfi
    57. fimax2g
    58. fimaxg
    59. fisupg
    60. wofi
    61. ordunifi
    62. nnunifi
    63. unblem1
    64. unblem2
    65. unblem3
    66. unblem4
    67. unbnn
    68. unbnn2
    69. isfinite2
    70. nnsdomg
    71. isfiniteg
    72. infsdomnn
    73. infn0
    74. fin2inf
    75. unfilem1
    76. unfilem2
    77. unfilem3
    78. unfi
    79. unfir
    80. unfi2
    81. difinf
    82. xpfi
    83. 3xpfi
    84. domunfican
    85. infcntss
    86. prfi
    87. tpfi
    88. fiint
    89. fnfi
    90. fodomfi
    91. fodomfib
    92. fofinf1o
    93. rneqdmfinf1o
    94. fidomdm
    95. dmfi
    96. fundmfibi
    97. resfnfinfin
    98. residfi
    99. cnvfi
    100. rnfi
    101. f1dmvrnfibi
    102. f1vrnfibi
    103. fofi
    104. f1fi
    105. iunfi
    106. unifi
    107. unifi2
    108. infssuni
    109. unirnffid
    110. imafi
    111. pwfilem
    112. pwfi
    113. mapfi
    114. ixpfi
    115. ixpfi2
    116. mptfi
    117. abrexfi
    118. cnvimamptfin
    119. elfpw
    120. unifpw
    121. f1opwfi
    122. fissuni
    123. fipreima
    124. finsschain
    125. 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, order types, weak dominance
    1. char
    2. cwdom
    3. df-har
    4. df-wdom
    5. harf
    6. harcl
    7. harval
    8. elharval
    9. harndom
    10. harword
    11. relwdom
    12. brwdom
    13. brwdomi
    14. brwdomn0
    15. 0wdom
    16. fowdom
    17. wdomref
    18. brwdom2
    19. domwdom
    20. wdomtr
    21. wdomen1
    22. wdomen2
    23. wdompwdom
    24. canthwdom
    25. wdom2d
    26. wdomd
    27. brwdom3
    28. brwdom3i
    29. unwdomg
    30. xpwdomg
    31. wdomima2g
    32. wdomimag
    33. unxpwdom2
    34. unxpwdom
    35. harwdom
    36. ixpiunwdom