mmtheorems46 - 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-12326

Statement List for Metamath Proof Explorer - 4501-4600 - Page 46 of 124

Type	Label	Description
Statement
Theorem	th3q 4501	Theorem 3Q of [Enderton] p. 60, extended to operations on ordered pairs.
|- R e. V   &   |- Er R   &   |- dom R = (S X. S)   &   |- ((((w e. S /\ v e. S) /\ (u e. S /\ t e. S)) /\ ((s e. S /\ f e. S) /\ (g e. S /\ h e. S))) -> ((<.w, v>.R<.u, t>. /\ <.s, f>.R<.g, h>.) -> (<.w, v>.F<.s, f>.)R(<.u, t>.F<.g, h>.)))   &   |- G = {<.<.x, y>., z>. | ((x e. ((S X. S)/.R) /\ y e. ((S X. S)/.R)) /\ E.wE.vE.uE.t((x = [<.w, v>.]R /\ y = [<.u, t>.]R) /\ z = [(<.w, v>.F<.u, t>.)]R))}   =>   |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> ([<.A, B>.]RG[<.C, D>.]R) = [(<.A, B>.F<.C, D>.)]R)
Theorem	oprec 4502	Express an operation on equivalence classes of ordered pairs in terms of equivalence class of operations on ordered pairs. (See set.mm for additional comments for the hypotheses.)
|- H e. V   &   |- K e. V   &   |- L e. V   &   |- R e. V   &   |- Er R   &   |- dom R = (S X. S)   &   |- R = {<.x, y>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.zE.wE.vE.u((x = <.z, w>. /\ y = <.v, u>.) /\ ph))}   &   |- (((z = a /\ w = b) /\ (v = c /\ u = d)) -> (ph <-> ps))   &   |- (((z = g /\ w = h) /\ (v = t /\ u = s)) -> (ph <-> ch))   &   |- G = {<.<.x, y>., z>. | ((x e. (S X. S) /\ y e. (S X. S)) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = J))}   &   |- (((w = a /\ v = b) /\ (u = g /\ f = h)) -> J = K)   &   |- (((w = c /\ v = d) /\ (u = t /\ f = s)) -> J = L)   &   |- (((w = A /\ v = B) /\ (u = C /\ f = D)) -> J = H)   &   |- F = {<.<.x, y>., z>. | ((x e. Q /\ y e. Q) /\ E.aE.bE.cE.d((x = [<.a, b>.]R /\ y = [<.c, d>.]R) /\ z = [(<.a, b>.G<.c, d>.)]R))}   &   |- Q = ((S X. S)/.R)   &   |- ((((a e. S /\ b e. S) /\ (c e. S /\ d e. S)) /\ ((g e. S /\ h e. S) /\ (t e. S /\ s e. S))) -> ((ps /\ ch) -> KRL))   =>   |- (((A e. S /\ B e. S) /\ (C e. S /\ D e. S)) -> ([<.A, B>.]RF[<.C, D>.]R) = [H]R)
Theorem	ecoprcom 4503	Lemma used to transfer a commutative law via an equivalence relation.
|- C = ((S X. S)/.R)   &   |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> ([<.x, y>.]RF[<.z, w>.]R) = [<.D, G>.]R)   &   |- (((z e. S /\ w e. S) /\ (x e. S /\ y e. S)) -> ([<.z, w>.]RF[<.x, y>.]R) = [<.H, J>.]R)   &   |- D = H   &   |- G = J   =>   |- ((A e. C /\ B e. C) -> (AFB) = (BFA))
Theorem	ecoprass 4504	Lemma used to transfer an associative law via an equivalence relation.
|- D = ((S X. S)/.R)   &   |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> ([<.x, y>.]RF[<.z, w>.]R) = [<.G, H>.]R)   &   |- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> ([<.z, w>.]RF[<.v, u>.]R) = [<.N, Q>.]R)   &   |- (((G e. S /\ H e. S) /\ (v e. S /\ u e. S)) -> ([<.G, H>.]RF[<.v, u>.]R) = [<.J, K>.]R)   &   |- (((x e. S /\ y e. S) /\ (N e. S /\ Q e. S)) -> ([<.x, y>.]RF[<.N, Q>.]R) = [<.L, M>.]R)   &   |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> (G e. S /\ H e. S))   &   |- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> (N e. S /\ Q e. S))   &   |- J = L   &   |- K = M   =>   |- ((A e. D /\ B e. D /\ C e. D) -> ((AFB)FC) = (AF(BFC)))
Theorem	ecoprdi 4505	Lemma used to transfer a distributive law via an equivalence relation.
|- D = ((S X. S)/.R)   &   |- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> ([<.z, w>.]RF[<.v, u>.]R) = [<.M, N>.]R)   &   |- (((x e. S /\ y e. S) /\ (M e. S /\ N e. S)) -> ([<.x, y>.]RG[<.M, N>.]R) = [<.H, J>.]R)   &   |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> ([<.x, y>.]RG[<.z, w>.]R) = [<.W, X>.]R)   &   |- (((x e. S /\ y e. S) /\ (v e. S /\ u e. S)) -> ([<.x, y>.]RG[<.v, u>.]R) = [<.Y, Z>.]R)   &   |- (((W e. S /\ X e. S) /\ (Y e. S /\ Z e. S)) -> ([<.W, X>.]RF[<.Y, Z>.]R) = [<.K, L>.]R)   &   |- (((z e. S /\ w e. S) /\ (v e. S /\ u e. S)) -> (M e. S /\ N e. S))   &   |- (((x e. S /\ y e. S) /\ (z e. S /\ w e. S)) -> (W e. S /\ X e. S))   &   |- (((x e. S /\ y e. S) /\ (v e. S /\ u e. S)) -> (Y e. S /\ Z e. S))   &   |- H = K   &   |- J = L   =>   |- ((A e. D /\ B e. D /\ C e. D) -> (AG(BFC)) = ((AGB)F(AGC)))
The mapping operation
Syntax	cm 4506	Extend the definition of a class to include the mapping operation. (Read for A ^m B, "the set of all functions that map from B to A.)
class ^m
Syntax	cpm 4507	Extend the definition of a class to include the partial mapping operation. (Read for A ^m B, "the set of all partial functions that map from B to A.)
class ^pm
Definition	df-map 4508	Define the mapping operation or set exponentiation. The set of all functions that map from B to A is written (A ^m B) (see mapval 4516). Many authors write A followed by B as a superscript for this operation and rely on context to avoid confusion other exponentiation operations (e.g. Definition 10.42 of [TakeutiZaring] p. 95). Other authors show B as a prefixed superscript, which is read "A pre B" (e.g. definition of [Enderton] p. 52). Definition 8.21 of [Eisenberg] p. 125 uses the notation Map(B, A) for our (A ^m B). The up-arrow is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976). We adopt the first case of his notation (simple exponentiation) and subscript it with m to distinguish it from other kinds of exponentiation.
|- ^m = {<.<.x, y>., z>. | z = {f | f:y-->x}}
Definition	df-pm 4509	Define the partial mapping operation. A partial function from B to A is a function from a subset of B to A. The set of all partial functions from B to A is written (A ^pm B) (see pmvalg 4515). A notation for this operation apparently does not appear in the literature. We use ^pm to distinguish it from the less general set exponentiation operation ^m (df-map 4508) . See mapsspm 4523 for its relationship to set exponentiation.
|- ^pm = {<.<.x, y>., z>. | z = {f | (Fun f /\ f (_ (y X. x))}}
Theorem	mapprc 4510	When A is a proper class, the class of all functions mapping A to B is empty. Exercise 4.41 of [Mendelson] p. 255.
|- (-. A e. V -> {f | f:A-->B} = (/))
Theorem	pmex 4511	The class of all partial functions from one set to another is a set.
|- ((A e. C /\ B e. D) -> {f | (Fun f /\ f (_ (A X. B))} e. V)
Theorem	mapex 4512	The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of [Kunen] p. 31. (Contributed by Raph Levien, 4-Dec-2003.)
|- ((A e. C /\ B e. D) -> {f | f:A-->B} e. V)
Theorem	fnmap 4513	Set exponentiation has a universal domain.
|- ^m Fn (V X. V)
Theorem	mapvalg 4514	The value of set exponentiation. (A ^m B) is the set of all functions that map from B to A. Definition 10.24 of [Kunen] p. 24.
|- ((A e. C /\ B e. D) -> (A ^m B) = {f | f:B-->A})
Theorem	pmvalg 4515	The value of the partial mapping operation. (A ^pm B) is the set of all partial functions that map from B to A.
|- ((A e. C /\ B e. D) -> (A ^pm B) = {f | (Fun f /\ f (_ (B X. A))})
Theorem	mapval 4516	The value of set exponentiation (inference version). (A ^m B) is the set of all functions that map from B to A. Definition 10.24 of [Kunen] p. 24.
|- A e. V   &   |- B e. V   =>   |- (A ^m B) = {f | f:B-->A}
Theorem	elmapg 4517	Membership relation for set exponentiation.
|- ((A e. R /\ B e. S) -> (C e. (A ^m B) <-> C:B-->A))
Theorem	elmap 4518	Membership relation for set exponentiation.
|- A e. V   &   |- B e. V   =>   |- (F e. (A ^m B) <-> F:B-->A)
Theorem	mapval2 4519	Alternate expression for the value of set exponentiation.
|- A e. V   &   |- B e. V   =>   |- (A ^m B) = (P~(B X. A) i^i {f | f Fn B})
Theorem	elpm 4520	The predicate "is a partial function."
|- A e. V   &   |- B e. V   =>   |- (F e. (A ^pm B) <-> (Fun F /\ F (_ (B X. A)))
Theorem	elpm2 4521	The predicate "is a partial function."
|- A e. V   &   |- B e. V   =>   |- (F e. (A ^pm B) <-> (F:dom F-->A /\ dom F (_ B))
Theorem	fpm 4522	A total function is a partial function.
|- A e. V   &   |- B e. V   =>   |- (F:A-->B -> F e. (B ^pm A))
Theorem	mapsspm 4523	Set exponentiation is a subset of partial maps.
|- A e. V   &   |- B e. V   =>   |- (A ^m B) (_ (A ^pm B)
Theorem	fvopabf4 4524	Special case of fvopab4 3934 for operator theorems.
|- C e. V   &   |- D e. V   &   |- R e. V   &   |- (x = A -> B = C)   &   |- F = {<.x, y>. | (x:D-->R /\ y = B)}   =>   |- (A:D-->R -> (F` A) = C)
Theorem	mapsspw 4525	Set exponentiation is a subset of the power set of the cross product of its arguments.
|- (B e. R -> (A ^m B) (_ P~(B X. A))
Theorem	map0e 4526	Set exponentiation with an empty exponent (ordinal number 0) is ordinal number 1. Exercise 4.42(a) of [Mendelson] p. 255.
|- A e. V   =>   |- (A ^m (/)) = 1o
Theorem	map0b 4527	Set exponentiation with an empty base is the empty set, provided the exponent is non-empty. Theorem 96 of [Suppes] p. 89.
|- A e. V   =>   |- (A =/= (/) -> ((/) ^m A) = (/))
Theorem	map0 4528	Set exponentiation is empty iff the base is empty and the exponent is not empty. Theorem 97 of [Suppes] p. 89.
|- A e. V   &   |- B e. V   =>   |- ((A ^m B) = (/) <-> (A = (/) /\ B =/= (/)))
Theorem	mapsn 4529	The value of set exponentiation with a singleton exponent. Theorem 98 of [Suppes] p. 89.
|- A e. V   &   |- B e. V   =>   |- (A ^m {B}) = {f | E.y e. A f = {<.B, y>.}}
Theorem	mapss 4530	Subset inheritance for set exponentiation. Theorem 99 of [Suppes] p. 89.
|- B e. V   &   |- C e. V   =>   |- (A (_ B -> (A ^m C) (_ (B ^m C))
Infinite Cartesian products
Syntax	cixp 4531	Extend class notation to include infinite Cartesian products.
class X_x e. A B
Definition	df-ixp 4532	Definition of infinite Cartesian product of [Enderton] p. 54. Enderton uses a bold "X" with x e. A written underneath or as a subscript, as does Stoll p. 47. Some books use a capital pi, but we will reserve that notation for products of numbers. Usually B represents a class expression containing x free and thus can be thought of as B(x). Normally, x is not free in A, although this is not a requirement of the definition.
|- X_x e. A B = {f | (f Fn A /\ A.x e. A (f` x) e. B)}
Theorem	elixp2 4533	Membership in an infinite Cartesian product. See df-ixp 4532 for discussion of the notation.
|- (F e. X_x e. A B <-> (F e. V /\ F Fn A /\ A.x e. A (F` x) e. B))
Theorem	elixp 4534	Membership in an infinite Cartesian product.
|- F e. V   =>   |- (F e. X_x e. A B <-> (F Fn A /\ A.x e. A (F` x) e. B))
Theorem	elixpconst 4535	Membership in an infinite Cartesian product of a constant B.
|- F e. V   =>   |- (F e. X_x e. A B <-> F:A-->B)
Theorem	ixpconst 4536	Infinite Cartesian product of a constant B.
|- A e. V   &   |- B e. V   =>   |- X_x e. A B = (B ^m A)
Theorem	ixpeq1 4537	Equality theorem for infinite Cartesian product.
|- (A = B -> X_x e. A C = X_x e. B C)
Theorem	ss2ixp 4538	Subclass theorem for infinite Cartesian product.
|- (A.x e. A B (_ C -> X_x e. A B (_ X_x e. A C)
Theorem	ixpeq2 4539	Equality theorem for infinite Cartesian product.
|- (A.x e. A B = C -> X_x e. A B = X_x e. A C)
Theorem	ixpf 4540	A member of an infinite Cartesian product maps to the indexed union of the product argument. Remark in [Enderton] p. 54.
|- (F e. X_x e. A B -> F:A-->U_x e. A B)
Theorem	uniixp 4541	The union of an infinite Cartesian product is included in a cross product.
|- U.X_x e. A B (_ (A X. U_x e. A B)
Theorem	ixpexg 4542	The existence of an infinite Cartesian product. x is normally a free-variable parameter in B. Remark in Enderton p. 54.
|- ((A e. C /\ A.x e. A B e. D) -> X_x e. A B e. V)
Theorem	ixp0x 4543	An infinite Cartesian product with an empty index set.
|- X_x e. (/) A = {(/)}
Theorem	0elixp 4544	Membership of the empty set in an infinite Cartesian product. (Contributed by Steve Rodriguez, 29-Sep-2006.)
|- (/) e. X_x e. (/) A
Theorem	ixp0 4545	The infinite Cartesian product of a family B(x) with an empty member is empty.
|- (E.x e. A B = (/) -> X_x e. A B = (/))
Theorem	mapixp 4546	Express set exponentiation in terms of an infinite Cartesian product. Remark in [Stoll] p. 47. Note that B is constant, i.e. x does not occur in B.
|- A e. V   &   |- B e. V   =>   |- (B ^m A) = X_x e. A B
Theorem	ixpssmap 4547	An infinite Cartesian product is a subset of set exponentation. Remark in [Enderton] p. 54.
|- A e. V   &   |- B e. V   =>   |- X_x e. A B (_ (U_x e. A B ^m A)
Equinumerosity
Syntax	cen 4548	Extend class definition to include the equinumerosity relation ("approximately equals" symbol)
class ~~
Syntax	cdom 4549	Extend class definition to include the dominance relation (curly less-than-or-equal)
class ~<_
Syntax	csdm 4550	Extend class definition to include the strict dominance relation (curly less-than)
class ~<
Syntax	cfn 4551	Extend class definition to include the class of all finite sets.
class Fin
Definition	df-en 4552	Define the equinumerosity relation. Definition of [Enderton] p. 129. We define ~~ to be a binary relation rather than a connective, so its arguments must be sets to be meaningful. This is acceptable because we do not consider equinumerosity for proper classes. We derive the usual definition as bren 4561.
|- ~~ = {<.x, y>. | E.f f:x-1-1-onto->y}
Definition	df-dom 4553	Define the dominance relation. For an alternate definition see dfdom2 4568. Compare Definition of [Enderton] p. 145. Typical textbook definitions are derived as brdom 4562 and domen 4563.
|- ~<_ = {<.x, y>. | E.f f:x-1-1->y}
Definition	df-sdom 4554	Define the strict dominance relation. Alternate possible definitions are derived as brsdom 4565 and brsdom2 4649. Definition 3 of [Suppes] p. 97.
|- ~< = ( ~<_ \ ~~ )
Definition	df-fin 4555	Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our "a e. Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 4813. If we accept Infinity, we can also express A e. Fin by A ~< om (theorem isfinite 4823.)
|- Fin = {x | E.y e. om x ~~ y}
Theorem	relen 4556	Equinumerosity is a relation.
|- Rel ~~
Theorem	reldom 4557	Dominance is a relation.
|- Rel ~<_
Theorem	relsdom 4558	Strict dominance is a relation.
|- Rel ~<
Theorem	breng 4559	Equinumerosity relation.
|- (B e. C -> (A ~~ B <-> E.f f:A-1-1-onto->B))
Theorem	brdomg 4560	Dominance relation.
|- (B e. C -> (A ~<_ B <-> E.f f:A-1-1->B))
Theorem	bren 4561	Equinumerosity relation. Compare Definition of [Enderton] p. 129.
|- B e. V   =>   |- (A ~~ B <-> E.f f:A-1-1-onto->B)
Theorem	brdom 4562	Dominance relation.
|- B e. V   =>   |- (A ~<_ B <-> E.f f:A-1-1->B)
Theorem	domen 4563	Dominance in terms of equinumerosity. Example 1 of [Enderton] p. 146.
|- B e. V   =>   |- (A ~<_ B <-> E.x(A ~~ x /\ x (_ B))
Theorem	domeng 4564	Dominance in terms of equinumerosity, with the sethood requirement expressed as an antecedent. Example 1 of [Enderton] p. 146.
|- (B e. C -> (A ~<_ B <-> E.x(A ~~ x /\ x (_ B)))
Theorem	brsdom 4565	Strict dominance relation, meaning "B is strictly greater in size than A." Definition of [Mendelson] p. 255.
|- (A ~< B <-> (A ~<_ B /\ -. A ~~ B))
Theorem	isfi 4566	Express "A is finite." Definition 10.29 of [TakeutiZaring] p. 91 (whose "Fin" is a predicate instead of a class).
|- (A e. Fin <-> E.x e. om A ~~ x)
Theorem	enssdom 4567	Equinumerosity implies dominance.
|- ~~ (_ ~<_
Theorem	dfdom2 4568	Alternate definition of dominance.
|- ~<_ = ( ~< u. ~~ )
Theorem	endom 4569	Equinumerosity implies dominance. Theorem 15 of [Suppes] p. 94.
|- (A ~~ B -> A ~<_ B)
Theorem	sdomdom 4570	Strict dominance implies dominance.
|- (A ~< B -> A ~<_ B)
Theorem	sdomnen 4571	Strict dominance implies non-equinumerosity.
|- (A ~< B -> -. A ~~ B)
Theorem	brdom2 4572	Dominance in terms of strict dominance and equinumerosity. Theorem 22(iv) of [Suppes] p. 97.
|- (A ~<_ B <-> (A ~< B \/ A ~~ B))
Theorem	bren2 4573	Equinumerosity expressed in terms of dominance and strict dominance.
|- (A ~~ B <-> (A ~<_ B /\ -. A ~< B))
Theorem	enrefg 4574	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92.
|- (A e. B -> A ~~ A)
Theorem	enref 4575	Equinumerosity is reflexive. Theorem 1 of [Suppes] p. 92.
|- A e. V   =>   |- A ~~ A
Theorem	eqeng 4576	Equality implies equinumerosity.
|- (A e. C -> (A = B -> A ~~ B))
Theorem	domrefg 4577	Dominance is reflexive.
|- (A e. B -> A ~<_ A)
Theorem	f1oen2g 4578	The domain and range of a one-to-one, onto function are equinumerous. This variation of f1oeng 4579 does not require the Axiom of Replacement.
|- ((F e. C /\ F:A-1-1-onto->B) -> A ~~ B)
Theorem	f1oeng 4579	The domain and range of a one-to-one, onto function are equinumerous.
|- ((A e. C /\ F:A-1-1-onto->B) -> A ~~ B)
Theorem	f1domg 4580	The domain of a one-to-one function is dominated by its codomain.
|- (A e. C -> (F:A-1-1->B -> A ~<_ B))
Theorem	f1dom2g 4581	The domain of a one-to-one function is dominated by its codomain.
|- (B e. C -> (F:A-1-1->B -> A ~<_ B))
Theorem	f1oen 4582	The domain and range of a one-to-one, onto function are equinumerous.
|- A e. V   =>   |- (F:A-1-1-onto->B -> A ~~ B)
Theorem	f1dom 4583	The domain of a one-to-one function is dominated by its codomain.
|- A e. V   =>   |- (F:A-1-1->B -> A ~<_ B)
Theorem	en2d 4584	Equinumerosity inference from an implicit one-to-one onto function.
|- (ph -> A e. V)   &   |- (ph -> (x e. A -> C e. V))   &   |- (ph -> (y e. B -> D e. V))   &   |- (ph -> ((x e. A /\ y = C) <-> (y e. B /\ x = D)))   =>   |- (ph -> A ~~ B)
Theorem	en3d 4585	Equinumerosity inference from an implicit one-to-one onto function.
|- (ph -> A e. V)   &   |- (ph -> (x e. A -> C e. B))   &   |- (ph -> (y e. B -> D e. A))   &   |- (ph -> ((x e. A /\ y e. B) -> (x = D <-> y = C)))   =>   |- (ph -> A ~~ B)
Theorem	en2 4586	Equinumerosity inference from an implicit one-to-one onto function.
|- A e. V   &   |- (x e. A -> C e. V)   &   |- (y e. B -> D e. V)   &   |- ((x e. A /\ y = C) <-> (y e. B /\ x = D))   =>   |- A ~~ B
Theorem	en3 4587	Equinumerosity inference from an implicit one-to-one onto function.
|- A e. V   &   |- (x e. A -> C e. B)   &   |- (y e. B -> D e. A)   &   |- ((x e. A /\ y e. B) -> (x = D <-> y = C))   =>   |- A ~~ B
Theorem	dom2d 4588	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain.
|- (ph -> (x e. A -> C e. B))   &   |- (ph -> ((x e. A /\ y e. A) -> (C = D <-> x = y)))   =>   |- (ph -> (A e. R -> A ~<_ B))
Theorem	dom2 4589	A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. C and D can be read C(x) and D(y), as can be shown from their distinct variable conditions.
|- (x e. A -> C e. B)   &   |- ((x e. A /\ y e. A) -> (C = D <-> x = y))   =>   |- (A e. R -> A ~<_ B)
Theorem	idssen 4590	Equality implies equinumerosity.
|- I (_ ~~
Theorem	dmen 4591	The domain of equinumerosity.
|- dom ~~ = V
Theorem	ssdomg 4592	A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
|- (A e. C -> (A (_ B -> A ~<_ B))
Theorem	ssdom2g 4593	A set dominates its subsets. Theorem 16 of [Suppes] p. 94.
|- (B e. C -> (A (_ B -> A ~<_ B))
Theorem	ener 4594	Equinumerosity is an equivalence relation.
|- Er ~~
Theorem	ensymg 4595	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|- (B e. C -> (A ~~ B -> B ~~ A))
Theorem	ensym 4596	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|- B e. V   =>   |- (A ~~ B -> B ~~ A)
Theorem	ensymi 4597	Symmetry of equinumerosity. Theorem 2 of [Suppes] p. 92.
|- B e. V   &   |- A ~~ B   =>   |- B ~~ A
Theorem	entr 4598	Transitivity of equinumerosity. Theorem 3 of [Suppes] p. 92.
|- ((A ~~ B /\ B ~~ C) -> A ~~ C)
Theorem	domtr 4599	Transitivity of dominance relation. Theorem 17 of [Suppes] p. 94.
|- ((A ~<_ B /\ B ~<_ C) -> A ~<_ C)
Theorem	entri 4600	A chained equinumerosity inference.
|- A ~~ B   &   |- B ~~ C   =>   |- A ~~ C