mmtheorems148 - 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-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19465

Statement List for Metamath Proof Explorer - 14701-14800 - Page 148 of 195

Type	Label	Description
Statement
Properties of relationships
Theorem	elresOLD 14701	Membership in a restriction. (Moved into main set.mm as elres 4400 and may be deleted by mathbox owner, SF. --NM 16-Mar-2013.)
|- (A e. (B |` C) <-> E.x e. C E.y(A = <.x, y>. /\ <.x, y>. e. B))
Theorem	elsnresOLD 14702	Memebership in restriction to a singleton. (Moved into main set.mm as elsnres 4401 and may be deleted by mathbox owner, SF. --NM 16-Mar-2013.)
|- C e. _V   =>   |- (A e. (B |` {C}) <-> E.y(A = <.C, y>. /\ <.C, y>. e. B))
Theorem	epelcNEW 14703	The epsilon relationship and the membership relation are the same.
|- B e. _V   =>   |- (A _E B <-> A e. B)
Theorem	epelg 14704	The epsilon relation and membership are the same. General version of epel 3778.
|- (B e. V -> (A _E B <-> A e. B))
Theorem	brtp 14705	A condition for a binary relation over an unordered triple.
|- X e. _V   &   |- Y e. _V   &   |- B e. _V   &   |- D e. _V   &   |- F e. _V   =>   |- (X{<.A, B>., <.C, D>., <.E, F>.}Y <-> ((X = A /\ Y = B) \/ (X = C /\ Y = D) \/ (X = E /\ Y = F)))
Theorem	frirrc 14706	A founded relation is irreflexive. Special case of Proposition 6.23 of [TakeutiZaring] p. 30.
|- ((R Fr A /\ X e. A) -> -. XRX)
Theorem	dftr6 14707	A potential definition of transitivity for sets.
|- A e. _V   =>   |- (Tr A <-> A e. (_V \ ran (( _E o. _E ) \ _E )))
Theorem	coep 14708	Composition with epsilon.
|- A e. _V   &   |- B e. _V   =>   |- (A( _E o. R)B <-> E.x e. B ARx)
Theorem	coepr 14709	Composition with the converse of epsilon.
|- A e. _V   &   |- B e. _V   =>   |- (A(R o. `' _E )B <-> E.x e. A xRB)
Theorem	dffr5 14710	A quantifier free definition of a founded relationship.
|- (R Fr A <-> (~PA \ {(/)}) C_ ran ( _E \ ( _E o. `'R)))
Theorem	dfso2 14711	Quantifier free definition of a strict order.
|- (R Or A <-> (R Po A /\ (A X. A) C_ (R u. ( _I u. `'R))))
Theorem	dfpo2 14712	Quantifier free definition of a partial ordering.
|- (R Po A <-> ((R i^i ( _I |` A)) = (/) /\ ((R i^i (A X. A)) o. (R i^i (A X. A))) C_ R))
Properties of functions and mappings
Theorem	funpsstri 14713	A condition for subset trichotomy for functions.
|- ((Fun H /\ (F C_ H /\ G C_ H) /\ (dom F C_ dom G \/ dom G C_ dom F)) -> (F C. G \/ F = G \/ G C. F))
Theorem	fundmpss 14714	If a class F is a proper subset of a function G, then dom F C. dom G.
|- (Fun G -> (F C. G -> dom F C. dom G))
Theorem	fvrn0 14715	A function value is a member of the range plus null.
|- (Fun A -> (A` X) e. (ran A u. {(/)}))
Theorem	eqfunfv 14716	Equality of functions is determined by their values.
|- ((Fun F /\ Fun G) -> (F = G <-> (dom F = dom G /\ A.x e. dom F(F` x) = (G` x))))
Theorem	fresin 14717	An identity for the mapping relationship under restriction.
|- (F:A-->B -> (F |` X):(A i^i X)-->B)
Theorem	fvresval 14718	The value of a function at a restriction is either null or the same as the function itself.
|- (((F |` B)` A) = (F` A) \/ ((F |` B)` A) = (/))
Theorem	rnoprab2 14719	The range of a restricted operation class abstraction.
|- ran {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} = {z | E.x e. A E.y e. B ph}
Theorem	mpt2fun 14720	The maps-to notation for an operation is always a function.
|- F = (x e. A, y e. B |-> C)   =>   |- Fun F
Theorem	mptrel 14721	The maps-to notation always describes a relationship.
|- Rel (x e. A |-> B)
Theorem	funsseq 14722	Given two functions with equal domains, equality only requires one direction of the subset relationship.
|- ((Fun F /\ Fun G /\ dom F = dom G) -> (F = G <-> F C_ G))
Theorem	fununiq 14723	The uniqueness condition of functions.
|- A e. _V   &   |- B e. _V   &   |- C e. _V   =>   |- (Fun F -> ((AFB /\ AFC) -> B = C))
Theorem	funbreq 14724	An equality condition for functions.
|- A e. _V   &   |- B e. _V   &   |- C e. _V   =>   |- ((Fun F /\ AFB) -> (AFC <-> B = C))
Epsilon induction
Theorem	setinds 14725	Principle of _E induction (set induction). If a property passes from all elements of x to x itself, then it holds for all x.
|- (A.y e. x [y / x]ph -> ph)   =>   |- ph
Theorem	setinds2f 14726	_E induction schema, using implicit substitution.
|- (ps -> A.xps)   &   |- (x = y -> (ph <-> ps))   &   |- (A.y e. x ps -> ph)   =>   |- ph
Theorem	setinds2 14727	_E induction schema, using implicit substitution.
|- (x = y -> (ph <-> ps))   &   |- (A.y e. x ps -> ph)   =>   |- ph
Ordinal numbers
Theorem	elpotr 14728	A class of transitive sets is partially ordered by _E.
|- (A.z e. A Tr z -> _E Po A)
Theorem	dford3 14729	Given ax-reg 5972, an ordinal is a transitive class totally ordered by epsilon.
|- (Ord A <-> (Tr A /\ _E Or A))
Theorem	dfon2lem1 14730	Lemma for dfon2 14739. [Auxiliary lemma - not displayed.]
Theorem	dfon2lem2 14731	Lemma for dfon2 14739 [Auxiliary lemma - not displayed.]
Theorem	dfon2lem3 14732	Lemma for dfon2 14739. All sets satisfying the new definition are transitive and untangled. [Auxiliary lemma - not displayed.]
Theorem	dfon2lem4 14733	Lemma for dfon2 14739. If two sets satisfy the new definition, then one is a subset of the other. [Auxiliary lemma - not displayed.]
Theorem	dfon2lem5 14734	Lemma for dfon2 14739. Two sets satisfying the new definition also satisfy trichotomy with respect to e. [Auxiliary lemma - not displayed.]
Theorem	dfon2lem6 14735	Lemma for dfon2 14739. A transitive class of sets satisfying the new definition satisfies the new definition. [Auxiliary lemma - not displayed.]
Theorem	dfon2lem7 14736	Lemma for dfon2 14739. All elements of a new ordinal are new ordinals. [Auxiliary lemma - not displayed.]
Theorem	dfon2lem8 14737	Lemma for dfon2 14739. The intersection of a non-empty class A of new ordinals is itself a new ordinal and is contained within A [Auxiliary lemma - not displayed.]
Theorem	dfon2lem9 14738	Lemma for dfon2 14739. A class of new ordinals is well-founded by _E. [Auxiliary lemma - not displayed.]
Theorem	dfon2 14739	On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers," American Mathematical Monthly, vol 67 (1960), pp. 51-52.
|- On = {x | A.y((y C. x /\ Tr y) -> y e. x)}
Theorem	domep 14740	The domain of the epsilon relation is the universe.
|- dom _E = _V
Theorem	2on0 14741	Ordinal two is not zero.
|- 2o =/= (/)
Theorem	ordsucuniel 14742	Given an element A of the union of an ordinal B, suc A is an element of B itself.
|- (Ord B -> (A e. U.B <-> suc A e. B))
Theorem	nnacli 14743	om is closed under addition. Inference form of nnacl 5487.
|- A e. om   &   |- B e. om   =>   |- (A +o B) e. om
Theorem	nnmcli 14744	om is closed under multiplication. Inference form of nnmcl 5488.
|- A e. om   &   |- B e. om   =>   |- (A .o B) e. om
Theorem	omssadd 14745	Adding to both sides of an inequality in om
|- ((A e. om /\ B e. om /\ C e. om) -> (A C_ B -> (A +o C) C_ (B +o C)))
Theorem	onm2 14746	Multiply an ordinal by 2o
|- (A e. On -> (A .o 2o) = (A +o A))
Theorem	omm2 14747	Multiply an element of om by 2o
|- (A e. om -> (2o .o A) = (A +o A))
Theorem	omopthlem1 14748	Lemma for omopthi 14750. [Auxiliary lemma - not displayed.]
Theorem	omopthlem2 14749	Lemma for omopthi 14750. [Auxiliary lemma - not displayed.]
Theorem	omopthi 14750	An ordered pair theorem for om. Theorem 17.3 of [Quine] p. 124. This proof is adapted from nn0opthi 8416.
|- A e. om   &   |- B e. om   &   |- C e. om   &   |- D e. om   =>   |- ((((A +o B) .o (A +o B)) +o B) = (((C +o D) .o (C +o D)) +o D) <-> (A = C /\ B = D))
Theorem	omopth 14751	An ordered pair theorem for finite integers. Analagous to nn0opthi 8416.
|- (((A e. om /\ B e. om) /\ (C e. om /\ D e. om)) -> ((((A +o B) .o (A +o B)) +o B) = (((C +o D) .o (C +o D)) +o D) <-> (A = C /\ B = D)))
Defined equality axioms
Theorem	axextdfeq 14752	A version of ax-ext 2152 for use with defined equality.
|- E.z((z e. x -> z e. y) -> ((z e. y -> z e. x) -> (x e. w -> y e. w)))
Theorem	ax13dfeq 14753	A version of ax-13 1628 for use with defined equality.
|- E.z((z e. x -> z e. y) -> (w e. x -> w e. y))
Theorem	axextdist 14754	ax-ext 2152 with distinctors instead of distinct variable restrictions.
|- ((-. A.z z = x /\ -. A.z z = y) -> (A.z(z e. x <-> z e. y) -> x = y))
Theorem	axext4dist 14755	axext4 2155 with distinctors instead of distinct variable restrictions.
|- ((-. A.z z = x /\ -. A.z z = y) -> (x = y <-> A.z(z e. x <-> z e. y)))
Theorem	19.12b 14756	19.12vv 1979 with not-free hypotheses, instead of distinct variable conditions.
|- (ph -> A.yph)   &   |- (ps -> A.xps)   =>   |- (E.xA.y(ph -> ps) <-> A.yE.x(ph -> ps))
Theorem	exnel 14757	There is always a set not in y.
|- E.x -. x e. y
Theorem	distel 14758	Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 3685 and elirrv 5977.)
|- (-. A.y y = x <-> -. A.y -. x e. y)
Theorem	axextndbi 14759	axextnd 6538 as a biconditional.
|- E.z(x = y <-> (z e. x <-> z e. y))
Hypothesis builders
Theorem	hbntg 14760	A more general form of hbnt 1667.
|- (A.x(ph -> A.xps) -> (-. ps -> A.x -. ph))
Theorem	hbimtg 14761	A more general and closed form of hbim 1672.
|- ((A.x(ph -> A.xch) /\ (ps -> A.xth)) -> ((ch -> ps) -> A.x(ph -> th)))
Theorem	hbaltg 14762	A more general and closed form of hbal 1670.
|- (A.x(ph -> A.yps) -> (A.xph -> A.yA.xps))
Theorem	hbng 14763	A more general form of hbn 1669.
|- (ph -> A.xps)   =>   |- (-. ps -> A.x -. ph)
Theorem	hbimg 14764	A more general form of hbim 1672.
|- (ph -> A.xps)   &   |- (ch -> A.xth)   =>   |- ((ps -> ch) -> A.x(ph -> th))
Theorem	elrn2g 14765	Membership in a range.
|- (A e. V -> (A e. ran B <-> E.x<.x, A>. e. B))
Theorem	elrng 14766	Membership in a range.
|- (A e. V -> (A e. ran B <-> E.x xBA))
The Predecessor Class
Syntax	cpred 14767	The predecessors symbol.
class Pred(R, A, X)
Definition	df-pred 14768	Define the predecessor class of a relationship. This is the class of all elements y of A such that yRX (see elpred 14777) .
|- Pred(R, A, X) = (A i^i (`'R"{X}))
Theorem	predeq1 14769	Equality theorem for the predecessor class.
|- (R = S -> Pred(R, A, X) = Pred(S, A, X))
Theorem	predeq2 14770	Equality theorem for the predecessor class.
|- (A = B -> Pred(R, A, X) = Pred(R, B, X))
Theorem	predeq3 14771	Equality theorem for the predecessor class.
|- (X = Y -> Pred(R, A, X) = Pred(R, A, Y))
Theorem	predpredss 14772	If A is a subset of B, then their predecessor classes are also subsets.
|- (A C_ B -> Pred(R, A, X) C_ Pred(R, B, X))
Theorem	predss 14773	The predecessor class of A is a subset of A
|- Pred(R, A, X) C_ A
Theorem	sspred 14774	Another subset/predecessor class relationship.
|- ((B C_ A /\ Pred(R, A, X) C_ B) -> Pred(R, A, X) = Pred(R, B, X))
Theorem	dfpred2 14775	An alternate definition of predecessor class when X is a set.
|- X e. _V   =>   |- Pred(R, A, X) = (A i^i {y | yRX})
Theorem	elpredim 14776	Membership in a predecessor class - implicative version.
|- X e. _V   =>   |- (Y e. Pred(R, A, X) -> YRX)
Theorem	elpred 14777	Membership in a predecessor class.
|- Y e. _V   =>   |- (X e. D -> (Y e. Pred(R, A, X) <-> (Y e. A /\ YRX)))
Theorem	elpredg 14778	Membership in a predecessor class.
|- ((X e. B /\ Y e. A) -> (Y e. Pred(R, A, X) <-> YRX))
Theorem	predreseq 14779	Equality of restriction to predecessor classes.
|- X e. _V   =>   |- ((F Fn A /\ G Fn A) -> ((F |` Pred(R, A, X)) = (G |` Pred(R, A, X)) <-> A.y e. A (yRX -> (F` y) = (G` y))))
Theorem	predasetex 14780	The predecessor class exists when A does.
|- A e. _V   =>   |- Pred(R, A, X) e. _V
Theorem	cbvsetlike 14781	Change the bound variable in the statement stating that R is set-like.
|- (A.x e. A Pred(R, A, x) e. _V <-> A.y e. A Pred(R, A, y) e. _V)
Theorem	dffr4 14782	Alternate definition of founded relation.
|- (R Fr A <-> A.x((x C_ A /\ x =/= (/)) -> E.y e. x Pred(R, x, y) = (/)))
Theorem	predel 14783	Membership in the predecessor class implies membership in the base class.
|- (Y e. Pred(R, A, X) -> Y e. A)
Theorem	predpo 14784	Property of the precessor class for partial orderings.
|- ((R Po A /\ X e. A) -> (Y e. Pred(R, A, X) -> Pred(R, A, Y) C_ Pred(R, A, X)))
Theorem	predso 14785	Property of the predecessor class for strict orderings.
|- ((R Or A /\ X e. A) -> (Y e. Pred(R, A, X) -> Pred(R, A, Y) C_ Pred(R, A, X)))
Theorem	predbr 14786	If a set is in the predecessor class, then it is less than the base element.
|- X e. _V   &   |- Y e. _V   =>   |- (Y e. Pred(R, A, X) -> YRX)
Theorem	predbrg 14787	Closed form of predbr 14786.
|- ((X e. A /\ Y e. B) -> (Y e. Pred(R, A, X) -> YRX))
Theorem	setlikespec 14788	If R is set-like in A then all predecessors classes of elements of A exist.
|- ((X e. A /\ A.x e. A Pred(R, A, x) e. _V) -> Pred(R, A, X) e. _V)
Theorem	predidm 14789	Idempotent law for the predecessor class.
|- Pred(R, Pred(R, A, X), X) = Pred(R, A, X)
Theorem	predin 14790	Intersection law for predecessor classes.
|- Pred(R, (A i^i B), X) = (Pred(R, A, X) i^i Pred(R, B, X))
Theorem	predun 14791	Union law for predecessor classes.
|- Pred(R, (A u. B), X) = (Pred(R, A, X) u. Pred(R, B, X))
Theorem	preddif 14792	Difference law for predecessor classes.
|- Pred(R, (A \ B), X) = (Pred(R, A, X) \ Pred(R, B, X))
Theorem	predep 14793	The predecessor under the epsilon relationship is equivalent to an intersection. (The proof was shortened by Andrew Salmon, 27-Aug-2011.)
|- (X e. B -> Pred( _E , A, X) = (A i^i X))
Theorem	predon 14794	For an ordinal, the predecessor under _E and On is an identity relationship.
|- (A e. On -> Pred( _E , On, A) = A)
Theorem	epsetlike 14795	The epsilon relationship is set-like.
|- A.x e. A Pred( _E , A, x) e. _V
Theorem	setlikess 14796	If R is set-like over A, then it is set-like over any subclass of A.
|- ((A C_ B /\ A.x e. B Pred(R, B, x) e. _V) -> A.x e. A Pred(R, A, x) e. _V)
Theorem	preddowncl 14797	A property of classes that are downward closed under predecessor.
|- ((B C_ A /\ A.x e. B Pred(R, A, x) C_ B) -> (X e. B -> Pred(R, B, X) = Pred(R, A, X)))
Theorem	predpoirr 14798	Given a partial ordering, X is not a member of its predecessor class.
|- (R Po A -> -. X e. Pred(R, A, X))
Theorem	predfrirr 14799	Given a founded relationship, X is not a member of its predecessor class.
|- (R Fr A -> -. X e. Pred(R, A, X))
Theorem	pred0 14800	The predecessor class over (/) is always (/)
|- Pred(R, (/), X) = (/)