mmtheorems166 - Metamath Proof Explorer

Jump to page: Contents + 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19026

Statement List for Metamath Proof Explorer - 16501-16600 - Page 166 of 191

Type	Label	Description
Statement
Theorem	prfunOLD 16501	A function with a domain of two elements. (Moved to funpr 4568 in main set.mm and may be deleted by mathbox owner, JM. --NM 26-Aug-2011.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- D e. _V   =>   |- (A =/= B -> Fun {<.A, C>., <.B, D>.})
Theorem	prfv1OLD 16502	The value of a function with a domain of two elements. (Moved to fvpr1 4846 in main set.mm and may be deleted by mathbox owner, JM. --NM 3-Sep-2011.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- D e. _V   =>   |- (A =/= B -> ({<.A, C>., <.B, D>.}` A) = C)
Theorem	prfv2OLD 16503	The value of a function with a domain of two elements. (Moved to fvpr2 4847 in main set.mm and may be deleted by mathbox owner, JM. --NM 3-Sep-2011.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- D e. _V   =>   |- (A =/= B -> ({<.A, C>., <.B, D>.}` B) = D)
Theorem	prfOLD 16504	A function with a domain of two elements. (Moved to fpr 4904 in main set.mm and may be deleted by mathbox owner, JM. --NM 3-Sep-2011.)
|- A e. _V   &   |- B e. _V   &   |- C e. _V   &   |- D e. _V   =>   |- (A =/= B -> {<.A, C>., <.B, D>.}:{A, B}-->{C, D})
Theorem	brabg2 16505	Relation by a binary relation abstraction.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- R = {<.x, y>. | ph}   &   |- (ch -> A e. C)   =>   |- (B e. D -> (ARB <-> ch))
Theorem	inpreimaOLD 16506	Preimage of an intersection. (Moved to inpreima 4871 in main set.mm and may be deleted by mathbox owner, JM. --NM 28-Mar-2013.)
|- (Fun F -> (`'F"(A i^i B)) = ((`'F"A) i^i (`'F"B)))
Theorem	unpreimaOLD 16507	Preimage of a union. (Moved to unpreima 4870 in main set.mm and may be deleted by mathbox owner, JM. --NM 29-Mar-2013.)
|- (Fun F -> (`'F"(A u. B)) = ((`'F"A) u. (`'F"B)))
Theorem	respreimaOLD 16508	The preimage of a restricted function. (Moved to respreima 4872 in main set.mm and may be deleted by mathbox owner, JM. --NM 30-Mar-2013.)
|- (Fun F -> (`'(F |` B)"A) = ((`'F"A) i^i B))
Theorem	foelrnOLD 16509	Property of a surjective function. (Moved to foelrn 4886 in main set.mm and may be deleted by mathbox owner, JM. --NM 4-Feb-2013.)
|- ((F:A-onto->B /\ C e. B) -> E.x e. A C = (F` x))
Theorem	foco2OLD 16510	If a composition of two functions is surjective, then the function on the left is surjective. (Moved to foco 4716 in main set.mm and may be deleted by mathbox owner, JM. --NM 18-Apr-2013.)
|- ((F:B-->C /\ G:A-->B /\ (F o. G):A-onto->C) -> F:B-onto->C)
Theorem	fnimaprOLD 16511	The image of a pair under a funtion. (Moved to fnimapr 4813 in main set.mm and may be deleted by mathbox owner, JM. --NM 19-Apr-2013.)
|- ((F Fn A /\ B e. A /\ C e. A) -> (F"{B, C}) = {(F` B), (F` C)})
Theorem	opelopab3 16512	Ordered pair membership in an ordered pair class abstraction, with a reduced hypothesis.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (ch -> A e. C)   =>   |- (B e. D -> (<.A, B>. e. {<.x, y>. | ph} <-> ch))
Theorem	cocanfo 16513	Cancellation of a surjective function from the right side of a composition.
|- (((F:A-onto->B /\ G Fn B /\ H Fn B) /\ (G o. F) = (H o. F)) -> G = H)
Theorem	difxpOLD 16514	Difference of Cartesian products, expressed in terms of a union of Cartesian products of differences. (Moved to difxp 5151 in main set.mm and may be deleted by mathbox owner, JM. --NM 15-Oct-2012.)
|- ((C X. D) \ (A X. B)) = ((((C \ A) X. D) u. (C X. (D \ B))) u. ((C \ A) X. (D \ B)))
Theorem	xpengOLD 16515	Equinumerosity law for cross product. (Moved to xpeng 5769 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- (((A e. W /\ B e. X) /\ (C e. Y /\ D e. Z)) -> ((A ~~ B /\ C ~~ D) -> (A X. C) ~~ (B X. D)))
Theorem	fvif 16516	Move a conditional outside of a function.
|- (F` if(ph, A, B)) = if(ph, (F` A), (F` B))
Theorem	ifeq1da 16517	Conditional equality.
|- ((ph /\ ps) -> A = B)   =>   |- (ph -> if(ps, A, C) = if(ps, B, C))
Theorem	ifeq2da 16518	Conditional equality.
|- ((ph /\ -. ps) -> A = B)   =>   |- (ph -> if(ps, C, A) = if(ps, C, B))
Theorem	ifclda 16519	Conditional closure.
|- ((ph /\ ps) -> A e. C)   &   |- ((ph /\ -. ps) -> B e. C)   =>   |- (ph -> if(ps, A, B) e. C)
Theorem	xpeq1dOLD 16520	Equality deduction for cross product. (Moved to xpeq1d 4157 in main set.mm and may be deleted by mathbox owner, JM. --NM 4-Feb-2013.)
|- (ph -> A = B)   =>   |- (ph -> (A X. C) = (B X. C))
Theorem	xpeq2dOLD 16521	Equality deduction for cross product. (Moved to xpeq1d 4157 in main set.mm and may be deleted by mathbox owner, JM. --NM 4-Feb-2013.)
|- (ph -> A = B)   =>   |- (ph -> (C X. A) = (C X. B))
Theorem	resex 16522	The restriction of a set is a set.
|- A e. _V   =>   |- (A |` B) e. _V
Theorem	brresi 16523	Restriction of a binary relation.
|- B e. _V   =>   |- (A(R |` C)B -> ARB)
Theorem	fconst6 16524	A constant function as a mapping.
|- B e. C   =>   |- (A X. {B}):A-->C
Theorem	opabex3OLD 16525	Existence of an ordered pair abstraction. (Moved to opabex3 4933 in main set.mm and may be deleted by mathbox owner, JM. --NM 30-Jan-2013.)
|- A e. _V   &   |- (x e. A -> {y | ph} e. _V)   =>   |- {<.x, y>. | (x e. A /\ ph)} e. _V
Theorem	fnopabeqd 16526	Equality deduction for function abstractions.
|- (ph -> B = C)   =>   |- (ph -> {<.x, y>. | (x e. A /\ y = B)} = {<.x, y>. | (x e. A /\ y = C)})
Theorem	fvopabf4g 16527	Function value of an operator abstraction whose domain is a set of functions with given domain and range.
|- C e. _V   &   |- (x = A -> B = C)   &   |- F = {<.x, y>. | (x:D-->R /\ y = B)}   =>   |- ((D e. X /\ R e. Y /\ A:D-->R) -> (F` A) = C)
Theorem	eqfnoprv2 16528	Two operators with the same domain are equal iff their values at each point in the domain are equal.
|- ((F Fn (A X. B) /\ G Fn (A X. B)) -> (F = G <-> A.x e. A A.y e. B (xFy) = (xGy)))
Theorem	eqfnun 16529	Two functions on A u. B are equal if and only if they have equal restrictions to both A and B.
|- ((F Fn (A u. B) /\ G Fn (A u. B)) -> (F = G <-> ((F |` A) = (G |` A) /\ (F |` B) = (G |` B))))
Theorem	oprabvalg 16530	The value of an operation class abstraction.
|- (x = A -> (ph <-> ps))   &   |- (y = B -> (ps <-> ch))   &   |- (z = C -> (ch <-> th))   &   |- ((ta /\ (x e. R /\ y e. S)) -> E!zph)   &   |- F = {<.<.x, y>., z>. | ((x e. R /\ y e. S) /\ ph)}   =>   |- ((ta /\ (A e. R /\ B e. S /\ C e. D)) -> ((AFB) = C <-> th))
Theorem	oprabval2a 16531	The value of an operation class abstraction. Variant of oprabval2 5051 which does not require D and x to be distinct.
|- S e. _V   &   |- (x = A -> R = G)   &   |- (x = A -> D = L)   &   |- (y = B -> G = S)   &   |- F = {<.<.x, y>., z>. | ((x e. C /\ y e. D) /\ z = R)}   =>   |- ((A e. C /\ B e. L) -> (AFB) = S)
Theorem	cbvoprab2 16532	Change the second bound variable in an operation abstraction.
|- (ph -> A.wph)   &   |- (ps -> A.yps)   &   |- (y = w -> (ph <-> ps))   =>   |- {<.<.x, y>., z>. | ph} = {<.<.x, w>., z>. | ps}
Theorem	oprabrexex2 16533	Existence of an existentially restricted operation abstraction.
|- A e. _V   &   |- {<.<.x, y>., z>. | ph} e. _V   =>   |- {<.<.x, y>., z>. | E.w e. A ph} e. _V
Theorem	resoprab2 16534	Restriction of an operator abstraction.
|- ((C C_ A /\ D C_ B) -> ({<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} |` (C X. D)) = {<.<.x, y>., z>. | ((x e. C /\ y e. D) /\ ph)})
Theorem	fnopabco 16535	Composition of a function with a function abstraction.
|- (x e. A -> B e. C)   &   |- F = {<.x, y>. | (x e. A /\ y = B)}   &   |- G = {<.x, y>. | (x e. A /\ y = (H` B))}   =>   |- (H Fn C -> G = (H o. F))
Theorem	opropabco 16536	Composition of an operator with a function abstraction.
|- (x e. A -> B e. R)   &   |- (x e. A -> C e. S)   &   |- F = {<.x, y>. | (x e. A /\ y = <.B, C>.)}   &   |- G = {<.x, y>. | (x e. A /\ y = (BMC))}   =>   |- (M Fn (R X. S) -> G = (M o. F))
Theorem	oprabexd 16537	Existence of an operator abstraction.
|- (ph -> A e. _V)   &   |- (ph -> B e. _V)   &   |- ((ph /\ (x e. A /\ y e. B)) -> E*zps)   &   |- (ph -> F = {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ps)})   =>   |- (ph -> F e. _V)
Theorem	f1opr 16538	Condition for an operation to be one-to-one.
|- (F:(A X. B)-1-1->C <-> (F:(A X. B)-->C /\ A.r e. A A.s e. B A.t e. A A.u e. B ((rFs) = (tFu) -> (r = t /\ s = u))))
Theorem	cnvcan 16539	Composition with the converse.
|- (Fun G -> (G o. `'G) = ( _I |` ran G))
Theorem	cocnv 16540	Composition with a function and then with the converse.
|- ((Fun F /\ Fun G) -> ((F o. G) o. `'G) = (F |` ran G))
Theorem	f1ocan1fv 16541	Cancel a composition by a bijection by preapplying the converse.
|- ((Fun F /\ G:A-1-1-onto->B /\ X e. B) -> ((F o. G)` (`'G` X)) = (F` X))
Theorem	f1ocan2fv 16542	Cancel a composition by the converse of a bijection by preapplying the bijection.
|- ((Fun F /\ G:A-1-1-onto->B /\ X e. A) -> ((F o. `'G)` (G` X)) = (F` X))
Theorem	f1elima 16543	Membership in the image of a 1-1 map.
|- ((F:A-1-1->B /\ X e. A /\ Y C_ A) -> ((F` X) e. (F"Y) <-> X e. Y))
Theorem	enf1f1o 16544	A one-to-one mapping of finite sets with the same cardinality is bijective.
|- ((A e. Fin /\ B ~~ A) -> (F:A-1-1->B -> F:A-1-1-onto->B))
Theorem	eqfnfv3OLD 16545	Derive equality of functions from equality of their values. (Moved to eqfnfv3 4855 in main set.mm and may be deleted by mathbox owner, JM. --NM 22-Nov-2011.)
|- ((F Fn A /\ G Fn B) -> (F = G <-> (B C_ A /\ A.x e. A (x e. B /\ (F` x) = (G` x)))))
Theorem	inixp 16546	Intersection of Cartesian products over the same base set.
|- (X_x e. A B i^i X_x e. A C) = X_x e. A (B i^i C)
Theorem	cbvixp 16547	Change bound variable in an indexed Cartesian product.
|- (w e. B -> A.y w e. B)   &   |- (z e. C -> A.x z e. C)   &   |- (x = y -> B = C)   =>   |- X_x e. A B = X_y e. A C
Theorem	cbvixpv 16548	Change bound variable in an indexed Cartesian product.
|- (x = y -> B = C)   =>   |- X_x e. A B = X_y e. A C
Theorem	hbixp1 16549	The index variable in an indexed cross product is not free.
|- (y e. X_x e. A B -> A.x y e. X_x e. A B)
Theorem	ixpssmapg 16550	An infinite Cartesian product is a subset of set exponentiation.
|- ((A e. C /\ A.x e. A B e. D) -> X_x e. A B C_ (U_x e. A B ^m A))
Theorem	mapfi 16551	Set exponentiation of finite sets is finite.
|- ((A e. Fin /\ B e. Fin) -> (A ^m B) e. Fin)
Theorem	ixpfi 16552	A cross product of finitely many finite sets is finite.
|- ((A e. Fin /\ A.x e. A B e. Fin) -> X_x e. A B e. Fin)
Theorem	upixp 16553	Universal property of the indexed Cartesian product.
|- X = X_b e. A (C` b)   &   |- P = {<.w, z>. | (w e. A /\ z = {<.x, y>. | (x e. X /\ y = (x` w))})}   =>   |- ((A e. R /\ B e. S /\ A.a e. A (F` a):B-->(C` a)) -> E!h(h:B-->X /\ A.a e. A (F` a) = ((P` a) o. h)))
Theorem	erthdmg 16554	Equality of equivalence classes.
|- ((B e. C /\ Er R /\ A e. dom R) -> ([A]R = [B]R <-> ARB))
Theorem	ecelqsg 16555	Membership of an equivalence class in a quotient set.
|- ((R e. C /\ B e. A) -> [B]R e. (A/.R))
Theorem	eroprlem 16556	Lemma for eroprv 16558 and eroprf 16559. [Auxiliary lemma - not displayed.]
Theorem	eropreu 16557	Lemma for eroprv 16558 and eroprf 16559. [Auxiliary lemma - not displayed.]
Theorem	eroprv 16558	The value of an operation defined on equivalence classes.
|- J = (A/.R)   &   |- K = (B/.S)   &   |- (ph -> T e. Z)   &   |- (ph -> Er R)   &   |- (ph -> Er S)   &   |- (ph -> Er T)   &   |- (ph -> A C_ dom R)   &   |- (ph -> B C_ dom S)   &   |- (ph -> C C_ dom T)   &   |- (ph -> F:(A X. B)-->C)   &   |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> ((rRs /\ tSu) -> (rFt)T(sFu)))   &   |- G = {<.<.x, y>., z>. | E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T)}   &   |- (ph -> R e. X)   &   |- (ph -> S e. Y)   =>   |- ((ph /\ P e. A /\ Q e. B) -> ([P]RG[Q]S) = [(PFQ)]T)
Theorem	eroprf 16559	Functionality of an operation defined on equivalence classes.
|- J = (A/.R)   &   |- K = (B/.S)   &   |- (ph -> T e. Z)   &   |- (ph -> Er R)   &   |- (ph -> Er S)   &   |- (ph -> Er T)   &   |- (ph -> A C_ dom R)   &   |- (ph -> B C_ dom S)   &   |- (ph -> C C_ dom T)   &   |- (ph -> F:(A X. B)-->C)   &   |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> ((rRs /\ tSu) -> (rFt)T(sFu)))   &   |- G = {<.<.x, y>., z>. | E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T)}   &   |- (ph -> R e. X)   &   |- (ph -> S e. Y)   &   |- L = (C/.T)   =>   |- (ph -> G:(J X. K)-->L)
Theorem	eroprv2 16560	The value of an operation defined on equivalence classes.
|- J = (A/.R)   &   |- G = {<.<.x, y>., z>. | E.p e. A E.q e. A ((x = [p]R /\ y = [q]R) /\ z = [(pFq)]R)}   &   |- (ph -> R e. X)   &   |- (ph -> Er R)   &   |- (ph -> A C_ dom R)   &   |- (ph -> F:(A X. A)-->A)   &   |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. A /\ u e. A))) -> ((rRs /\ tRu) -> (rFt)R(sFu)))   =>   |- ((ph /\ P e. A /\ Q e. A) -> ([P]RG[Q]R) = [(PFQ)]R)
Theorem	eroprf2 16561	Functionality of an operation defined on equivalence classes.
|- J = (A/.R)   &   |- G = {<.<.x, y>., z>. | E.p e. A E.q e. A ((x = [p]R /\ y = [q]R) /\ z = [(pFq)]R)}   &   |- (ph -> R e. X)   &   |- (ph -> Er R)   &   |- (ph -> A C_ dom R)   &   |- (ph -> F:(A X. A)-->A)   &   |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. A /\ u e. A))) -> ((rRs /\ tRu) -> (rFt)R(sFu)))   =>   |- (ph -> G:(J X. J)-->J)
Theorem	abrexex2gOLD 16562	Existence of an existentially restricted class abstraction. (Moved to abrexex2g 4932 in main set.mm and may be deleted by mathbox owner, JM. --NM 21-May-2012.)
|- ((A e. B /\ A.x e. A {y | ph} e. C) -> {y | E.x e. A ph} e. _V)
Theorem	abrexdom 16563	An indexed set is dominated by the indexing set.
|- (y e. A -> E*xph)   =>   |- (A e. V -> {x | E.y e. A ph} ~<_ A)
Theorem	abrexdom2 16564	An indexed set is dominated by the indexing set.
|- (A e. C -> {x | E.y e. A x = B} ~<_ A)
Theorem	firnfi 16565	A set indexed by a finite set is finite.
|- (y e. A -> E*xph)   =>   |- (A e. Fin -> {x | E.y e. A ph} e. Fin)
Theorem	firnfi2 16566	A set indexed by a finite set is finite.
|- (A e. Fin -> {x | E.y e. A x = B} e. Fin)
Theorem	firnfi3 16567	A set indexed by a finite set is finite.
|- (ph -> E*xps)   =>   |- ({y | ph} e. Fin -> {x | E.y(ph /\ ps)} e. Fin)
Theorem	firnfi4 16568	A set indexed by a finite set is finite.
|- ({y | ph} e. Fin -> {x | E.y(ph /\ x = A)} e. Fin)
Theorem	findcard2OLD 16569	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 5844 in main set.mm and may be deleted by mathbox owner, JM. --NM 30-Nov-2012.)
|- (x = (/) -> (ph <-> ps))   &   |- (x = y -> (ph <-> ch))   &   |- (x = (y u. {z}) -> (ph <-> th))   &   |- (x = A -> (ph <-> ta))   &   |- ps   &   |- (y e. Fin -> (ch -> th))   =>   |- (A e. Fin -> ta)
Theorem	fimaxOLD 16570	A finite set has a maximum under a total order. (Moved to fimax 5846 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- R Or A   =>   |- ((A e. Fin /\ A =/= (/)) -> E.x e. A A.y e. A (x =/= y -> yRx))
Theorem	fimaxgOLD 16571	A finite set has a maximum under a total order. (Moved to fimaxg 5847 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- ((R Or A /\ A e. Fin /\ A =/= (/)) -> E.x e. A A.y e. A (x =/= y -> yRx))
Theorem	fisupgOLD 16572	Lemma showing existence and closure of supremum of a finite set. (Moved to fisupg 5848 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- ((R Or A /\ A e. Fin /\ A =/= (/)) -> E.x e. A (A.y e. A -. xRy /\ A.y e. A (yRx -> E.z e. A yRz)))
Theorem	ac6gf 16573	Axiom of Choice.
|- (ps -> A.yps)   &   |- (y = (f` x) -> (ph <-> ps))   =>   |- ((A e. C /\ A.x e. A E.y e. B ph) -> E.f(f:A-->B /\ A.x e. A ps))
Theorem	acdcg 16574	Dependent choice.
|- ((A e. B /\ A =/= (/) /\ F:A-->(~PA \ {(/)})) -> E.g(g:NN-->A /\ A.k e. NN (g` (k + 1)) e. (F` (g` k))))
Theorem	acdc3g 16575	Dependent choice.
|- ((A e. B /\ F:A-->(~PA \ {(/)}) /\ C e. A) -> E.g(g:NN-->A /\ (g` 1) = C /\ A.k e. NN (g` (k + 1)) e. (F` (g` k))))
Theorem	acdc5g 16576	Dependent choice.
|- ((A e. B /\ F:(NN X. A)-->(~PA \ {(/)}) /\ C e. A) -> E.g(g:NN-->A /\ (g` 1) = C /\ A.k e. NN (g` (k + 1)) e. ((k + 1)F(g` k))))
Theorem	indexa 16577	If for every element of an indexing set A there exists a corresponding element of another set B, then there exists a subset of B consisting only of those elements which are indexed by A. Used to avoid the Axiom of Choice in situations where only the range of the choice function is needed.
|- ((B e. M /\ A.x e. A E.y e. B ph) -> E.c(c C_ B /\ A.x e. A E.y e. c ph /\ A.y e. c E.x e. A ph))
Theorem	indexdom 16578	If for every element of an indexing set A there exists a corresponding element of another set B, then there exists a subset of B consisting only of those elements which are indexed by A, and which is dominated by the set A.
|- ((A e. M /\ A.x e. A E.y e. B ph) -> E.c((c ~<_ A /\ c C_ B) /\ (A.x e. A E.y e. c ph /\ A.y e. c E.x e. A ph)))
Theorem	indexfiOLD 16579	If for every element of a finite indexing set A there exists a corresponding element of another set B, then there exists a finite subset of B consisting only of those elements which are indexed by A. Proven without the Axiom of Choice, unlike indexdom 16578. (Moved to indexfi 5878 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Apr-2012.)
|- ((A e. Fin /\ B e. M /\ A.x e. A E.y e. B ph) -> E.c e. Fin (c C_ B /\ A.x e. A E.y e. c ph /\ A.y e. c E.x e. A ph))
Theorem	fipreimaOLD 16580	Given a finite subset A of the range of a function, there exists a finite subset of the domain whose image is A. (Moved to fipreima 5879 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Apr-2012.)
|- (((F Fn B /\ B e. M) /\ (A C_ ran F /\ A e. Fin)) -> E.c e. (~PB i^i Fin)(F"c) = A)
Theorem	inficl 16581	A set which is closed under pairwise intersection is closed under finite intersection.
|- ((A e. V /\ A.x e. A A.y e. A (x i^i y) e. A) -> ( fi ` A) = A)
Theorem	frinfm 16582	A subset of a well founded set has an infimum.
|- ((R Fr A /\ (B e. C /\ B C_ A /\ B =/= (/))) -> E.x e. A (A.y e. B -. x`'Ry /\ A.y e. A (y`'Rx -> E.z e. B y`'Rz)))
Theorem	welb 16583	A non-empty subset of a well ordered set has a lower bound.
|- ((R We A /\ (B e. C /\ B C_ A /\ B =/= (/))) -> (`'R Or B /\ E.x e. B (A.y e. B -. x`'Ry /\ A.y e. B (y`'Rx -> E.z e. B y`'Rz))))
Theorem	supeq2 16584	Equality theorem for supremum.
|- (B = C -> sup(A, B, R) = sup(A, C, R))
Theorem	supex2g 16585	Existence of supremum.
|- (A e. C -> sup(B, A, R) e. _V)
Theorem	supclt 16586	Closure of supremum.
|- ((R Or A /\ E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) -> sup(B, A, R) e. A)
Theorem	supubt 16587	Upper bound property of supremum.
|- ((R Or A /\ E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) -> (C e. B -> -. sup(B, A, R)RC))
Theorem	zornn0 16588	Variant of Zorn's lemma zorn 6370 in which (/), the union of the empty chain, is not required to be an element of A.
|- A e. _V   =>   |- ((A =/= (/) /\ A.z((z C_ A /\ z =/= (/) /\ A.x e. z A.y e. z (x C_ y \/ y C_ x)) -> U.z e. A)) -> E.x e. A A.y e. A -. x C. y)
Theorem	infmrlb 16589	A member of a non-empty bounded set of reals is greater than or equal to the set's lower bound.
|- (((A C_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A x <_ y) /\ B e. A) -> sup(A, RR, `' < ) <_ B)
Theorem	infmrgelb 16590	The infimum of a non-empty bounded set of reals is greater than or equal to a lower bound.
|- (((A C_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A x <_ y) /\ (B e. RR /\ A.z e. A B <_ z)) -> B <_ sup(A, RR, `' < ))
Theorem	supeutOLD 16591	A supremum is unique. Closed version of supeu 5897. (Moved to supeut 5907 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- ((R Or A /\ E.x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz))) -> E!x e. A (A.y e. B -. xRy /\ A.y e. A (yRx -> E.z e. B yRz)))
Theorem	fisup2gOLD 16592	A nonempty finite set contains its supremum. (Moved to fisup2g 5908 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- ((R Or A /\ (B e. Fin /\ B =/= (/) /\ B C_ A)) -> sup(B, A, R) e. B)
Theorem	fimax2gOLD 16593	A finite set has a maximum under a total order. (Moved to fimax2g 5849 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- ((R Or A /\ A e. Fin /\ A =/= (/)) -> E.x e. A A.y e. A -. xRy)
Theorem	wofiOLD 16594	A total order on a finite set is a well order. (Moved to wofi 5850 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- ((R Or A /\ A e. Fin) -> R We A)
Theorem	frfiOLD 16595	A partial order is founded on a finite set. (Moved to frfi 5851 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- ((R Po A /\ A e. Fin) -> R Fr A)
Theorem	pofunOLD 16596	A function preserves a partial order relation. (Moved to pofun 3763 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- S = {<.x, y>. | XRY}   &   |- (x = y -> X = Y)   =>   |- ((R Po B /\ A.x e. A X e. B) -> S Po A)
Theorem	frminexOLD 16597	If an element of a founded set satisfies a property ph, then there is a minimal element that satisfies ph. (Moved to frminex 3792 in main set.mm and may be deleted by mathbox owner, JM. --NM 16-Mar-2013.)
|- A e. _V   &   |- (x = y -> (ph <-> ps))   =>   |- (R Fr A -> (E.x e. A ph -> E.x e. A (ph /\ A.y e. A (ps -> -. yRx))))
Real and complex numbers; integers
Theorem	fimaxre 16598	A finite set of real numbers has a maximum.
|- ((A C_ RR /\ A e. Fin /\ A =/= (/)) -> E.x e. A A.y e. A y <_ x)
Theorem	fimaxre2 16599	A nonempty finite set of real numbers has a maximum.
|- ((A C_ RR /\ A e. Fin /\ A =/= (/)) -> E.x e. RR A.y e. A y <_ x)
Theorem	filbcmb 16600	Combine a finite set of lower bounds.
|- ((A e. Fin /\ A =/= (/) /\ B C_ RR) -> (A.x e. A E.y e. B A.z e. B (y <_ z -> ph) -> E.y e. B A.z e. B (y <_ z -> A.x e. A ph)))