Home | Metamath
Proof ExplorerTheorem List
(p. 258 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-21459) |
Hilbert Space Explorer
(21460-22982) |
Users' Mathboxes
(22983-31404) |

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

Statement | ||

Theorem | biadan2OLD 25701 | Add a conjunction to an equivalence. (Moved to biadan2 626 in main set.mm and may be deleted by mathbox owner, JM. --NM 25-Feb-2014.) (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |

Theorem | syldanl 25702 | A syllogism deduction with conjoined antecedents. (Contributed by Jeff Madsen, 20-Jun-2011.) |

Theorem | syl3an2cOLDOLD 25703 | 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 25704 | 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 25705 | 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 25706* | Inference from Theorem 19.21 of [Margaris] p. 90. (Restricted quantifier version with double quantification.) (Moved to ralrimivva 2610 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 25707* | Substitution into "at most one". (Moved to sbmo 2148 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 25708* | Distribute quantification over "or". (Moved to 2ralor 2684 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 25709 | Restricted existential quantification over union. (Moved to rexun 3330 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 25710* | Restricted quantification over union. (Moved to ralun 3332 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 25711* | Restricted existential quantification over a singleton. (Moved to rexsn 3649 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 25712* | Specialized existential commutation lemma. (Moved to rexcom4a 2783 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 25713* | Specialized existential commutation lemma. (Moved to rexcom4b 2784 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 25714* | Rearrange three existential quantifiers. (Moved to 3reeanv 2683 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 25715* | Derive membership from uniqueness. (Moved to morex 2924 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 25716* | The unique element such that . (Moved to iota2 6251 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 25717* | 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 25718* | Equality of restricted class abstractions. (Moved to rabeqbidv 2758 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 25719* | Condition for a restricted class abstraction to be empty. (Moved to rabeq0 3451 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 25720* | Law of excluded middle, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Moved to rabxm 3452 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 25721* | Law of noncontradiction, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Moved to rabnc 3453 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 25722* | Universal quantification over a class abstraction. (Moved to ralab 2901 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 25723* | Universal quantification over a restricted class abstraction. (Moved to ralrab 2902 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 25724* | Existential quantification over a class abstraction. (Moved to rexrab 2904 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 25725* | Change the domain of quantification by a function. (Moved to ralima 5692 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 25726* | 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 25727* | 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 25728* | Two ways of saying that two classes are disjoint. (Moved to disjr 3471 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 25729 | Represent a set difference as an intersection with a larger difference. (Moved to difin2 3405 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 25730 | A function with a domain of two elements. (Moved to funpr 5240 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 25731 | The value of a function with a domain of two elements. (Moved to fvpr1 5656 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 25732 | The value of a function with a domain of two elements. (Moved to fvpr2 5657 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 25733 | A function with a domain of two elements. (Moved to fpr 5638 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 25734* | Relation by a binary relation abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | inpreimaOLD 25735 | Preimage of an intersection. (Moved to inpreima 5586 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 25736 | Preimage of a union. (Moved to unpreima 5585 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 25737 | The preimage of a restricted function. (Moved to respreima 5588 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 25738* | Property of a surjective function. (Moved to foelrn 5613 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 25739 | If a composition of two functions is surjective, then the function on the left is surjective. (Moved to foco2 5614 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 25740 | The image of a pair under a funtion. (Moved to fnimapr 5517 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 25741* | Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis. (Contributed by Jeff Madsen, 29-May-2011.) |

Theorem | cocanfo 25742 | 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 25743 | Equinumerosity law for cross product. (Moved to xpen 6992 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 25744 | Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to fvif 5473 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 25745 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to ifeq1da 3564 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 25746 | Conditional equality. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to ifeq2da 3565 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 25747 | Conditional closure. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to ifclda 3566 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 25748 | Equality deduction for cross product. (Moved to xpeq1d 4700 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 25749 | Equality deduction for cross product. (Moved to xpeq1d 4700 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 25750 | The restriction of a set is a set. (Contributed by Jeff Madsen, 19-Jun-2011.) (Moved to resex 4983 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 25751 | Restriction of a binary relation. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | opabex3OLD 25752* | Existence of an ordered pair abstraction. (Moved to opabex3 5703 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 25753* | Equality deduction for function abstractions. (Contributed by Jeff Madsen, 19-Jun-2011.) |

Theorem | fvopabf4g 25754* | 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 25755 | 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 25756* | Composition of a function with a function abstraction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |

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

Theorem | oprabexdOLD 25758* | Existence of an operator abstraction. (Moved to oprabexd 5894 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 25759* | Condition for an operation to be one-to-one. (Contributed by Jeff Madsen, 17-Jun-2010.) |

Theorem | cnvcanOLD 25760 | Composition with the converse. (Moved to funcocnv2 5436 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 25761 | Composition with a function and then with the converse. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | f1ocan1fv 25762 | 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 25763 | Cancel a composition by the converse of a bijection by preapplying the bijection. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | f1elimaOLD 25764 | Membership in the image of a 1-1 map. (Moved to f1elima 5721 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 25765 | A one-to-one mapping of finite sets with the same cardinality is bijective. (Moved to f1finf1o 7054 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 25766* | Derive equality of functions from equality of their values. (Moved to eqfnfv3 5558 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 25767* | Intersection of Cartesian products over the same base set. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | ixpssmapgOLD 25768* | An infinite Cartesian product is a subset of set exponentiation. (Moved into main set.mm as ixpssmapg 6814 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 25769 | Set exponentiation of finite sets is finite. (Moved into main set.mm as mapfi 7120 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 25770* | A cross product of finitely many finite sets is finite. (Moved into main set.mm as ixpfi 7121 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 25771* | Universal property of the indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |

Theorem | abrexex2gOLD 25772* | Existence of an existentially restricted class abstraction. (Moved to abrexex2g 5702 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 25773* | An indexed set is dominated by the indexing set. (Contributed by Jeff Madsen, 2-Sep-2009.) |

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

Theorem | findcard2OLD 25775* | 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 7066 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 25776* | A finite set has a maximum under a total order. (Moved to fimaxg 7072 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 25777* | A finite set has a maximum under a total order. (Moved to fimaxg 7072 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 25778* | Lemma showing existence and closure of supremum of a finite set. (Moved to fisupg 7073 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 25779* | Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009.) |

Theorem | indexa 25780* | 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 25781* | 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 25782* | 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 25781. (Moved to indexfi 7131 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 25783* | Given a finite subset of the range of a function, there exists a finite subset of the domain whose image is . (Moved to fipreima 7129 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 25784* | A subset of a well founded set has an infimum. (Contributed by Jeff Madsen, 2-Sep-2009.) |

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

Theorem | supeq2OLD 25786 | Equality theorem for supremum. (Moved to supeq2 7169 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 25787 | Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009.) |

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

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

Theorem | infmrlbOLD 25790* | 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 9703 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 25791* | A supremum is unique. Closed version of supeu 7173. (Moved to supeu 7173 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 25792 | A nonempty finite set contains its supremum. (Moved to fisupcl 7186 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 25793* | A finite set has a maximum under a total order. (Moved to fimax2g 7071 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 25794 | A total order on a finite set is a well order. (Moved to wofi 7074 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 25795 | A partial order is founded on a finite set. (Moved to frfi 7070 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 25796* | A function preserves a partial order relation. (Moved to pofun 4302 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 25797* | If an element of a founded set satisfies a property , then there is a minimal element that satisfies . (Moved to frminex 4345 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.) |

18.14.2 Real and complex numbers;
integers | ||

Theorem | fimaxreOLD 25798* | A finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 2-Sep-2009.) (Moved to fimaxre 9669 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 25799* | A nonempty finite set of real numbers has a maximum. (Contributed by Jeff Madsen, 27-May-2011.) (Moved to fimaxre2 9670 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 25800* | Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009.) |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |