Metamath Proof Explorer

Table of Contents - 2.4. ZF Set Theory - add the Axiom of Union

Introduce the Axiom of Union
1. ax-un
2. zfun
3. axun2
4. uniex2
5. uniex2OLD
6. vuniex
7. uniexg
8. uniex
9. uniexd
10. unexg
11. unex
12. unexOLD
13. tpex
14. unexb
15. unexbOLD
16. unexgOLD
17. xpexg
18. xpexd
19. 3xpexg
20. xpex
21. unexd
22. sqxpexg
23. abnexg
24. abnex
25. snnex
26. pwnex
27. difex2
28. difsnexi
29. uniuni
30. uniexr
31. uniexb
32. pwexr
33. pwexb
34. elpwpwel
35. eldifpw
36. elpwun
37. pwuncl
38. iunpw
39. fr3nr
40. epne3
41. dfwe2
Ordinals (continued)
1. epweon
2. epweonALT
3. ordon
4. onprc
5. ssorduni
6. ssonuni
7. ssonunii
8. ordeleqon
9. ordsson
10. dford5
11. onss
12. predon
13. ssonprc
14. onuni
15. orduni
16. onint
17. onint0
18. onssmin
19. onminesb
20. onminsb
21. oninton
22. onintrab
23. onintrab2
24. onnmin
25. onnminsb
26. oneqmin
27. uniordint
28. onminex
29. sucon
30. sucexb
31. sucexg
32. sucex
33. onmindif2
34. ordsuci
35. sucexeloni
36. onsuc
37. ordsuc
38. ordpwsuc
39. onpwsuc
40. onsucb
41. ordsucss
42. onpsssuc
43. ordelsuc
44. onsucmin
45. ordsucelsuc
46. ordsucsssuc
47. ordsucuniel
48. ordsucun
49. ordunpr
50. ordunel
51. onsucuni
52. ordsucuni
53. orduniorsuc
54. unon
55. ordunisuc
56. orduniss2
57. onsucuni2
58. 0elsuc
59. limon
60. onuniorsuc
61. onssi
62. onsuci
63. onuninsuci
64. onsucssi
65. nlimsucg
66. orduninsuc
67. ordunisuc2
68. ordzsl
69. onzsl
70. dflim3
71. dflim4
72. limsuc
73. limsssuc
74. nlimon
75. limuni3
Transfinite induction
1. tfi
2. tfisg
3. tfis
4. tfis2f
5. tfis2
6. tfis3
7. tfisi
8. tfinds
9. tfindsg
10. tfindsg2
11. tfindes
12. tfinds2
13. tfinds3
The natural numbers (i.e., finite ordinals)
1. com
2. df-om
3. dfom2
4. elom
5. omsson
6. limomss
7. nnon
8. nnoni
9. nnord
10. trom
11. ordom
12. elnn
13. omon
14. omelon2
15. nnlim
16. omssnlim
17. limom
18. peano2b
19. nnsuc
20. omsucne
21. ssnlim
22. omsinds
23. omun
Peano's postulates
1. peano1
2. peano2
3. peano3
4. peano3OLD
5. peano4
6. peano5
7. nn0suc
Finite induction (for finite ordinals)
1. find
2. finds
3. findsg
4. finds2
5. finds1
6. findes
Relations and functions (cont.)
1. dmexg
2. rnexg
3. dmexd
4. fndmexd
5. dmfex
6. fndmexb
7. fdmexb
8. dmfexALT
9. dmex
10. rnex
11. iprc
12. resiexg
13. imaexg
14. imaex
15. rnexd
16. imaexd
17. exse2
18. xpexr
19. xpexr2
20. xpexcnv
21. soex
22. elxp4
23. elxp5
24. cnvexg
25. cnvex
26. relcnvexb
27. f1oexrnex
28. f1oexbi
29. coexg
30. coex
31. coexd
32. funcnvuni
33. fun11uni
34. resf1extb
35. resf1ext2b
36. fex2
37. fabexd
38. fabexg
39. fabex
40. mapex
41. f1oabexg
42. fiunlem
43. fiun
44. f1iun
45. fviunfun
46. ffoss
47. f11o
48. resfunexgALT
49. cofunexg
50. cofunex2g
51. fnexALT
52. funexw
53. mptexw
54. funrnex
55. zfrep6OLD
56. focdmex
57. f1dmex
58. f1ovv
59. fvclex
60. fvresex
61. abrexexg
62. abrexex
63. iunexg
64. abrexex2g
65. opabex3d
66. opabex3rd
67. opabex3
68. iunex
69. abrexex2
70. abexssex
71. abexex
72. f1oweALT
73. wemoiso
74. wemoiso2
75. oprabexd
76. oprabex
77. oprabex3
78. oprabrexex2
79. ab2rexex
80. ab2rexex2
81. xpexgALT
82. offval3
83. offres
84. ofmres
85. ofmresex
86. mptcnfimad
First and second members of an ordered pair
1. c1st
2. c2nd
3. df-1st
4. df-2nd
5. 1stval
6. 2ndval
7. 1stnpr
8. 2ndnpr
9. 1st0
10. 2nd0
11. op1st
12. op2nd
13. op1std
14. op2ndd
15. op1stg
16. op2ndg
17. ot1stg
18. ot2ndg
19. ot3rdg
20. 1stval2
21. 2ndval2
22. oteqimp
23. fo1st
24. fo2nd
25. br1steqg
26. br2ndeqg
27. f1stres
28. f2ndres
29. fo1stres
30. fo2ndres
31. 1st2val
32. 2nd2val
33. 1stcof
34. 2ndcof
35. xp1st
36. xp2nd
37. elxp6
38. elxp7
39. eqopi
40. xp2
41. unielxp
42. 1st2nd2
43. 1st2ndb
44. xpopth
45. eqop
46. eqop2
47. op1steq
48. opreuopreu
49. el2xptp
50. el2xptp0
51. el2xpss
52. 2nd1st
53. 1st2nd
54. 1stdm
55. 2ndrn
56. 1st2ndbr
57. releldm2
58. reldm
59. releldmdifi
60. funfv1st2nd
61. funelss
62. funeldmdif
63. sbcopeq1a
64. csbopeq1a
65. sbcoteq1a
66. dfopab2
67. dfoprab3s
68. dfoprab3
69. dfoprab4
70. dfoprab4f
71. opabex2
72. opabn1stprc
73. opiota
74. cnvoprab
75. dfxp3
76. elopabi
77. eloprabi
78. mpomptsx
79. mpompts
80. dmmpossx
81. fmpox
82. fmpo
83. fnmpo
84. fnmpoi
85. dmmpo
86. ovmpoelrn
87. dmmpoga
88. dmmpog
89. mpoexxg
90. mpoexg
91. mpoexga
92. mpoexw
93. mpoex
94. mpoexd
95. mptmpoopabbrd
96. mptmpoopabovd
97. el2mpocsbcl
98. el2mpocl
99. fnmpoovd
100. offval22
101. brovpreldm
102. bropopvvv
103. bropfvvvvlem
104. bropfvvvv
105. ovmptss
106. relmpoopab
107. fmpoco
108. oprabco
109. oprab2co
110. df1st2
111. df2nd2
112. 1stconst
113. 2ndconst
114. dfmpo
115. mposn
116. curry1
117. curry1val
118. curry1f
119. curry2
120. curry2f
121. curry2val
122. cnvf1olem
123. cnvf1o
124. fparlem1
125. fparlem2
126. fparlem3
127. fparlem4
128. fpar
129. fsplit
130. fsplitfpar
131. offsplitfpar
132. f2ndf
133. fo2ndf
134. f1o2ndf1
135. opco1
136. opco2
137. opco1i
138. mpof1o2d
139. frxp
140. xporderlem
141. poxp
142. soxp
143. wexp
144. fnwelem
145. fnwe
146. fnse
147. fvproj
148. fimaproj
149. ralxpes
150. ralxp3f
151. ralxp3
152. ralxp3es
Induction on Cartesian products
1. frpoins3xpg
2. frpoins3xp3g
Ordering on Cartesian products
1. xpord2lem
2. poxp2
3. frxp2
4. xpord2pred
5. sexp2
6. xpord2indlem
7. xpord2ind
8. xpord3lem
9. poxp3
10. frxp3
11. xpord3pred
12. sexp3
13. xpord3inddlem
14. xpord3indd
15. xpord3ind
Ordering Ordinal Sequences
1. orderseqlem
2. poseq
3. soseq
The support of functions
1. csupp
2. df-supp
3. suppval
4. supp0prc
5. suppvalbr
6. supp0
7. suppval1
8. suppvalfng
9. suppvalfn
10. elsuppfng
11. elsuppfn
12. fvdifsupp
13. cnvimadfsn
14. suppimacnvss
15. suppimacnv
16. fsuppeq
17. fsuppeqg
18. suppssdm
19. suppsnop
20. snopsuppss
21. fvn0elsupp
22. fvn0elsuppb
23. rexsupp
24. ressuppss
25. suppun
26. ressuppssdif
27. mptsuppdifd
28. mptsuppd
29. extmptsuppeq
30. suppfnss
31. funsssuppss
32. fnsuppres
33. fnsuppeq0
34. fczsupp0
35. suppss
36. suppssr
37. suppssrg
38. suppssov1
39. suppssov2
40. suppssof1
41. suppss2
42. suppsssn
43. suppssfv
44. suppofssd
45. suppofss1d
46. suppofss2d
47. suppco
48. suppcoss
49. supp0cosupp0
50. imacosupp
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
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
Curry and uncurry
1. ccur
2. cunc
3. df-cur
4. df-unc
5. mpocurryd
6. mpocurryvald
7. fvmpocurryd
Undefined values
1. cund
2. df-undef
3. pwuninel2
4. pwuninel
5. pwuninelOLD
6. undefval
7. undefnel2
8. undefnel
9. undefne0
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
Well-ordered recursion
1. cwrecs
2. df-wrecs
3. wrecseq123
4. nfwrecs
5. wrecseq1
6. wrecseq2
7. wrecseq3
8. csbwrecsg
9. wfr3g
10. wfrrel
11. wfrdmss
12. wfrdmcl
13. wfrfun
14. wfrresex
15. wfr2a
16. wfr1
17. wfr2
18. wfr3
Functions on ordinals; strictly monotone ordinal functions
1. iunon
2. iinon
3. onfununi
4. onovuni
5. onoviun
6. onnseq
7. wsmo
8. df-smo
9. dfsmo2
10. issmo
11. issmo2
12. smoeq
13. smodm
14. smores
15. smores3
16. smores2
17. smodm2
18. smofvon2
19. iordsmo
20. smo0
21. smofvon
22. smoel
23. smoiun
24. smoiso
25. smoel2
26. smo11
27. smoord
28. smoword
29. smogt
30. smocdmdom
31. smoiso2
"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. tfrlem6OLD
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
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
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
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. 1oelpr
20. 2oex
21. 1on
22. 2on
23. 2on0
24. ord3
25. 3on
26. 4on
27. 1n0
28. 1n0OLD
29. nlim1
30. nlim2
31. xp01disj
32. xp01disjl
33. ordgt0ge1
34. ordge1n0
35. el1o
36. ord1eln01
37. ord2eln012
38. 1ellim
39. 2ellim
40. dif1o
41. ondif1
42. ondif2
43. 2oconcl
44. 0lt1o
45. dif20el
46. 0we1
47. brwitnlem
48. fnoa
49. fnom
50. fnoe
51. oav
52. omv
53. oe0lem
54. oev
55. oevn0
56. oa0
57. om0
58. oe0m
59. om0x
60. oe0m0
61. oe0m1
62. oe0
63. oev2
64. oasuc
65. oesuclem
66. omsuc
67. oesuc
68. onasuc
69. onmsuc
70. onesuc
71. oa1suc
72. oalim
73. omlim
74. oelim
75. oacl
76. omcl
77. oecl
78. oa0r
79. om0r
80. o1p1e2
81. o2p2e4
82. om1
83. om1r
84. oe1
85. oe1m
86. oaordi
87. oaord
88. oacan
89. oaword
90. oawordri
91. oaord1
92. oaword1
93. oaword2
94. oawordeulem
95. oawordeu
96. oawordexr
97. oawordex
98. oaordex
99. oa00
100. oalimcl
101. oaass
102. oarec
103. oaf1o
104. oacomf1olem
105. oacomf1o
106. omordi
107. omord2
108. omord
109. omcan
110. omword
111. omwordi
112. omwordri
113. omword1
114. omword2
115. om00
116. om00el
117. omordlim
118. omlimcl
119. odi
120. omass
121. oneo
122. omeulem1
123. omeulem2
124. omopth2
125. omeu
126. om2
127. oen0
128. oeordi
129. oeord
130. oecan
131. oeword
132. oewordi
133. oewordri
134. oeworde
135. oeordsuc
136. oelim2
137. oeoalem
138. oeoa
139. oeoelem
140. oeoe
141. oelimcl
142. oeeulem
143. oeeui
144. oeeu
Natural number arithmetic
1. nna0
2. nnm0
3. nnasuc
4. nnmsuc
5. nnesuc
6. nna0r
7. nnm0r
8. nnacl
9. nnmcl
10. nnecl
11. nnacli
12. nnmcli
13. nnarcl
14. nnacom
15. nnaordi
16. nnaord
17. nnaordr
18. nnawordi
19. nnaass
20. nndi
21. nnmass
22. nnmsucr
23. nnmcom
24. nnaword
25. nnacan
26. nnaword1
27. nnaword2
28. nnmordi
29. nnmord
30. nnmword
31. nnmcan
32. nnmwordi
33. nnmwordri
34. nnawordex
35. nnaordex
36. nnaordex2
37. 1onn
38. 1onnALT
39. 2onn
40. 2onnALT
41. 3onn
42. 4onn
43. 1one2o
44. oaabslem
45. oaabs
46. oaabs2
47. omabslem
48. omabs
49. nnm1
50. nnm2
51. nn2m
52. nnneo
53. nneob
54. omsmolem
55. omsmo
56. omopthlem1
57. omopthlem2
58. omopthi
59. omopth
60. nnasmo
61. eldifsucnn
Natural addition
1. cnadd
2. df-nadd
3. on2recsfn
4. on2recsov
5. on2ind
6. on3ind
7. coflton
8. cofon1
9. cofon2
10. cofonr
11. naddfn
12. naddcllem
13. naddcl
14. naddov
15. naddov2
16. naddcld
17. naddov3
18. naddf
19. naddcom
20. naddrid
21. naddlid
22. naddssim
23. naddelim
24. naddel1
25. naddel2
26. naddss1
27. naddss2
28. naddword1
29. naddword2
30. naddunif
31. naddasslem1
32. naddasslem2
33. naddass
34. nadd32
35. nadd4
36. nadd42
37. naddel12
38. naddsuc2
39. naddoa
40. omnaddcl
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. dfqs2
12. ereq1
13. ereq2
14. errel
15. erdm
16. ercl
17. ersym
18. ercl2
19. ersymb
20. ertr
21. ertrd
22. ertr2d
23. ertr3d
24. ertr4d
25. erref
26. ercnv
27. errn
28. erssxp
29. erex
30. erexb
31. iserd
32. iseri
33. iseriALT
34. brinxper
35. brdifun
36. swoer
37. swoord1
38. swoord2
39. swoso
40. eqerlem
41. eqer
42. ider
43. 0er
44. eceq1
45. eceq1d
46. eceq2
47. eceq2i
48. eceq2d
49. elecg
50. ecref
51. elec
52. relelec
53. elecres
54. elecreseq
55. elecex
56. ecss
57. ecdmn0
58. ereldm
59. erth
60. erth2
61. erthi
62. erdisj
63. ecidsn
64. qseq1
65. qseq2
66. qseq2i
67. qseq1d
68. qseq2d
69. qseq12
70. 0qs
71. elqsg
72. elqs
73. elqsi
74. elqsecl
75. ecelqs
76. ecelqsw
77. ecelqsi
78. ecopqsi
79. qsexg
80. qsex
81. uniqs
82. uniqsw
83. qsss
84. uniqs2
85. snecg
86. snec
87. ecqs
88. ecid
89. qsid
90. ectocld
91. ectocl
92. elqsn0
93. ecelqsdm
94. ecelqsdmb
95. eceldmqs
96. xpider
97. iiner
98. riiner
99. erinxp
100. ecinxp
101. qsinxp
102. qsdisj
103. qsdisj2
104. qsel
105. uniinqs
106. qliftlem
107. qliftrel
108. qliftel
109. qliftel1
110. qliftfun
111. qliftfund
112. qliftfuns
113. qliftf
114. qliftval
115. ecoptocl
116. 2ecoptocl
117. 3ecoptocl
118. brecop
119. brecop2
120. eroveu
121. erovlem
122. erov
123. eroprf
124. erov2
125. eroprf2
126. ecopoveq
127. ecopovsym
128. ecopovtrn
129. ecopover
130. eceqoveq
131. ecovcom
132. ecovass
133. ecovdi
The mapping operation
1. cmap
2. cpm
3. df-map
4. df-pm
5. mapprc
6. pmex
7. fnmap
8. fnpm
9. reldmmap
10. mapvalg
11. pmvalg
12. mapval
13. elmapg
14. elmapd
15. elmapdd
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. elmapssresd
43. fpmg
44. pmss12g
45. pmresg
46. elmap
47. mapval2
48. elpm
49. elpm2
50. fpm
51. mapsspm
52. pmsspw
53. mapsspw
54. mapfvd
55. elmapresaun
56. fvmptmap
57. map0e
58. map0b
59. map0g
60. 0map0sn0
61. mapsnd
62. map0
63. mapsn
64. mapss
65. fdiagfn
66. fvdiagfn
67. mapsnconst
68. mapsncnv
69. mapsnf1o2
70. mapsnf1o3
71. ralxpmap
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
Equinumerosity
1. cen
2. cdom
3. csdm
4. cfn
5. df-en
6. df-dom
7. df-sdom
8. df-fin
9. relen
10. reldom
11. relsdom
12. encv
13. breng
14. bren
15. brdom2g
16. brdomg
17. brdomi
18. brdom
19. domen
20. domeng
21. ctex
22. f1oen4g
23. f1dom4g
24. f1oen3g
25. f1dom3g
26. f1oen2g
27. f1dom2g
28. f1oeng
29. f1domg
30. f1oen
31. f1dom
32. brsdom
33. isfi
34. enssdom
35. enssdomOLD
36. dfdom2
37. endom
38. sdomdom
39. sdomnen
40. brdom2
41. bren2
42. enrefg
43. enref
44. eqeng
45. domrefg
46. en2d
47. en3d
48. en2i
49. en3i
50. dom2lem
51. dom2d
52. dom3d
53. dom2
54. dom3
55. idssen
56. domssl
57. domssr
58. ssdomg
59. ener
60. ensymb
61. ensym
62. ensymi
63. ensymd
64. entr
65. domtr
66. entri
67. entr2i
68. entr3i
69. entr4i
70. endomtr
71. domentr
72. f1imaeng
73. f1imaen2g
74. f1imaen3g
75. f1imaen
76. en0
77. en0ALT
78. en0r
79. ensn1
80. ensn1g
81. enpr1g
82. en1
83. en1b
84. reuen1
85. euen1
86. euen1b
87. en1uniel
88. 2dom
89. fundmen
90. fundmeng
91. cnven
92. cnvct
93. fndmeng
94. mapsnend
95. mapsnen
96. snmapen
97. snmapen1
98. map1
99. en2sn
100. 0fi
101. snfi
102. fiprc
103. unen
104. enrefnn
105. en2prd
106. enpr2d
107. ssct
108. difsnen
109. domdifsn
110. xpsnen
111. xpsneng
112. xp1en
113. endisj
114. undom
115. xpcomf1o
116. xpcomco
117. xpcomen
118. xpcomeng
119. xpsnen2g
120. xpassen
121. xpdom2
122. xpdom2g
123. xpdom1g
124. xpdom3
125. xpdom1
126. domunsncan
127. omxpenlem
128. omxpen
129. omf1o
130. pw2f1olem
131. pw2f1o
132. pw2eng
133. pw2en
134. fopwdom
135. enfixsn
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
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
Finite sets
1. dif1enlem
2. rexdif1en
3. dif1en
4. dif1ennn
5. findcard
6. findcard2
7. findcard2s
8. findcard2d
9. nnfi
10. pssnn
11. ssnnfi
12. unfi
13. unfid
14. ssfi
15. ssfiALT
16. diffi
17. cnvfi
18. pwssfi
19. fnfi
20. f1oenfi
21. f1oenfirn
22. f1domfi
23. f1domfi2
24. enreffi
25. ensymfib
26. entrfil
27. enfii
28. enfi
29. enfiALT
30. domfi
31. entrfi
32. entrfir
33. domtrfil
34. domtrfi
35. domtrfir
36. f1imaenfi
37. ssdomfi
38. ssdomfi2
39. sbthfilem
40. sbthfi
41. domnsymfi
42. sdomdomtrfi
43. domsdomtrfi
44. sucdom2
Pigeonhole Principle
1. phplem1
2. phplem2
3. nneneq
4. php
5. php2
6. php3
7. php4
8. php5
9. phpeqd
10. nndomog
Finite sets (cont.)
1. onomeneq
2. onfin
3. ordfin
4. onfin2
5. nndomo
6. nnsdomo
7. sucdom
8. snnen2o
9. 0sdom1dom
10. 0sdom1domALT
11. 1sdom2
12. 1sdom2ALT
13. sdom1
14. modom
15. modom2
16. rex2dom
17. 1sdom2dom
18. 1sdom
19. unxpdomlem1
20. unxpdomlem2
21. unxpdomlem3
22. unxpdom
23. unxpdom2
24. sucxpdom
25. pssinf
26. fisseneq
27. ominf
28. isinf
29. fineqvlem
30. fineqv
31. xpfir
32. ssfid
33. infi
34. rabfi
35. finresfin
36. f1finf1o
37. nfielex
38. en1eqsn
39. en1eqsnbi
40. dif1ennnALT
41. enp1ilem
42. enp1i
43. en2
44. en3
45. en4
46. findcard3
47. ac6sfi
48. frfi
49. fimax2g
50. fimaxg
51. fisupg
52. wofi
53. ordunifi
54. nnunifi
55. unblem1
56. unblem2
57. unblem3
58. unblem4
59. unbnn
60. unbnn2
61. isfinite2
62. nnsdomg
63. isfiniteg
64. infsdomnn
65. infn0
66. infn0ALT
67. fin2inf
68. unfilem1
69. unfilem2
70. unfilem3
71. unfir
72. unfib
73. unfi2
74. difinf
75. fodomfi
76. fofi
77. f1fi
78. imafi
79. pwfir
80. pwfilem
81. pwfi
82. xpfi
83. 3xpfi
84. domunfican
85. infcntss
86. prfi
87. prfiALT
88. tpfi
89. fiint
90. fodomfir
91. fodomfib
92. fofinf1o
93. rneqdmfinf1o
94. fidomdm
95. dmfi
96. fundmfibi
97. resfnfinfin
98. residfi
99. cnvfiALT
100. rnfi
101. f1dmvrnfibi
102. f1vrnfibi
103. iunfi
104. unifi
105. unifi2
106. infssuni
107. unirnffid
108. mapfi
109. ixpfi
110. ixpfi2
111. mptfi
112. abrexfi
113. cnvimamptfin
114. elfpw
115. unifpw
116. f1opwfi
117. fissuni
118. fipreima
119. finsschain
120. indexfi
121. imafi2
122. unifi3
123. tfsnfin2
Finitely supported functions
1. cfsupp
2. df-fsupp
3. relfsupp
4. relprcnfsupp
5. isfsupp
6. isfsuppd
7. funisfsupp
8. fsuppimp
9. fsuppimpd
10. fsuppfund
11. fisuppfi
12. fidmfisupp
13. finnzfsuppd
14. fdmfisuppfi
15. fdmfifsupp
16. fsuppmptdm
17. fndmfisuppfi
18. fndmfifsupp
19. suppeqfsuppbi
20. suppssfifsupp
21. fsuppsssupp
22. fsuppsssuppgd
23. fsuppss
24. fsuppssov1
25. fsuppxpfi
26. fczfsuppd
27. fsuppun
28. fsuppunfi
29. fsuppunbi
30. 0fsupp
31. snopfsupp
32. funsnfsupp
33. fsuppres
34. fmptssfisupp
35. ressuppfi
36. resfsupp
37. resfifsupp
38. ffsuppbi
39. fsuppmptif
40. sniffsupp
41. fsuppcolem
42. fsuppco
43. fsuppco2
44. fsuppcor
45. mapfienlem1
46. mapfienlem2
47. mapfienlem3
48. mapfien
49. mapfien2
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
Hall's marriage theorem
1. marypha1lem
2. marypha1
3. marypha2lem1
4. marypha2lem2
5. marypha2lem3
6. marypha2lem4
7. marypha2
Supremum and infimum
1. csup
2. cinf
3. df-sup
4. df-inf
5. dfsup2
6. supeq1
7. supeq1d
8. supeq1i
9. supeq2
10. supeq3
11. supeq123d
12. nfsup
13. supmo
14. supexd
15. supeu
16. supval2
17. eqsup
18. eqsupd
19. supcl
20. supub
21. suplub
22. suplub2
23. supnub
24. supssd
25. supex
26. sup00
27. sup0riota
28. sup0
29. supmax
30. fisup2g
31. fisupcl
32. supgtoreq
33. suppr
34. supsn
35. supisolem
36. supisoex
37. supiso
38. infeq1
39. infeq1d
40. infeq1i
41. infeq2
42. infeq3
43. infeq123d
44. nfinf
45. infexd
46. eqinf
47. eqinfd
48. infval
49. infcllem
50. infcl
51. inflb
52. infglb
53. infglbb
54. infnlb
55. infssd
56. infex
57. infmin
58. infmo
59. infeu
60. fimin2g
61. fiming
62. fiinfg
63. fiinf2g
64. fiinfcl
65. infltoreq
66. infpr
67. infsupprpr
68. infsn
69. inf00
70. infempty
71. infiso
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
Hartogs function
1. char
2. df-har
3. harf
4. harcl
5. harval
6. elharval
7. harndom
8. harword
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