Home | Intuitionistic Logic Explorer Theorem List (p. 43 of 138) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | opex 4201 | An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.) |
Theorem | otexg 4202 | An ordered triple of sets is a set. (Contributed by Jim Kingdon, 19-Sep-2018.) |
Theorem | elop 4203 | 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 4204 | One of the two elements in an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opi2 4205 | One of the two elements of an ordered pair. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opm 4206* | An ordered pair is inhabited iff the arguments are sets. (Contributed by Jim Kingdon, 21-Sep-2018.) |
Theorem | opnzi 4207 | An ordered pair is nonempty if the arguments are sets (it is also inhabited; see opm 4206). (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth1 4208 | Equality of the first members of equal ordered pairs. (Contributed by NM, 28-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth 4209 | 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 4210 | 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 4211 | Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opth2 4212 | Ordered pair theorem. (Contributed by NM, 21-Sep-2014.) |
Theorem | otth2 4213 | Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | otth 4214 | Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | eqvinop 4215* | A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.) |
Theorem | copsexg 4216* | Substitution of class for ordered pair . (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.) |
Theorem | copsex2t 4217* | Closed theorem form of copsex2g 4218. (Contributed by NM, 17-Feb-2013.) |
Theorem | copsex2g 4218* | Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.) |
Theorem | copsex4g 4219* | An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.) |
Theorem | 0nelop 4220 | A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.) |
Theorem | opeqex 4221 | Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.) |
Theorem | opcom 4222 | An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.) |
Theorem | moop2 4223* | "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opeqsn 4224 | Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.) |
Theorem | opeqpr 4225 | Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.) |
Theorem | euotd 4226* | Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.) |
Theorem | uniop 4227 | 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 4228 | Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Theorem | opabid 4229 | 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 4230* | Membership in a class abstraction of ordered pairs. (Contributed by NM, 24-Mar-1998.) |
Theorem | opelopabsbALT 4231* | The law of concretion in terms of substitutions. Less general than opelopabsb 4232, 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 4232* | The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.) |
Theorem | brabsb 4233* | The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.) |
Theorem | opelopabt 4234* | Closed theorem form of opelopab 4243. (Contributed by NM, 19-Feb-2013.) |
Theorem | opelopabga 4235* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | brabga 4236* | The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab2a 4237* | Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopaba 4238* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Theorem | braba 4239* | The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.) |
Theorem | opelopabg 4240* | 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 4241* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab2 4242* | Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Theorem | opelopab 4243* | The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.) |
Theorem | brab 4244* | The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) |
Theorem | opelopabaf 4245* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4243 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 4246* | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4243 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.) |
Theorem | ssopab2 4247 | Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.) |
Theorem | ssopab2b 4248 | Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
Theorem | ssopab2i 4249 | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.) |
Theorem | ssopab2dv 4250* | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
Theorem | eqopab2b 4251 | Equivalence of ordered pair abstraction equality and biconditional. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Theorem | opabm 4252* | Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon, 29-Sep-2018.) |
Theorem | iunopab 4253* | Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
Theorem | pwin 4254 | 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 4255 | 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 4256 | 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 4257 | Break up the power class of a union into a union of smaller classes. (Contributed by Jim Kingdon, 30-Sep-2018.) |
Theorem | pwunim 4258 | 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.) |
Syntax | cep 4259 | Extend class notation to include the epsilon relation. |
Syntax | cid 4260 | Extend the definition of a class to include identity relation. |
Definition | df-eprel 4261* | 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 4262. Thus, 5 { 1 , 5 }. (Contributed by NM, 13-Aug-1995.) |
Theorem | epelg 4262 | The epsilon relation and membership are the same. General version of epel 4264. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | epelc 4263 | The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.) |
Theorem | epel 4264 | The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.) |
Definition | df-id 4265* | Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 5 and 4 5. (Contributed by NM, 13-Aug-1995.) |
We have not yet defined relations (df-rel 4605), but here we introduce a few related notions we will use to develop ordinals. The class variable is no different from other class variables, but it reminds us that typically it represents what we will later call a "relation". | ||
Syntax | wpo 4266 | Extend wff notation to include the strict partial ordering predicate. Read: ' is a partial order on .' |
Syntax | wor 4267 | Extend wff notation to include the strict linear ordering predicate. Read: ' orders .' |
Definition | df-po 4268* | 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 4269* | 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 4270 | Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
Theorem | poeq1 4271 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
Theorem | poeq2 4272 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
Theorem | nfpo 4273 | Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
Theorem | nfso 4274 | Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
Theorem | pocl 4275 | Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.) |
Theorem | ispod 4276* | Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.) |
Theorem | swopolem 4277* | Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.) |
Theorem | swopo 4278* | A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.) |
Theorem | poirr 4279 | A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.) |
Theorem | potr 4280 | A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.) |
Theorem | po2nr 4281 | A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.) |
Theorem | po3nr 4282 | A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.) |
Theorem | po0 4283 | Any relation is a partial ordering of the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | pofun 4284* | A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.) |
Theorem | sopo 4285 | A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.) |
Theorem | soss 4286 | Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Theorem | soeq1 4287 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
Theorem | soeq2 4288 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
Theorem | sonr 4289 | A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.) |
Theorem | sotr 4290 | A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.) |
Theorem | issod 4291* | An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4269). (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.) |
Theorem | sowlin 4292 | A strict order relation satisfies weak linearity. (Contributed by Jim Kingdon, 6-Oct-2018.) |
Theorem | so2nr 4293 | A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.) |
Theorem | so3nr 4294 | A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.) |
Theorem | sotricim 4295 | One direction of sotritric 4296 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.) |
Theorem | sotritric 4296 | A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 28-Sep-2019.) |
Theorem | sotritrieq 4297 | A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.) |
Theorem | so0 4298 | Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Syntax | wfrfor 4299 | Extend wff notation to include the well-founded predicate. |
FrFor | ||
Syntax | wfr 4300 | Extend wff notation to include the well-founded predicate. Read: ' is a well-founded relation on .' |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |