Home | Metamath
Proof ExplorerTheorem List
(p. 42 of 315)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21490) |
Hilbert Space Explorer
(21491-23013) |
Users' Mathboxes
(23014-31421) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | mpteq1 4101* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |

Theorem | mpteq1d 4102* | An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.) |

Theorem | mpteq2ia 4103 | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |

Theorem | mpteq2i 4104 | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) |

Theorem | mpteq12i 4105 | An equality inference for the maps to notation. (Contributed by Scott Fenton, 27-Oct-2010.) (Revised by Mario Carneiro, 16-Dec-2013.) |

Theorem | mpteq2da 4106 | Slightly more general equality inference for the maps to notation. (Contributed by FL, 14-Sep-2013.) (Revised by Mario Carneiro, 16-Dec-2013.) |

Theorem | mpteq2dva 4107* | Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |

Theorem | mpteq2dv 4108* | An equality inference for the maps to notation. (Contributed by Mario Carneiro, 23-Aug-2014.) |

Theorem | nfmpt 4109* | Bound-variable hypothesis builder for the maps-to notation. (Contributed by NM, 20-Feb-2013.) |

Theorem | nfmpt1 4110 | Bound-variable hypothesis builder for the maps-to notation. (Contributed by FL, 17-Feb-2008.) |

Theorem | cbvmpt 4111* | Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.) |

Theorem | cbvmptv 4112* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |

Theorem | mptv 4113* | Function with universal domain in maps-to notation. (Contributed by NM, 16-Aug-2013.) |

2.1.24 Transitive classes | ||

Syntax | wtr 4114 | Extend wff notation to include transitive classes. Notation from [TakeutiZaring] p. 35. |

Definition | df-tr 4115 | Define the transitive class predicate. Not to be confused with a transitive relation (see cotr 5054). Definition of [Enderton] p. 71 extended to arbitrary classes. For alternate definitions, see dftr2 4116 (which is suggestive of the word "transitive"), dftr3 4118, dftr4 4119, dftr5 4117, and (when is a set) unisuc 4467. The term "complete" is used instead of "transitive" in Definition 3 of [Suppes] p. 130. (Contributed by NM, 29-Aug-1993.) |

Theorem | dftr2 4116* | An alternate way of defining a transitive class. Exercise 7 of [TakeutiZaring] p. 40. (Contributed by NM, 24-Apr-1994.) |

Theorem | dftr5 4117* | An alternate way of defining a transitive class. (Contributed by NM, 20-Mar-2004.) |

Theorem | dftr3 4118* | An alternate way of defining a transitive class. Definition 7.1 of [TakeutiZaring] p. 35. (Contributed by NM, 29-Aug-1993.) |

Theorem | dftr4 4119 | An alternate way of defining a transitive class. Definition of [Enderton] p. 71. (Contributed by NM, 29-Aug-1993.) |

Theorem | treq 4120 | Equality theorem for the transitive class predicate. (Contributed by NM, 17-Sep-1993.) |

Theorem | trel 4121 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |

Theorem | trel3 4122 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |

Theorem | trss 4123 | An element of a transitive class is a subset of the class. (Contributed by NM, 7-Aug-1994.) |

Theorem | trin 4124 | The intersection of transitive classes is transitive. (Contributed by NM, 9-May-1994.) |

Theorem | tr0 4125 | The empty set is transitive. (Contributed by NM, 16-Sep-1993.) |

Theorem | trv 4126 | The universe is transitive. (Contributed by NM, 14-Sep-2003.) |

Theorem | triun 4127* | The indexed union of a class of transitive sets is transitive. (Contributed by Mario Carneiro, 16-Nov-2014.) |

Theorem | truni 4128* | The union of a class of transitive sets is transitive. Exercise 5(a) of [Enderton] p. 73. (Contributed by Scott Fenton, 21-Feb-2011.) (Proof shortened by Mario Carneiro, 26-Apr-2014.) |

Theorem | trint 4129* | The intersection of a class of transitive sets is transitive. Exercise 5(b) of [Enderton] p. 73. (Contributed by Scott Fenton, 25-Feb-2011.) |

Theorem | trintss 4130 | If is transitive and non-null, then is a subset of . (Contributed by Scott Fenton, 3-Mar-2011.) |

Theorem | trint0 4131 | Any non-empty transitive class includes its intersection. Exercise 2 in [TakeutiZaring] p. 44. (Contributed by Andrew Salmon, 14-Nov-2011.) |

2.2 ZF Set Theory - add the Axiom of
Replacement | ||

2.2.1 Introduce the Axiom of
Replacement | ||

Axiom | ax-rep 4132* |
Axiom of Replacement. An axiom scheme of Zermelo-Fraenkel set theory.
Axiom 5 of [TakeutiZaring] p. 19.
It tells us that the image of any set
under a function is also a set (see the variant funimaex 5295). Although
may be
any wff whatsoever, this axiom is useful (i.e. its
antecedent is satisfied) when we are given some function and
encodes the predicate "the value of the function at is ."
Thus
will ordinarily have free variables and -
think
of it informally as . We prefix
with the
quantifier in order to
"protect" the axiom from any
containing , thus
allowing us to eliminate any restrictions on
. This
makes the axiom usable in a formalization that omits the
logically redundant axiom ax-17 1604. Another common variant is derived
as axrep5 4137, where you can find some further remarks. A
slightly more
compact version is shown as axrep2 4134. A quite different variant is
zfrep6 5709, which if used in place of ax-rep 4132 would also require that
the Separation Scheme axsep 4141 be stated as a separate axiom.
There is very a strong generalization of Replacement that doesn't demand function-like behavior of . Two versions of this generalization are called the Collection Principle cp 7556 and the Boundedness Axiom bnd 7557. Many developments of set theory distinguish the uses of Replacement from uses the weaker axioms of Separation axsep 4141, Null Set axnul 4149, and Pairing axpr 4212, all of which we derive from Replacement. In order to make it easier to identify the uses of those redundant axioms, we restate them as axioms ax-sep 4142, ax-nul 4150, and ax-pr 4213 below the theorems that prove them. (Contributed by NM, 23-Dec-1993.) |

Theorem | axrep1 4133* | The version of the Axiom of Replacement used in the Metamath Solitaire applet http://us.metamath.org/mmsolitaire/mms.html. Equivalence is shown via the path ax-rep 4132 axrep1 4133 axrep2 4134 axrepnd 8211 zfcndrep 8231 = ax-rep 4132. (Contributed by NM, 19-Nov-2005.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |

Theorem | axrep2 4134* | Axiom of Replacement expressed with the fewest number of different variables and without any restrictions on . (Contributed by NM, 15-Aug-2003.) |

Theorem | axrep3 4135* | Axiom of Replacement slightly strengthened from axrep2 4134; may occur free in . (Contributed by NM, 2-Jan-1997.) |

Theorem | axrep4 4136* | A more traditional version of the Axiom of Replacement. (Contributed by NM, 14-Aug-1994.) |

Theorem | axrep5 4137* | Axiom of Replacement (similar to Axiom Rep of [BellMachover] p. 463). The antecedent tells us is analogous to a "function" from to (although it is not really a function since it is a wff and not a class). In the consequent we postulate the existence of a set that corresponds to the "image" of restricted to some other set . The hypothesis says must not be free in . (Contributed by NM, 26-Nov-1995.) (Revised by Mario Carneiro, 14-Oct-2016.) |

Theorem | zfrepclf 4138* | An inference rule based on the Axiom of Replacement. Typically, defines a function from to . (Contributed by NM, 26-Nov-1995.) |

Theorem | zfrep3cl 4139* | An inference rule based on the Axiom of Replacement. Typically, defines a function from to . (Contributed by NM, 26-Nov-1995.) |

Theorem | zfrep4 4140* | A version of Replacement using class abstractions. (Contributed by NM, 26-Nov-1995.) |

2.2.2 Derive the Axiom of
Separation | ||

Theorem | axsep 4141* |
Separation Scheme, which is an axiom scheme of Zermelo's original
theory. Scheme Sep of [BellMachover] p. 463. As we show here, it
is
redundant if we assume Replacement in the form of ax-rep 4132. Some
textbooks present Separation as a separate axiom scheme in order to show
that much of set theory can be derived without the stronger
Replacement. The Separation Scheme is a weak form of Frege's Axiom of
Comprehension, conditioning it (with ) so that it
asserts the
existence of a collection only if it is smaller than some other
collection that
already exists. This prevents Russell's paradox
ru 2991. In some texts, this scheme is called
"Aussonderung" or the
Subset Axiom.
The variable
can appear free in the wff , which in
textbooks is often written . To specify this in the
Metamath language, we For a version using a class variable, see zfauscl 4144, which requires the Axiom of Extensionality as well as Replacement for its derivation. If we omit the requirement that not occur in , we can derive a contradiction, as notzfaus 4184 shows (contradicting zfauscl 4144). However, as axsep2 4143 shows, we can eliminate the restriction that not occur in . Note: the distinct variable restriction that not occur in is actually redundant in this particular proof, but we keep it since its purpose is to demonstrate the derivation of the exact ax-sep 4142 from ax-rep 4132. This theorem should not be referenced by any proof. Instead, use ax-sep 4142 below so that the uses of the Axiom of Separation can be more easily identified. (Contributed by NM, 11-Sep-2006.) (New usage is discouraged.) |

Axiom | ax-sep 4142* | The Axiom of Separation of ZF set theory. See axsep 4141 for more information. It was derived as axsep 4141 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 11-Sep-2006.) |

Theorem | axsep2 4143* | A less restrictive version of the Separation Scheme axsep 4141, where variables and can both appear free in the wff , which can therefore be thought of as . This version was derived from the more restrictive ax-sep 4142 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |

Theorem | zfauscl 4144* |
Separation Scheme (Aussonderung) using a class variable. To derive this
from ax-sep 4142, we invoke the Axiom of Extensionality
(indirectly via
vtocl 2839), which is needed for the justification of
class variable
notation.
If we omit the requirement that not occur in , we can derive a contradiction, as notzfaus 4184 shows. (Contributed by NM, 5-Aug-1993.) |

Theorem | bm1.3ii 4145* | Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4142. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.) |

Theorem | ax9vsep 4146* | Derive a weakened version of ax9 1890 ( i.e. ax9v 1638), where and must be distinct, from Separation ax-sep 4142 and Extensionality ax-ext 2265. See ax9 1890 for the derivation of ax9 1890 from ax9v 1638. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |

2.2.3 Derive the Null Set Axiom | ||

Theorem | zfnuleu 4147* | Show the uniqueness of the empty set (using the Axiom of Extensionality via bm1.1 2269 to strengthen the hypothesis in the form of axnul 4149). (Contributed by NM, 22-Dec-2007.) |

Theorem | axnulALT 4148* | Prove axnul 4149 directly from ax-rep 4132 without using any equality axioms (ax9 1890 thru ax-16 2086) if we accept ax4 1717 as an axiom. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (Proof modification is discouraged.) |

Theorem | axnul 4149* |
The Null Set Axiom of ZF set theory: there exists a set with no
elements. Axiom of Empty Set of [Enderton] p. 18. In some textbooks,
this is presented as a separate axiom; here we show it can be derived
from Separation ax-sep 4142. This version of the Null Set Axiom tells us
that at least one empty set exists, but does not tells us that it is
unique - we need the Axiom of Extensionality to do that (see
zfnuleu 4147).
This proof, suggested by Jeff Hoffman (3-Feb-2008), uses only ax-5 1545 and ax-gen 1534 from predicate calculus, which are valid in "free logic" i.e. logic holding in an empty domain (see Axiom A5 and Rule R2 of [LeBlanc] p. 277). Thus our ax-sep 4142 implies the existence of at least one set. Note that Kunen's version of ax-sep 4142 (Axiom 3 of [Kunen] p. 11) does not imply the existence of a set because his is universally closed i.e. prefixed with universal quantifiers to eliminate all free variables. His existence is provided by a separate axiom stating (Axiom 0 of [Kunen] p. 10). See axnulALT 4148 for a proof directly from ax-rep 4132. This theorem should not be referenced by any proof. Instead, use ax-nul 4150 below so that the uses of the Null Set Axiom can be more easily identified. (Contributed by NM, 7-Aug-2003.) (Revised by NM, 4-Feb-2008.) (New usage is discouraged.) |

Axiom | ax-nul 4150* | The Null Set Axiom of ZF set theory. It was derived as axnul 4149 above and is therefore redundant, but we state it as a separate axiom here so that its uses can be identified more easily. (Contributed by NM, 7-Aug-2003.) |

Theorem | 0ex 4151 | The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 4150. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) |

2.2.4 Theorems requiring subset and intersection
existence | ||

Theorem | nalset 4152* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |

Theorem | vprc 4153 | The universal class is not a member of itself (and thus is not a set). Proposition 5.21 of [TakeutiZaring] p. 21; our proof, however, does not depend on the Axiom of Regularity. (Contributed by NM, 23-Aug-1993.) |

Theorem | nvel 4154 | The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.) |

Theorem | vnex 4155 | The universal class does not exist. (Contributed by NM, 4-Jul-2005.) |

Theorem | inex1 4156 | Separation Scheme (Aussonderung) using class notation. Compare Exercise 4 of [TakeutiZaring] p. 22. (Contributed by NM, 5-Aug-1993.) |

Theorem | inex2 4157 | Separation Scheme (Aussonderung) using class notation. (Contributed by NM, 27-Apr-1994.) |

Theorem | inex1g 4158 | Closed-form, generalized Separation Scheme. (Contributed by NM, 7-Apr-1995.) |

Theorem | ssex 4159 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22. This is one way to express the Axiom of Separation ax-sep 4142 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |

Theorem | ssexi 4160 | The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |

Theorem | ssexg 4161 | The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |

Theorem | ssexd 4162 | A subclass of a set is a set. Deduction form of ssexg 4161. (Contributed by David Moews, 1-May-2017.) |

Theorem | difexg 4163 | Existence of a difference. (Contributed by NM, 26-May-1998.) |

Theorem | zfausab 4164* | Separation Scheme (Aussonderung) in terms of a class abstraction. (Contributed by NM, 8-Jun-1994.) |

Theorem | rabexg 4165* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 23-Oct-1999.) |

Theorem | rabex 4166* | Separation Scheme in terms of a restricted class abstraction. (Contributed by NM, 19-Jul-1996.) |

Theorem | elssabg 4167* | Membership in a class abstraction involving a subset. Unlike elabg 2916, does not have to be a set. (Contributed by NM, 29-Aug-2006.) |

Theorem | elpw2g 4168 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 7-Aug-2000.) |

Theorem | elpw2 4169 | Membership in a power class. Theorem 86 of [Suppes] p. 47. (Contributed by NM, 11-Oct-2007.) |

Theorem | intex 4170 | The intersection of a non-empty class exists. Exercise 5 of [TakeutiZaring] p. 44 and its converse. (Contributed by NM, 13-Aug-2002.) |

Theorem | intnex 4171 | If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005.) |

Theorem | intexab 4172 | The intersection of a non-empty class abstraction exists. (Contributed by NM, 21-Oct-2003.) |

Theorem | intexrab 4173 | The intersection of a non-empty restricted class abstraction exists. (Contributed by NM, 21-Oct-2003.) |

Theorem | iinexg 4174* | The existence of an indexed union. is normally a free-variable parameter in , which should be read . (Contributed by FL, 19-Sep-2011.) |

Theorem | intabs 4175* | Absorption of a redundant conjunct in the intersection of a class abstraction. (Contributed by NM, 3-Jul-2005.) |

Theorem | inuni 4176* | The intersection of a union with a class is equal to the union of the intersections of each element of with . (Contributed by FL, 24-Mar-2007.) |

2.2.5 Theorems requiring empty set
existence | ||

Theorem | class2set 4177* | Construct, from any class , a set equal to it when the class exists and equal to the empty set when the class is proper. This theorem shows that the constructed set always exists. (Contributed by NM, 16-Oct-2003.) |

Theorem | class2seteq 4178* | Equality theorem based on class2set 4177. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |

Theorem | 0elpw 4179 | Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.) |

Theorem | 0nep0 4180 | The empty set and its power set are not equal. (Contributed by NM, 23-Dec-1993.) |

Theorem | 0inp0 4181 | Something cannot be equal to both the null set and the power set of the null set. (Contributed by NM, 30-Sep-2003.) |

Theorem | unidif0 4182 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |

Theorem | iin0 4183* | An indexed intersection of the empty set, with a non-empty index set, is empty. (Contributed by NM, 20-Oct-2005.) |

Theorem | notzfaus 4184* | In the Separation Scheme zfauscl 4144, we require that not occur in (which can be generalized to "not be free in"). Here we show special cases of and that result in a contradiction by violating this requirement. (Contributed by NM, 8-Feb-2006.) |

Theorem | intv 4185 | The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.) |

Theorem | axpweq 4186* | Two equivalent ways to express the Power Set Axiom. Note that ax-pow 4187 is not used by the proof. (Contributed by NM, 22-Jun-2009.) |

2.3 ZF Set Theory - add the Axiom of Power
Sets | ||

2.3.1 Introduce the Axiom of Power
Sets | ||

Axiom | ax-pow 4187* | Axiom of Power Sets. An axiom of Zermelo-Fraenkel set theory. It states that a set exists that includes the power set of a given set i.e. contains every subset of . The variant axpow2 4189 uses explicit subset notation. A version using class notation is pwex 4192. (Contributed by NM, 5-Aug-1993.) |

Theorem | zfpow 4188* | Axiom of Power Sets expressed with fewest number of different variables. (Contributed by NM, 14-Aug-2003.) |

Theorem | axpow2 4189* | A variant of the Axiom of Power Sets ax-pow 4187 using subset notation. Problem in {BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |

Theorem | axpow3 4190* | A variant of the Axiom of Power Sets ax-pow 4187. For any set , there exists a set whose members are exactly the subsets of i.e. the power set of . Axiom Pow of [BellMachover] p. 466. (Contributed by NM, 4-Jun-2006.) |

Theorem | el 4191* | Every set is an element of some other set. See elALT 4217 for a shorter proof using more axioms. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |

Theorem | pwex 4192 | Power set axiom expressed in class notation. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |

Theorem | pwexg 4193 | Power set axiom expressed in class notation, with the sethood requirement as an antecedent. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) |

Theorem | abssexg 4194* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |

Theorem | snexALT 4195 | A singleton is a set. Theorem 7.13 of [Quine] p. 51, but proved using only Extensionality, Power Set, and Separation. Unlike the proof of zfpair 4211, Replacement is not needed. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) See also snex 4215. (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | p0ex 4196 | The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.) |

Theorem | p0exALT 4197 | The power set of the empty set (the ordinal 1) is a set. Alternate proof. (Contributed by NM, 23-Dec-1993.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | pp0ex 4198 | The power set of the power set of the empty set (the ordinal 2) is a set. (Contributed by NM, 5-Aug-1993.) |

Theorem | ord3ex 4199 | The ordinal number 3 is a set, proved without the Axiom of Union ax-un 4511. (Contributed by NM, 2-May-2009.) |

Theorem | dtru 4200* |
At least two sets exist (or in terms of first-order logic, the universe
of discourse has two or more objects). Note that we may not substitute
the same variable for both and (as
indicated by the distinct
variable requirement), for otherwise we would contradict stdpc6 1651.
This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2265 or ax-sep 4142. See dtruALT 4206 for a shorter proof using these axioms. The proof makes use of dummy variables and which do not appear in the final theorem. They must be distinct from each other and from and . In other words, if we were to substitute for throughout the proof, the proof would fail. Although this requirement is made explicitly in the set.mm source file, it is implicit on the web page (i.e. doesn't appear in the "Distinct variable group"). (Contributed by NM, 7-Nov-2006.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |