Home | Metamath
Proof ExplorerTheorem List
(p. 256 of 311)
| < 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-31058) |

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

Statement | ||

Theorem | syl3an2cOLDOLD 25501 | A syllogism inference combined with contraction. (Moved to syl13anc 1189 in main set.mm and may be deleted by mathbox owner, JM. --NM 8-Sep-2011.) (Contributed by Jeff Madsen, 17-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | mp4anOLD 25502 | An inference based on modus ponens. (Moved to mp4an 657 in main set.mm and may be deleted by mathbox owner, JM. --NM 19-Oct-2012.) (Contributed by Jeff Madsen, 15-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | imdistandaOLD 25503 | Distribution of implication with conjunction (deduction version with conjoined antecedent). (Moved into main set.mm as imdistanda 677 and may be deleted by mathbox owner, SF. --NM 20-Sep-2013.) (Contributed by Jeff Madsen, 19-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | r19.21aivvaOLD 25504* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Moved to ralrimivva 2597 in main set.mm and may be deleted by mathbox owner, JM. --NM 17-Jul-2012.) (Contributed by Jeff Madsen, 19-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | sbmoOLD 25505* | Substitution into "at most one". (Moved to sbmo 2143 in main set.mm and may be deleted by mathbox owner, JM. --NM 29-Jan-2012.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | 2ralorOLD 25506* | Distribute quantification over "or". (Moved to 2ralor 2671 in main set.mm and may be deleted by mathbox owner, JM. --NM 29-Jan-2012.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | rexunOLD 25507 | Restricted existential quantification over union. (Moved to rexun 3263 in main set.mm and may be deleted by mathbox owner, JM. --NM 29-Jan-2012.) (Contributed by Jeff Madsen, 5-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ralunOLD 25508* | Restricted quantification over union. (Moved to ralun 3265 in main set.mm and may be deleted by mathbox owner, JM. --NM 29-Jan-2012.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | rexsnOLD 25509* | Restricted existential quantification over a singleton. (Moved to rexsn 3579 in main set.mm and may be deleted by mathbox owner, JM. --NM 29-Jan-2012.) (Contributed by Jeff Madsen, 5-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | rexcom4aOLD 25510* | Specialized existential commutation lemma. (Moved to rexcom4a 2746 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Apr-2012.) (Contributed by Jeff Madsen, 1-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | rexcom4bOLD 25511* | Specialized existential commutation lemma. (Moved to rexcom4b 2747 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Apr-2012.) (Contributed by Jeff Madsen, 1-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | 3reeanvOLD 25512* | Rearrange three existential quantifiers. (Moved to 3reeanv 2670 in main set.mm and may be deleted by mathbox owner, JM. --NM 21-Mar-2013.) (Contributed by Jeff Madsen, 11-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | morexOLD 25513* | Derive membership from uniqueness. (Moved to morex 2886 in main set.mm and may be deleted by mathbox owner, JM. --NM 19-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | euuni2OLD 25514* | The unique element such that . (Moved to iota2 6169 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Oct-2012.) (Contributed by Jeff Madsen, 1-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | unirep 25515* | Define a quantity whose definition involves a choice of representative, but which is uniquely determined regardless of the choice. (Contributed by Jeff Madsen, 1-Jun-2011.) |

Theorem | rabeq12OLD 25516* | Equality of restricted class abstractions. (Moved to rabeqbidv 2722 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Sep-2011.) (Contributed by Jeff Madsen, 1-Dec-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | rabeq0OLD 25517* | Condition for a restricted class abstraction to be empty. (Moved to rabeq0 3383 in main set.mm and may be deleted by mathbox owner, JM. --NM 1-Apr-2013.) (Contributed by Jeff Madsen, 7-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | rabxmOLD 25518* | Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Moved to rabxm 3384 in main set.mm and may be deleted by mathbox owner, JM. --NM 10-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | rabncOLD 25519* | Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Moved to rabnc 3385 in main set.mm and may be deleted by mathbox owner, JM. --NM 10-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ralabOLD 25520* | Universal quantification over a class abstraction. (Moved to ralab 2863 in main set.mm and may be deleted by mathbox owner, JM. --NM 20-Oct-2011.) (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ralrabOLD 25521* | Universal quantification over a restricted class abstraction. (Moved to ralrab 2864 in main set.mm and may be deleted by mathbox owner, JM. --NM 20-Oct-2011.) (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | rexrabOLD 25522* | Existential quantification over a class abstraction. (Moved to rexrab 2866 in main set.mm and may be deleted by mathbox owner, JM. --NM 20-Mar-2013.) (Contributed by Jeff Madsen, 17-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | raleqfnOLD 25523* | Change the domain of quantification by a function. (Moved to ralima 5610 in main set.mm and may be deleted by mathbox owner, JM. --NM 17-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | cover2 25524* | Two ways of expressing the statement "there is a cover of by elements of such that for each set in the cover, ." Note that and must be distinct. (Contributed by Jeff Madsen, 20-Jun-2010.) |

Theorem | cover2g 25525* | Two ways of expressing the statement "there is a cover of by elements of such that for each set in the cover, ." Note that and must be distinct. (Contributed by Jeff Madsen, 21-Jun-2010.) |

Theorem | disjrOLD 25526* | Two ways of saying that two classes are disjoint. (Moved to disjr 3403 in main set.mm and may be deleted by mathbox owner, JM. --NM 23-Mar-2013.) (Contributed by Jeff Madsen, 19-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | difin2OLD 25527 | Represent a set difference as an intersection with a larger difference. (Moved to difin2 3337 in main set.mm and may be deleted by mathbox owner, JM. --NM 31-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | prfunOLD 25528 | A function with a domain of two elements. (Moved to funpr 5159 in main set.mm and may be deleted by mathbox owner, JM. --NM 26-Aug-2011.) (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | prfv1OLD 25529 | The value of a function with a domain of two elements. (Moved to fvpr1 5574 in main set.mm and may be deleted by mathbox owner, JM. --NM 3-Sep-2011.) (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | prfv2OLD 25530 | The value of a function with a domain of two elements. (Moved to fvpr2 5575 in main set.mm and may be deleted by mathbox owner, JM. --NM 3-Sep-2011.) (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | prfOLD 25531 | A function with a domain of two elements. (Moved to fpr 5556 in main set.mm and may be deleted by mathbox owner, JM. --NM 3-Sep-2011.) (Contributed by Jeff Madsen, 20-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | brabg2 25532* | Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | inpreimaOLD 25533 | Preimage of an intersection. (Moved to inpreima 5504 in main set.mm and may be deleted by mathbox owner, JM. --NM 28-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | unpreimaOLD 25534 | Preimage of a union. (Moved to unpreima 5503 in main set.mm and may be deleted by mathbox owner, JM. --NM 29-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | respreimaOLD 25535 | The preimage of a restricted function. (Moved to respreima 5506 in main set.mm and may be deleted by mathbox owner, JM. --NM 30-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | foelrnOLD 25536* | Property of a surjective function. (Moved to foelrn 5531 in main set.mm and may be deleted by mathbox owner, JM. --NM 4-Feb-2013.) (Contributed by Jeff Madsen, 4-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | foco2OLD 25537 | If a composition of two functions is surjective, then the function on the left is surjective. (Moved to foco2 5532 in main set.mm and may be deleted by mathbox owner, JM. --NM 18-Apr-2013.) (Contributed by Jeff Madsen, 16-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fnimaprOLD 25538 | The image of a pair under a funtion. (Moved to fnimapr 5435 in main set.mm and may be deleted by mathbox owner, JM. --NM 19-Apr-2013.) (Contributed by Jeff Madsen, 6-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | opelopab3 25539* | Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011.) |

Theorem | cocanfo 25540 | Cancellation of a surjective function from the right side of a composition. (Contributed by Jeff Madsen, 1-Jun-2011.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |

Theorem | xpengOLD 25541 | Equinumerosity law for cross product. (Moved to xpen 6909 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 17-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fvifOLD 25542 | Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to fvif 5392 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Jan-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ifeq1daOLD 25543 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to ifeq1da 3495 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Jan-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ifeq2daOLD 25544 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to ifeq2da 3496 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Jan-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ifcldaOLD 25545 | Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to ifclda 3497 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Jan-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | xpeq1dOLD 25546 | Equality deduction for cross product. (Moved to xpeq1d 4619 in main set.mm and may be deleted by mathbox owner, JM. --NM 4-Feb-2013.) (Contributed by Jeff Madsen, 17-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | xpeq2dOLD 25547 | Equality deduction for cross product. (Moved to xpeq1d 4619 in main set.mm and may be deleted by mathbox owner, JM. --NM 4-Feb-2013.) (Contributed by Jeff Madsen, 17-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | resexOLD 25548 | The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.) (Moved to resex 4902 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Jan-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | brresi 25549 | Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | opabex3OLD 25550* | Existence of an ordered pair abstraction. (Moved to opabex3 5621 in main set.mm and may be deleted by mathbox owner, JM. --NM 30-Jan-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fnopabeqd 25551* | Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011.) |

Theorem | fvopabf4g 25552* | Function value of an operator abstraction whose domain is a set of functions with given domain and range. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |

Theorem | eqfnun 25553 | Two functions on are equal if and only if they have equal restrictions to both and . (Contributed by Jeff Madsen, 19-Jun-2011.) |

Theorem | fnopabco 25554* | Composition of a function with a function abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |

Theorem | opropabco 25555* | Composition of an operator with a function abstraction. (Contributed by Jeff Madsen, 11-Jun-2010.) |

Theorem | oprabexdOLD 25556* | Existence of an operator abstraction. (Moved to oprabexd 5812 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | f1opr 25557* | Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010.) |

Theorem | cnvcanOLD 25558 | Composition with the converse. (Moved to funcocnv2 5355 in main set.mm and may be deleted by mathbox owner, JM. --NM 28-Feb-2015.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | cocnv 25559 | Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | f1ocan1fv 25560 | Cancel a composition by a bijection by preapplying the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 27-Dec-2014.) |

Theorem | f1ocan2fv 25561 | Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | f1elimaOLD 25562 | Membership in the image of a 1-1 map. (Moved to f1elima 5639 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | enf1f1oOLD 25563 | A one-to-one mapping of finite sets with the same cardinality is bijective. (Moved to f1finf1o 6971 in main set.mm and may be deleted by mathbox owner, JM. --NM 24-Sep-2013.) (Contributed by Jeff Madsen, 5-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | eqfnfv3OLD 25564* | Derive equality of functions from equality of their values. (Moved to eqfnfv3 5476 in main set.mm and may be deleted by mathbox owner, JM. --NM 22-Nov-2011.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | inixp 25565* | Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | ixpssmapgOLD 25566* | An infinite Cartesian product is a subset of set exponentiation. (Moved into main set.mm as ixpssmapg 6732 and may be deleted by mathbox owner, JM. --NM 18-Jun-2013.) (Contributed by Jeff Madsen, 19-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | mapfiOLD 25567 | Set exponentiation of finite sets is finite. (Moved into main set.mm as mapfi 7036 and may be deleted by mathbox owner, JM. --NM 24-Sep-2013.) (Contributed by Jeff Madsen, 19-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ixpfiOLD 25568* | A cross product of finitely many finite sets is finite. (Moved into main set.mm as ixpfi 7037 and may be deleted by mathbox owner, JM. --NM 24-Sep-2013.) (Contributed by Jeff Madsen, 19-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | upixp 25569* | Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |

Theorem | abrexex2gOLD 25570* | Existence of an existentially restricted class abstraction. (Moved to abrexex2g 5620 in main set.mm and may be deleted by mathbox owner, JM. --NM 21-May-2012.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | abrexdom 25571* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | abrexdom2 25572* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | findcard2OLD 25573* | Schema for induction on the cardinality of a finite set. The inductive step shows that the result is true if one more element is added to the set. The result is then proven to be true for all finite sets. (Moved to findcard2 6983 in main set.mm and may be deleted by mathbox owner, JM. --NM 30-Nov-2012.) (Contributed by Jeff Madsen, 8-Jul-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fimaxOLD 25574* | A finite set has a maximum under a total order. (Moved to fimaxg 6989 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fimaxgOLD 25575* | A finite set has a maximum under a total order. (Moved to fimaxg 6989 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fisupgOLD 25576* | Lemma showing existence and closure of supremum of a finite set. (Moved to fisupg 6990 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | ac6gf 25577* | Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | indexa 25578* | If for every element of an indexing set there exists a corresponding element of another set , then there exists a subset of consisting only of those elements which are indexed by . Used to avoid the Axiom of Choice in situations where only the range of the choice function is needed. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | indexdom 25579* | If for every element of an indexing set there exists a corresponding element of another set , then there exists a subset of consisting only of those elements which are indexed by , and which is dominated by the set . (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | indexfiOLD 25580* | If for every element of a finite indexing set there exists a corresponding element of another set , then there exists a finite subset of consisting only of those elements which are indexed by . Proven without the Axiom of Choice, unlike indexdom 25579. (Moved to indexfi 7047 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Apr-2012.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fipreimaOLD 25581* | Given a finite subset of the range of a function, there exists a finite subset of the domain whose image is . (Moved to fipreima 7045 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Apr-2012.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 1-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | frinfm 25582* | A subset of a well founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | welb 25583* | A non-empty subset of a well ordered set has a lower bound. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | supeq2OLD 25584 | Equality theorem for supremum. (Moved to supeq2 7085 in main set.mm and may be deleted by mathbox owner, JM. --NM 24-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | supex2g 25585 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | supclt 25586* | Closure of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | supubt 25587* | Upper bound property of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | infmrlbOLD 25588* | A member of a non-empty bounded set of reals is greater than or equal to the set's lower bound. (Contributed by Jeff Madsen, 2-Feb-2011.) (Moved to infmrlb 9615 in main set.mm and may be deleted by mathbox owner, JM. --NM 21-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | supeutOLD 25589* | A supremum is unique. Closed version of supeu 7089. (Moved to supeu 7089 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 9-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fisup2gOLD 25590 | A nonempty finite set contains its supremum. (Moved to fisupcl 7102 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 9-May-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fimax2gOLD 25591* | A finite set has a maximum under a total order. (Moved to fimax2g 6988 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | wofiOLD 25592 | A total order on a finite set is a well order. (Moved to wofi 6991 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | frfiOLD 25593 | A partial order is founded on a finite set. (Moved to frfi 6987 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | pofunOLD 25594* | A function preserves a partial order relation. (Moved to pofun 4223 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | frminexOLD 25595* | If an element of a founded set satisfies a property , then there is a minimal element that satisfies . (Moved to frminex 4266 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.) (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

16.13.2 Real and complex numbers;
integers | ||

Theorem | fimaxreOLD 25596* | A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to fimaxre 9581 in main set.mm and may be deleted by mathbox owner, JM. --NM 22-Mar-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | fimaxre2OLD 25597* | A nonempty finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 27-May-2011.) (Moved to fimaxre2 9582 in main set.mm and may be deleted by mathbox owner, JM. --NM 22-Mar-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | filbcmb 25598* | Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | add20OLD 25599 | Two nonnegative numbers are zero iff their sum is zero. (Moved to add20 9166 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | addsubeq4OLD 25600 | Relation between sums and differences.. (Moved to addsubeq4 8946 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Sep-2013.) (Contributed by Jeff Madsen, 17-Jun-2010.) (Proof modification is discouraged.) (New usage is discouraged.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |