Home | Metamath
Proof ExplorerTheorem List
(p. 41 of 309)
| < 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-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-30843) |

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

Statement | ||

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

Theorem | mpteq2da 4002 | 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 4003* | Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.) |

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

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

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

Theorem | cbvmpt 4007* | 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 4008* | Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |

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

2.1.24 Transitive classes | ||

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

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

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

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

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

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

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

Theorem | trel 4017 | 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 4018 | In a transitive class, the membership relation is transitive. (Contributed by NM, 19-Apr-1994.) |

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

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

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

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

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

Theorem | truni 4024* | 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 4025* | 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 4026 | If is transitive and non-null, then is a subset of . (Contributed by Scott Fenton, 3-Mar-2011.) |

Theorem | trint0 4027 | 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 4028* |
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 5187). 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 1628. Another common variant is derived
as axrep5 4033, where you can find some further remarks. A
slightly more
compact version is shown as axrep2 4030. A quite different variant is
zfrep6 5600, which if used in place of ax-rep 4028 would also require that
the Separation Scheme axsep 4037 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 7445 and the Boundedness Axiom bnd 7446. Many developments of set theory distinguish the uses of Replacement from uses the weaker axioms of Separation axsep 4037, Null Set axnul 4045, and Pairing axpr 4107, 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 4038, ax-nul 4046, and ax-pr 4108 below the theorems that prove them. (Contributed by NM, 23-Dec-1993.) |

Theorem | axrep1 4029* | 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 4028 axrep1 4029 axrep2 4030 axrepnd 8096 zfcndrep 8116 = ax-rep 4028. (Contributed by NM, 19-Nov-2005.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |

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

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

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

Theorem | axrep5 4033* | 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 4034* | An inference rule based on the Axiom of Replacement. Typically, defines a function from to . (Contributed by NM, 26-Nov-1995.) |

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

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

2.2.2 Derive the Axiom of
Separation | ||

Theorem | axsep 4037* |
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 4028. 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 2920. 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 4040, 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 4079 shows (contradicting zfauscl 4040). However, as axsep2 4039 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 4038 from ax-rep 4028. This theorem should not be referenced by any proof. Instead, use ax-sep 4038 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 4038* | The Axiom of Separation of ZF set theory. See axsep 4037 for more information. It was derived as axsep 4037 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 4039* | A less restrictive version of the Separation Scheme axsep 4037, 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 4038 with no additional set theory axioms. (Contributed by NM, 10-Dec-2006.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) |

Theorem | zfauscl 4040* |
Separation Scheme (Aussonderung) using a class variable. To derive this
from ax-sep 4038, we invoke the Axiom of Extensionality
(indirectly via
vtocl 2776), 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 4079 shows. (Contributed by NM, 5-Aug-1993.) |

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

Theorem | ax9vsep 4042* | Derive a weakened version of ax-9 1684 ( i.e. ax-9v 1632), where and must be distinct, from Separation ax-sep 4038 and Extensionality ax-ext 2234. See ax9 1683 for the derivation of ax-9 1684 from ax-9v 1632. (Contributed by NM, 12-Nov-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |

2.2.3 Derive the Null Set Axiom | ||

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

Theorem | axnulALT 4044* | Prove axnul 4045 directly from ax-rep 4028 without using any equality axioms (ax-9 1684 thru ax-16 1926) if we accept ax-4 1692 as an axiom. (Contributed by Jeff Hoffman, 3-Feb-2008.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (Proof modification is discouraged.) |

Theorem | axnul 4045* |
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 4038. 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 4043).
This proof, suggested by Jeff Hoffman (3-Feb-2008), uses only ax-5 1533 and ax-gen 1536 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 4038 implies the existence of at least one set. Note that Kunen's version of ax-sep 4038 (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 4044 for a proof directly from ax-rep 4028. This theorem should not be referenced by any proof. Instead, use ax-nul 4046 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 4046* | The Null Set Axiom of ZF set theory. It was derived as axnul 4045 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 4047 | 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 4046. (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 4048* | No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.) |

Theorem | vprc 4049 | 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 4050 | The universal class doesn't belong to any class. (Contributed by FL, 31-Dec-2006.) |

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

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

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

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

Theorem | ssex 4055 | 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 4038 (a.k.a. Subset Axiom). (Contributed by NM, 27-Apr-1994.) |

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

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

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

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

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

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

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

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

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

Theorem | intex 4065 | 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 4066 | If a class intersection is not a set, it must be the universe. (Contributed by NM, 3-Jul-2005.) |

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

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

Theorem | iinexg 4069* | 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 4070* | Absorption of a redundant conjunct in the intersection of a class abstraction. (Contributed by NM, 3-Jul-2005.) |

Theorem | inuni 4071* | 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 4072* | 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 4073* | Equality theorem based on class2set 4072. (Contributed by NM, 13-Dec-2005.) (Proof shortened by Raph Levien, 30-Jun-2006.) |

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

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

Theorem | 0inp0 4076 | 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 4077 | The removal of the empty set from a class does not affect its union. (Contributed by NM, 22-Mar-2004.) |

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

Theorem | notzfaus 4079* | In the Separation Scheme zfauscl 4040, 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 4080 | The intersection of the universal class is empty. (Contributed by NM, 11-Sep-2008.) |

Theorem | axpweq 4081* | Two equivalent ways to express the Power Set Axiom. Note that ax-pow 4082 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 4082* | 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 4084 uses explicit subset notation. A version using class notation is pwex 4087. (Contributed by NM, 5-Aug-1993.) |

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

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

Theorem | axpow3 4085* | A variant of the Axiom of Power Sets ax-pow 4082. 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 4086* | Every set is an element of some other set. See elALT 4112 for a shorter proof using more axioms. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |

Theorem | pwex 4087 | 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 4088 | 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 4089* | Existence of a class of subsets. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |

Theorem | snexALT 4090 | 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 4106, Replacement is not needed. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) See also snex 4110. (Proof modification is discouraged.) (New usage is discouraged.) |

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

Theorem | p0exALT 4092 | 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 4093 | 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 4094 | The ordinal number 3 is a set, proved without the Axiom of Union ax-un 4403. (Contributed by NM, 2-May-2009.) |

Theorem | dtru 4095* |
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 1821.
This theorem is proved directly from set theory axioms (no set theory definitions) and does not use ax-ext 2234 or ax-sep 4038. See dtruALT 4101 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.) |

Theorem | ax16b 4096* | This theorem shows that axiom ax-16 1926 is redundant in the presence of theorem dtru 4095, which states simply that at least two things exist. This justifies the remark at http://us.metamath.org/mpegif/mmzfcnd.html#twoness (which links to this theorem). (Contributed by NM, 7-Nov-2006.) |

Theorem | eunex 4097 | Existential uniqueness implies there is a value for which the wff argument is false. (Contributed by NM, 24-Oct-2010.) |

Theorem | nfnid 4098 | A set variable is not free from itself. The proof relies on dtru 4095, that is, it is not true in a one-element domain. (Contributed by Mario Carneiro, 8-Oct-2016.) |

Theorem | nfcvb 4099* | The "distinctor" expression , stating that and are not the same variable, can be written in terms of in the obvious way. This theorem is not true in a one-element domain, because then and will both be true. (Contributed by Mario Carneiro, 8-Oct-2016.) |

Theorem | pwuni 4100 | A class is a subclass of the power class of its union. Exercise 6(b) of [Enderton] p. 38. (Contributed by NM, 14-Oct-1996.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |