Theorem List for Intuitionistic Logic Explorer - 4101-4200 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
2.3.3 Axiom of Pairing
|
|
Axiom | ax-pr 4101* |
The Axiom of Pairing of IZF set theory. Axiom 2 of [Crosilla] p.
"Axioms of CZF and IZF", except (a) unnecessary quantifiers
are removed,
and (b) Crosilla has a biconditional rather than an implication (but the
two are equivalent by bm1.3ii 4019). (Contributed by NM, 14-Nov-2006.)
|
|
|
Theorem | zfpair2 4102 |
Derive the abbreviated version of the Axiom of Pairing from ax-pr 4101.
(Contributed by NM, 14-Nov-2006.)
|
|
|
Theorem | prexg 4103 |
The Axiom of Pairing using class variables. Theorem 7.13 of [Quine]
p. 51, but restricted to classes which exist. For proper classes, see
prprc 3603, prprc1 3601, and prprc2 3602. (Contributed by Jim Kingdon,
16-Sep-2018.)
|
|
|
Theorem | snelpwi 4104 |
A singleton of a set belongs to the power class of a class containing the
set. (Contributed by Alan Sare, 25-Aug-2011.)
|
|
|
Theorem | snelpw 4105 |
A singleton of a set belongs to the power class of a class containing
the set. (Contributed by NM, 1-Apr-1998.)
|
|
|
Theorem | prelpwi 4106 |
A pair of two sets belongs to the power class of a class containing those
two sets. (Contributed by Thierry Arnoux, 10-Mar-2017.)
|
|
|
Theorem | rext 4107* |
A theorem similar to extensionality, requiring the existence of a
singleton. Exercise 8 of [TakeutiZaring] p. 16. (Contributed by NM,
10-Aug-1993.)
|
|
|
Theorem | sspwb 4108 |
Classes are subclasses if and only if their power classes are
subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM,
13-Oct-1996.)
|
|
|
Theorem | unipw 4109 |
A class equals the union of its power class. Exercise 6(a) of
[Enderton] p. 38. (Contributed by NM,
14-Oct-1996.) (Proof shortened
by Alan Sare, 28-Dec-2008.)
|
|
|
Theorem | pwel 4110 |
Membership of a power class. Exercise 10 of [Enderton] p. 26.
(Contributed by NM, 13-Jan-2007.)
|
|
|
Theorem | pwtr 4111 |
A class is transitive iff its power class is transitive. (Contributed by
Alan Sare, 25-Aug-2011.) (Revised by Mario Carneiro, 15-Jun-2014.)
|
|
|
Theorem | ssextss 4112* |
An extensionality-like principle defining subclass in terms of subsets.
(Contributed by NM, 30-Jun-2004.)
|
|
|
Theorem | ssext 4113* |
An extensionality-like principle that uses the subset instead of the
membership relation: two classes are equal iff they have the same
subsets. (Contributed by NM, 30-Jun-2004.)
|
|
|
Theorem | nssssr 4114* |
Negation of subclass relationship. Compare nssr 3127.
(Contributed by
Jim Kingdon, 17-Sep-2018.)
|
|
|
Theorem | pweqb 4115 |
Classes are equal if and only if their power classes are equal. Exercise
19 of [TakeutiZaring] p. 18.
(Contributed by NM, 13-Oct-1996.)
|
|
|
Theorem | intid 4116* |
The intersection of all sets to which a set belongs is the singleton of
that set. (Contributed by NM, 5-Jun-2009.)
|
|
|
Theorem | euabex 4117 |
The abstraction of a wff with existential uniqueness exists.
(Contributed by NM, 25-Nov-1994.)
|
|
|
Theorem | mss 4118* |
An inhabited class (even if proper) has an inhabited subset.
(Contributed by Jim Kingdon, 17-Sep-2018.)
|
|
|
Theorem | exss 4119* |
Restricted existence in a class (even if proper) implies restricted
existence in a subset. (Contributed by NM, 23-Aug-2003.)
|
|
|
Theorem | opexg 4120 |
An ordered pair of sets is a set. (Contributed by Jim Kingdon,
11-Jan-2019.)
|
|
|
Theorem | opex 4121 |
An ordered pair of sets is a set. (Contributed by Jim Kingdon,
24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.)
|
|
|
Theorem | otexg 4122 |
An ordered triple of sets is a set. (Contributed by Jim Kingdon,
19-Sep-2018.)
|
|
|
Theorem | elop 4123 |
An ordered pair has two elements. Exercise 3 of [TakeutiZaring] p. 15.
(Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | opi1 4124 |
One of the two elements in an ordered pair. (Contributed by NM,
5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opi2 4125 |
One of the two elements of an ordered pair. (Contributed by NM,
5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
2.3.4 Ordered pair theorem
|
|
Theorem | opm 4126* |
An ordered pair is inhabited iff the arguments are sets. (Contributed
by Jim Kingdon, 21-Sep-2018.)
|
|
|
Theorem | opnzi 4127 |
An ordered pair is nonempty if the arguments are sets (it is also
inhabited; see opm 4126). (Contributed by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | opth1 4128 |
Equality of the first members of equal ordered pairs. (Contributed by
NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opth 4129 |
The ordered pair theorem. If two ordered pairs are equal, their first
elements are equal and their second elements are equal. Exercise 6 of
[TakeutiZaring] p. 16. Note that
and are not required to be
sets due our specific ordered pair definition. (Contributed by NM,
28-May-1995.)
|
|
|
Theorem | opthg 4130 |
Ordered pair theorem.
and are not required
to be sets under
our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.)
(Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opthg2 4131 |
Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by
Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opth2 4132 |
Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
|
|
|
Theorem | otth2 4133 |
Ordered triple theorem, with triple express with ordered pairs.
(Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | otth 4134 |
Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by
Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | eqvinop 4135* |
A variable introduction law for ordered pairs. Analog of Lemma 15 of
[Monk2] p. 109. (Contributed by NM,
28-May-1995.)
|
|
|
Theorem | copsexg 4136* |
Substitution of class
for ordered pair .
(Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon,
11-Jul-2011.)
|
|
|
Theorem | copsex2t 4137* |
Closed theorem form of copsex2g 4138. (Contributed by NM,
17-Feb-2013.)
|
|
|
Theorem | copsex2g 4138* |
Implicit substitution inference for ordered pairs. (Contributed by NM,
28-May-1995.)
|
|
|
Theorem | copsex4g 4139* |
An implicit substitution inference for 2 ordered pairs. (Contributed by
NM, 5-Aug-1995.)
|
|
|
Theorem | 0nelop 4140 |
A property of ordered pairs. (Contributed by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | opeqex 4141 |
Equivalence of existence implied by equality of ordered pairs.
(Contributed by NM, 28-May-2008.)
|
|
|
Theorem | opcom 4142 |
An ordered pair commutes iff its members are equal. (Contributed by NM,
28-May-2009.)
|
|
|
Theorem | moop2 4143* |
"At most one" property of an ordered pair. (Contributed by NM,
11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
Theorem | opeqsn 4144 |
Equivalence for an ordered pair equal to a singleton. (Contributed by
NM, 3-Jun-2008.)
|
|
|
Theorem | opeqpr 4145 |
Equivalence for an ordered pair equal to an unordered pair.
(Contributed by NM, 3-Jun-2008.)
|
|
|
Theorem | euotd 4146* |
Prove existential uniqueness for an ordered triple. (Contributed by
Mario Carneiro, 20-May-2015.)
|
|
|
Theorem | uniop 4147 |
The union of an ordered pair. Theorem 65 of [Suppes] p. 39.
(Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro,
26-Apr-2015.)
|
|
|
Theorem | uniopel 4148 |
Ordered pair membership is inherited by class union. (Contributed by
NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
|
|
|
2.3.5 Ordered-pair class abstractions
(cont.)
|
|
Theorem | opabid 4149 |
The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61.
(Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon,
25-Jul-2011.)
|
|
|
Theorem | elopab 4150* |
Membership in a class abstraction of pairs. (Contributed by NM,
24-Mar-1998.)
|
|
|
Theorem | opelopabsbALT 4151* |
The law of concretion in terms of substitutions. Less general than
opelopabsb 4152, but having a much shorter proof.
(Contributed by NM,
30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(New usage is discouraged.) (Proof modification is discouraged.)
|
|
|
Theorem | opelopabsb 4152* |
The law of concretion in terms of substitutions. (Contributed by NM,
30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
|
|
|
Theorem | brabsb 4153* |
The law of concretion in terms of substitutions. (Contributed by NM,
17-Mar-2008.)
|
|
|
Theorem | opelopabt 4154* |
Closed theorem form of opelopab 4163. (Contributed by NM,
19-Feb-2013.)
|
|
|
Theorem | opelopabga 4155* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19-Dec-2013.)
|
|
|
Theorem | brabga 4156* |
The law of concretion for a binary relation. (Contributed by Mario
Carneiro, 19-Dec-2013.)
|
|
|
Theorem | opelopab2a 4157* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by Mario Carneiro, 19-Dec-2013.)
|
|
|
Theorem | opelopaba 4158* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
Mario Carneiro, 19-Dec-2013.)
|
|
|
Theorem | braba 4159* |
The law of concretion for a binary relation. (Contributed by NM,
19-Dec-2013.)
|
|
|
Theorem | opelopabg 4160* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
|
|
Theorem | brabg 4161* |
The law of concretion for a binary relation. (Contributed by NM,
16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
|
|
|
Theorem | opelopab2 4162* |
Ordered pair membership in an ordered pair class abstraction.
(Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro,
19-Dec-2013.)
|
|
|
Theorem | opelopab 4163* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. (Contributed by
NM, 16-May-1995.)
|
|
|
Theorem | brab 4164* |
The law of concretion for a binary relation. (Contributed by NM,
16-Aug-1999.)
|
|
|
Theorem | opelopabaf 4165* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 4163 uses bound-variable hypotheses in place of
distinct variable
conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof
shortened by Mario Carneiro, 18-Nov-2016.)
|
|
|
Theorem | opelopabf 4166* |
The law of concretion. Theorem 9.5 of [Quine] p.
61. This version of
opelopab 4163 uses bound-variable hypotheses in place of
distinct variable
conditions." (Contributed by NM, 19-Dec-2008.)
|
|
|
Theorem | ssopab2 4167 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro,
19-May-2013.)
|
|
|
Theorem | ssopab2b 4168 |
Equivalence of ordered pair abstraction subclass and implication.
(Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro,
18-Nov-2016.)
|
|
|
Theorem | ssopab2i 4169 |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 5-Apr-1995.)
|
|
|
Theorem | ssopab2dv 4170* |
Inference of ordered pair abstraction subclass from implication.
(Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro,
24-Jun-2014.)
|
|
|
Theorem | eqopab2b 4171 |
Equivalence of ordered pair abstraction equality and biconditional.
(Contributed by Mario Carneiro, 4-Jan-2017.)
|
|
|
Theorem | opabm 4172* |
Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon,
29-Sep-2018.)
|
|
|
Theorem | iunopab 4173* |
Move indexed union inside an ordered-pair abstraction. (Contributed by
Stefan O'Rear, 20-Feb-2015.)
|
|
|
2.3.6 Power class of union and
intersection
|
|
Theorem | pwin 4174 |
The power class of the intersection of two classes is the intersection
of their power classes. Exercise 4.12(j) of [Mendelson] p. 235.
(Contributed by NM, 23-Nov-2003.)
|
|
|
Theorem | pwunss 4175 |
The power class of the union of two classes includes the union of their
power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by
NM, 23-Nov-2003.)
|
|
|
Theorem | pwssunim 4176 |
The power class of the union of two classes is a subset of the union of
their power classes, if one class is a subclass of the other. One
direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by
Jim Kingdon, 30-Sep-2018.)
|
|
|
Theorem | pwundifss 4177 |
Break up the power class of a union into a union of smaller classes.
(Contributed by Jim Kingdon, 30-Sep-2018.)
|
|
|
Theorem | pwunim 4178 |
The power class of the union of two classes equals the union of their
power classes, iff one class is a subclass of the other. Part of Exercise
7(b) of [Enderton] p. 28. (Contributed
by Jim Kingdon, 30-Sep-2018.)
|
|
|
2.3.7 Epsilon and identity
relations
|
|
Syntax | cep 4179 |
Extend class notation to include the epsilon relation.
|
|
|
Syntax | cid 4180 |
Extend the definition of a class to include identity relation.
|
|
|
Definition | df-eprel 4181* |
Define the epsilon relation. Similar to Definition 6.22 of
[TakeutiZaring] p. 30. The
epsilon relation and set membership are the
same, that is, when is a set by
epelg 4182. Thus, 5 { 1 , 5 }. (Contributed by NM,
13-Aug-1995.)
|
|
|
Theorem | epelg 4182 |
The epsilon relation and membership are the same. General version of
epel 4184. (Contributed by Scott Fenton, 27-Mar-2011.)
(Revised by Mario
Carneiro, 28-Apr-2015.)
|
|
|
Theorem | epelc 4183 |
The epsilon relationship and the membership relation are the same.
(Contributed by Scott Fenton, 11-Apr-2012.)
|
|
|
Theorem | epel 4184 |
The epsilon relation and the membership relation are the same.
(Contributed by NM, 13-Aug-1995.)
|
|
|
Definition | df-id 4185* |
Define the identity relation. Definition 9.15 of [Quine] p. 64. For
example, 5 5
and 4 5. (Contributed by NM,
13-Aug-1995.)
|
|
|
2.3.8 Partial and complete ordering
|
|
Syntax | wpo 4186 |
Extend wff notation to include the strict partial ordering predicate.
Read: ' is a
partial order on .'
|
|
|
Syntax | wor 4187 |
Extend wff notation to include the strict linear ordering predicate.
Read: ' orders
.'
|
|
|
Definition | df-po 4188* |
Define the strict partial order predicate. Definition of [Enderton]
p. 168. The expression means is a partial order on
. (Contributed
by NM, 16-Mar-1997.)
|
|
|
Definition | df-iso 4189* |
Define the strict linear order predicate. The expression
is
true if relationship orders .
The property
is called
weak linearity by Proposition
11.2.3 of [HoTT], p. (varies). If we
assumed excluded middle, it would
be equivalent to trichotomy, . (Contributed
by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
|
|
|
Theorem | poss 4190 |
Subset theorem for the partial ordering predicate. (Contributed by NM,
27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
|
|
|
Theorem | poeq1 4191 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | poeq2 4192 |
Equality theorem for partial ordering predicate. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | nfpo 4193 |
Bound-variable hypothesis builder for partial orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
|
|
Theorem | nfso 4194 |
Bound-variable hypothesis builder for total orders. (Contributed by
Stefan O'Rear, 20-Jan-2015.)
|
|
|
Theorem | pocl 4195 |
Properties of partial order relation in class notation. (Contributed by
NM, 27-Mar-1997.)
|
|
|
Theorem | ispod 4196* |
Sufficient conditions for a partial order. (Contributed by NM,
9-Jul-2014.)
|
|
|
Theorem | swopolem 4197* |
Perform the substitutions into the strict weak ordering law.
(Contributed by Mario Carneiro, 31-Dec-2014.)
|
|
|
Theorem | swopo 4198* |
A strict weak order is a partial order. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
|
|
Theorem | poirr 4199 |
A partial order relation is irreflexive. (Contributed by NM,
27-Mar-1997.)
|
|
|
Theorem | potr 4200 |
A partial order relation is a transitive relation. (Contributed by NM,
27-Mar-1997.)
|
|