mmtheorems50 - 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-12229

Statement List for Metamath Proof Explorer - 4901-5000 - Page 50 of 123

Type	Label	Description
Statement
Theorem	ac6 4901	Equivalent of Axiom of Choice. This is useful for proving that there exists, for example, a sequence mapping natural numbers to members of a largei set B, where ph depends on x (the natural number) and y (to specify a member of B). A stronger version of this theorem, ac6s 4902, allows B to be a proper class.
|- A e. V   &   |- B e. V   &   |- (y = (f` x) -> (ph <-> ps))   =>   |- (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps))
Theorem	ac6s 4902	Equivalent of Axiom of Choice. Using the Boundedness Axiom bnd2 4870, we derive this strong version of ac6 4901 that doesn't require B to be a set.
|- A e. V   &   |- (y = (f` x) -> (ph <-> ps))   =>   |- (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps))
Theorem	ac6n 4903	Equivalent of Axiom of Choice. Contrapositive of ac6s 4902.
|- A e. V   &   |- (y = (f` x) -> (ph <-> ps))   =>   |- (A.f(f:A-->B -> E.x e. A ps) -> E.x e. A A.y e. B ph)
Theorem	ac6s2 4904	Generalization of the Axiom of Choice to classes. Slightly strengthened version of ac6s3 4905.
|- A e. V   &   |- (y = (f` x) -> (ph <-> ps))   =>   |- (A.x e. A E.yph -> E.f(f Fn A /\ A.x e. A ps))
Theorem	ac6s3 4905	Generalization of the Axiom of Choice to classes. Theorem 10.46 of [TakeutiZaring] p. 97.
|- A e. V   &   |- (y = (f` x) -> (ph <-> ps))   =>   |- (A.x e. A E.yph -> E.fA.x e. A ps)
Theorem	ac6sf 4906	Version of ac6 4901 with bound-variable hypothesis.
|- (ps -> A.yps)   &   |- A e. V   &   |- (y = (f` x) -> (ph <-> ps))   =>   |- (A.x e. A E.y e. B ph -> E.f(f:A-->B /\ A.x e. A ps))
Theorem	ac6s4 4907	Generalization of the Axiom of Choice to proper classes. B is a collection B(x) of nonempty, possible proper classes.
|- A e. V   =>   |- (A.x e. A B =/= (/) -> E.f(f Fn A /\ A.x e. A (f` x) e. B))
Theorem	ac6s5 4908	Generalization of the Axiom of Choice to proper classes. B is a collection B(x) of nonempty, possible proper classes. Remark after Theorem 10.46 of [TakeutiZaring] p. 98.
|- A e. V   =>   |- (A.x e. A B =/= (/) -> E.fA.x e. A (f` x) e. B)
Theorem	ac8 4909	An Axiom of Choice equivalent. Given a family x of mutually disjoint nonempty sets, there exists a set y containing exactly one member from each set in the family. Theorem 6M(4) of [Enderton] p. 151.
|- ((A.z e. x z =/= (/) /\ A.z e. x A.w e. x (z =/= w -> (z i^i w) = (/))) -> E.yA.z e. x E!v v e. (z i^i y))
Theorem	ac9s 4910	An Axiom of Choice equivalent: the infinite Cartesian product of nonempty classes is nonempty. Axiom of Choice (second form) of [Enderton] p. 55 and its converse. This is a stronger version of the axiom in Enderton, with no existence requirement for the family of classes B(x) (achieved via the Collection Principle cp 4868).
|- A e. V   =>   |- (A.x e. A B =/= (/) <-> X_x e. A B =/= (/))
Theorem	kmlem1 4911	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, 1 => 2.
Theorem	kmlem2 4912	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4.
Theorem	kmlem3 4913	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4. The right-hand side is part of the hypothesis of 4.
Theorem	kmlem4 4914	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4.
Theorem	kmlem5 4915	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4.
Theorem	kmlem6 4916	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1.
Theorem	kmlem7 4917	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1.
Theorem	kmlem8 4918	Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4.
Theorem	kmlem9 4919	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4.
Theorem	kmlem10 4920	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4.
Theorem	kmlem11 4921	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4.
Theorem	kmlem12 4922	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 3 => 4.
Theorem	kmlem13 4923	Lemma for 5-quantifier AC of Kurt Maes, Th. 4 1 <=> 4.
Theorem	kmlem14 4924	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4.
Theorem	kmlem15 4925	Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 5 <=> 4.
Theorem	kmlem16 4926	Lemma for 5-quantifier AC of Kurt Maes, Th. 4 5 <=> 4.
Theorem	aceqkm 4927	Equivalence of the Axiom of Choice (first form) of [Enderton] p. 49 and Maes' AC ackm 4928. The proof consists of lemmas kmlem1 4911 through kmlem16 4926 and this final theorem. AC is not used for the proof. Note: bypassing the first step (i.e. replacing aceq5 4886 with biid 168) establishes the AC equivalence shown by Mae's writeup. The left-hand-side AC shown here was chosen because it is shorter to display.
|- (A.xE.f(f (_ x /\ f Fn dom x) <-> A.xE.yA.zE.vA.u((y e. x /\ (z e. y -> ((v e. x /\ -. y = v) /\ z e. v))) \/ (-. y e. x /\ (z e. x -> ((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v))))))
Theorem	ackm 4928	A remarkable equivalent to the Axiom of Choice that has only 5 quantifiers (when expanded to e., = primitives in prenex form), discovered and proved by Kurt Maes. This establishes a new record, reducing from 6 to 5 the largest number of quantified variables needed by any ZFC axiom. The ZF-equivalence to AC is shown by theorem aceqkm 4927. Maes found this version of AC in April, 2004 (replacing a longer version, also with 5 quantifiers, that he found in November, 2003). See Kurt Maes, "A 5-quantifier (e.,=)-expression ZF-equivalent to the Axiom of Choice" (http://arxiv.org/PS_cache/arxiv/pdf/0705/0705.3162v1.pdf). The original FOM posts are: http://www.cs.nyu.edu/pipermail/fom/2003-November/007631.html http://www.cs.nyu.edu/pipermail/fom/2003-November/007641.html.
|- A.xE.yA.zE.vA.u((y e. x /\ (z e. y -> ((v e. x /\ -. y = v) /\ z e. v))) \/ (-. y e. x /\ (z e. x -> ((v e. z /\ v e. y) /\ ((u e. z /\ u e. y) -> u = v)))))
AC equivalents: well ordering, Zorn's lemma
Theorem	numthlem 4929	Lemma for numth 4930.
Theorem	numth 4930	Numeration theorem: every set can be put into one-to-one correspondence with some ordinal (using AC). Theorem 10.3 of [TakeutiZaring] p. 84.
|- A e. V   =>   |- E.x e. On E.f f:x-1-1-onto->A
Theorem	numth2 4931	Numeration theorem: any set is equinumerous to some ordinal (using AC). Theorem 10.3 of [TakeutiZaring] p. 84.
|- E.x e. On x ~~ A
Theorem	numthcor 4932	Any set is strictly dominated by some ordinal.
|- (A e. B -> E.x e. On A ~< x)
Theorem	weth 4933	Well-ordering theorem: any set A can be well-ordered. This is an equivalent of the Axiom of Choice. Theorem 6 of [Suppes] p. 242. First proved by Ernst Zermelo (the "Z" in ZFC) in 1904.
|- A e. V   =>   |- E.x x We A
Theorem	zorn2lem1 4934	Lemma for zorn2 4942.
Theorem	zorn2lem2 4935	Lemma for zorn2 4942.
Theorem	zorn2lem3 4936	Lemma for zorn2 4942.
Theorem	zorn2lem4 4937	Lemma for zorn2 4942.
Theorem	zorn2lem5 4938	Lemma for zorn2 4942.
Theorem	zorn2lem6 4939	Lemma for zorn2 4942.
Theorem	zorn2lem7 4940	Lemma for zorn2 4942.
Theorem	zornlem 4941	Lemma for zorn 4943.
Theorem	zorn2 4942	Zorn's Lemma of [Monk1] p. 117. This theorem is equivalent to the Axiom of Choice and states that every partially ordered set A (with an ordering relation R) in which every totally ordered subset has an upper bound, contains at least one maximal element. The main proof consists of lemmas zorn2lem1 4934 through zorn2lem7 4940; this final piece mainly changes bound variables to eliminate the hypotheses of zorn2lem7 4940.
|- A e. V   =>   |- ((R Po A /\ A.w((w (_ A /\ R Or w) -> E.x e. A A.z e. w (zRx \/ z = x))) -> E.x e. A A.y e. A -. xRy)
Theorem	zorn 4943	Zorn's Lemma. If the union of every chain (with respect to inclusion) in a set belongs to the set, then the set contains a maximal element. This theorem is equivalent to the Axiom of Choice. Theorem 6M of [Enderton] p. 151. See zorn2 4942 for a version with general partial orderings.
|- A e. V   =>   |- (A.z((z (_ A /\ A.x e. z A.y e. z (x (_ y \/ y (_ x)) -> U.z e. A) -> E.x e. A A.y e. A -. x (. y)
Theorem	fodom 4944	An onto function implies dominance of domain over range. Lemma 10.20 of [Kunen] p. 30. This theorem uses the Axiom of Choice ac7g 4895. AC is not needed for finite sets - see fodomfi 4709.
|- A e. V   =>   |- (F:A-onto->B -> B ~<_ A)
Theorem	fodomg 4945	An onto function implies dominance of domain over range.
|- (A e. C -> (F:A-onto->B -> B ~<_ A))
Theorem	fodomb 4946	Equivalence of an onto mapping and dominance for a non-empty set. Proposition 10.35 of [TakeutiZaring] p. 93.
|- A e. V   =>   |- ((A =/= (/) /\ E.f f:A-onto->B) <-> ((/) ~< B /\ B ~<_ A))
Theorem	brdom3 4947	Equivalence to a dominance relation.
|- A e. V   &   |- B e. V   =>   |- (A ~<_ B <-> E.f(A.xE*y xfy /\ A.x e. A E.y e. B yfx))
Theorem	brdom5 4948	An equivalence to a dominance relation.
|- A e. V   &   |- B e. V   =>   |- (A ~<_ B <-> E.f(A.x e. B E*y xfy /\ A.x e. A E.y e. B yfx))
Theorem	brdom4 4949	An equivalence to a dominance relation.
|- A e. V   &   |- B e. V   =>   |- (A ~<_ B <-> E.f(A.x e. B E*y(y e. A /\ xfy) /\ A.x e. A E.y e. B yfx))
Theorem	brdom7disj 4950	An equivalence to a dominance relation for disjoint sets.
|- A e. V   &   |- B e. V   &   |- (A i^i B) = (/)   =>   |- (A ~<_ B <-> E.f(A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f))
Theorem	brdom6disj 4951	An equivalence to a dominance relation for disjoint sets.
|- A e. V   &   |- B e. V   &   |- (A i^i B) = (/)   =>   |- (A ~<_ B <-> E.f(A.x e. B E*y{x, y} e. f /\ A.x e. A E.y e. B {y, x} e. f))
Theorem	imadomg 4952	An image of a function under a set is dominated by the set. Proposition 10.34 of [TakeutiZaring] p. 92.
|- (A e. B -> (Fun F -> (F"A) ~<_ A))
Theorem	fnrndomg 4953	The range of a function is dominated by its domain.
|- (A e. B -> (F Fn A -> ran F ~<_ A))
Theorem	unidom 4954	An upper bound for the cardinality of a union. Theorem 10.47 of [TakeutiZaring] p. 98.
|- A e. V   &   |- B e. V   =>   |- (A.x e. A x ~<_ B -> U.A ~<_ (A X. B))
Theorem	unidomg 4955	An upper bound for the cardinality of a union. Theorem 10.47 of [TakeutiZaring] p. 98.
|- ((A e. C /\ B e. D /\ A.x e. A x ~<_ B) -> U.A ~<_ (A X. B))
Theorem	uniimadom 4956	An upper bound for the cardinality of the union of an image. Theorem 10.48 of [TakeutiZaring] p. 99.
|- A e. V   &   |- B e. V   =>   |- ((Fun F /\ A.x e. A (F` x) ~<_ B) -> U.(F"A) ~<_ (A X. B))
Theorem	uniimadomf 4957	An upper bound for the cardinality of the union of an image. Theorem 10.48 of [TakeutiZaring] p. 99. This version of uniimadom 4956 uses a bound-variable hypothesis in place of a distinct variable condition.
|- (y e. F -> A.x y e. F)   &   |- A e. V   &   |- B e. V   =>   |- ((Fun F /\ A.x e. A (F` x) ~<_ B) -> U.(F"A) ~<_ (A X. B))
Theorem	iundom 4958	An upper bound for the cardinality of an indexed union. C depends on x and should be thought of as C(x).
|- A e. V   &   |- B e. V   &   |- C e. V   =>   |- (A.x e. A C ~<_ B -> U_x e. A C ~<_ (A X. B))
Cardinal numbers
Syntax	ccrd 4959	Extend class definition to include the cardinal size function.
class card
Syntax	cale 4960	Extend class definition to include the aleph function.
class aleph
Syntax	ccf 4961	Extend class definition to include the cofinality function.
class cf
Definition	df-card 4962	Define the cardinal number function. The cardinal number of a set is the least ordinal number equinumerous to it. In other words, it is the "size" of the set. Definition of [Enderton] p. 197. See cardval 4973 for its value, cardval2 5005 for a simpler version of its value. The principle theorem relating cardinality to equinumerosity is carden 4979. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function.
|- card = {<.x, y>. | y = |^|{z e. On | z ~~ x}}
Definition	df-aleph 4963	Define the aleph function. Our definition expresses Definition 12 of [Suppes] p. 229 in a closed form, from which we derive the recursive definition as theorems aleph0 5013, alephsuc 5016, and alephlim 5014. The aleph function provides a one-to-one, onto mapping from the ordinal numbers to the infinite cardinal numbers. Roughly, any aleph is the smallest infinite cardinal number whose size is strictly greater than any aleph before it.
|- aleph = rec({<.x, y>. | y = |^|{z e. On | x ~< z}}, om)
Definition	df-cf 4964	Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 5056 for its value and a description.
|- cf = {<.x, y>. | (x e. On /\ y = |^|{z | E.w(z = (card` w) /\ (w (_ x /\ A.v e. x E.u e. w v (_ u))})}
Theorem	oncardval 4965	The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 4973, this theorem does not require the Axiom of Choice.
|- (A e. On -> (card` A) = |^|{x e. On | x ~~ A})
Theorem	oncardon 4966	The cardinal number of an ordinal number is an ordinal number. Unlike cardon 4974, this theorem does not require the Axiom of Choice.
|- (A e. On -> (card` A) e. On)
Theorem	oncardid 4967	Any ordinal number is equinumerous to its cardinal number. Unlike cardid 4975, this theorem does not require the Axiom of Choice.
|- (A e. On -> (card` A) ~~ A)
Theorem	cardonle 4968	The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85.
|- (A e. On -> (card` A) (_ A)
Theorem	card0 4969	The cardinality of the empty set is the empty set.
|- (card` (/)) = (/)
Theorem	cardnn 4970	The cardinality of a natural number is the number. Corollary 10.23 of [TakeutiZaring] p. 90.
|- (A e. om -> (card` A) = A)
Theorem	cardsucnn 4971	The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 4991.
|- (A e. om -> (card` suc A) = suc (card` A))
Theorem	cardom 4972	The set of natural numbers is a cardinal number. Theorem 18.11 of [Monk1] p. 133.
|- (card` om) = om
Theorem	cardval 4973	The value of the cardinal number function. Definition 10.4 of [TakeutiZaring] p. 85. See cardval2 5005 for a simpler version of its value.
|- (card` A) = |^|{x e. On | x ~~ A}
Theorem	cardon 4974	The cardinal number of a set is an ordinal number. Proposition 10.6(1) of [TakeutiZaring] p. 85. Unlike Takeuti/Zaring's proposition, we need the Axiom of Choice (in cardval 4973) because of our slightly different definition of of cardinal number.
|- (card` A) e. On
Theorem	cardid 4975	Any set is equinumerous to its cardinal number. Proposition 10.5 of [TakeutiZaring] p. 85.
|- (card` A) ~~ A
Theorem	oncard 4976	A set is a cardinal number iff it equals its own cardinal number. Proposition 10.9 of [TakeutiZaring] p. 85.
|- (E.x A = (card` x) <-> A = (card` A))
Theorem	ficardom 4977	The cardinal number of a finite set is a finite ordinal. (Contributed by Paul Chapman, 11-Apr-2009.)
|- (A e. Fin -> (card` A) e. om)
Theorem	cardne 4978	No member of a cardinal number of a set is equinumerous to the set. Proposition 10.6(2) of [TakeutiZaring] p. 85.
|- (A e. (card` B) -> -. A ~~ B)
Theorem	carden 4979	Two sets are equinumerous iff their cardinal numbers are equal. This important theorem expresses the essential concept behind "cardinality" or "size." This theorem appears as Proposition 10.10 of [TakeutiZaring] p. 85, Theorem 7P of [Enderton] p. 197, and Theorem 9 of [Suppes] p. 242 (among others). The Axiom of Choice is required for its proof. The theory of cardinality can also be developed without AC by introducing "card" as a primitive notion and stating this theorem as an axiom, as is done with the axiom for cardinal numbers in [Suppes] p. 111. Finally, if we allow the Axiom of Regularity, we can avoid AC by defining the cardinal number of a set as the set of all sets equinumerous to it and having least possible rank (see karden 4872).
|- ((A e. C /\ B e. D) -> ((card` A) = (card` B) <-> A ~~ B))
Theorem	cardeq0 4980	Only the empty set has cardinality zero.
|- (A e. B -> ((card` A) = (/) <-> A = (/)))
Theorem	card1 4981	A set has cardinality one iff it is a singleton.
|- ((card` A) = 1o <-> E.x A = {x})
Theorem	cardsn 4982	A singleton has cardinality one.
|- (A e. B -> (card` {A}) = 1o)
Theorem	unsnen 4983	Equinumerosity of a set with a new element added.
|- A e. V   &   |- B e. V   =>   |- (-. B e. A -> (A u. {B}) ~~ suc (card` A))
Theorem	carddomi 4984	Two sets have the dominance relationship if their cardinalities have the subset relationship.
|- (A e. C -> ((card` A) (_ (card` B) -> A ~<_ B))
Theorem	carddom 4985	Two sets have the dominance relationship iff their cardinalities have the subset relationship. Equation i of [Quine] p. 232.
|- ((A e. C /\ B e. D) -> ((card` A) (_ (card` B) <-> A ~<_ B))
Theorem	cardsdom 4986	Two sets have the strict dominance relationship iff their cardinalities have the membership relationship. Corollary 19.7(2) of [Eisenberg] p. 310.
|- ((A e. C /\ B e. D) -> ((card` A) e. (card` B) <-> A ~< B))
Theorem	domtri 4987	Trichotomy law for dominance and strict dominance. This theorem is equivalent to the Axiom of Choice.
|- ((A e. C /\ B e. D) -> (A ~<_ B <-> -. B ~< A))
Theorem	entric 4988	Trichotomy of equinumerosity and strict dominance. This theorem is equivalent to the Axiom of Choice. Theorem 8 of [Suppes] p. 242.
|- ((A e. C /\ B e. D) -> (A ~< B \/ A ~~ B \/ B ~< A))
Theorem	entri2 4989	Trichotomy of dominance and strict dominance.
|- ((A e. C /\ B e. D) -> (A ~<_ B \/ B ~< A))
Theorem	entri3 4990	Trichotomy of dominance. This theorem is equivalent to the Axiom of Choice. Part of Proposition 4.42(d) of [Mendelson] p. 275.
|- ((A e. C /\ B e. D) -> (A ~<_ B \/ B ~<_ A))
Theorem	cardsucinf 4991	The cardinality of the successor of an infinite ordinal.
|- ((A e. On /\ om (_ A) -> (card` suc A) = (card` A))
Theorem	sucdom 4992	Strict dominance of a set over a natural number is the same as dominance over its successor. The proof uses AC and Infinity. It is unclear if a proof without using these is possible, unlike the weaker versions omsucdom 4669, sucdomi 4670, and finsucdom 4673.
|- ((A e. om /\ B e. C) -> (A ~< B <-> suc A ~<_ B))
Theorem	unxpdomlem 4993	Lemma for unxpdom 4994.
Theorem	unxpdom 4994	Cross product dominates union for sets with cardinality greater than 1. Proposition 10.36 of [TakeutiZaring] p. 93.
|- ((1o ~< A /\ 1o ~< B) -> (A u. B) ~<_ (A X. B))
Theorem	unxpdom2 4995	Corollary of unxpdom 4994.
|- A e. V   &   |- B e. V   =>   |- ((1o ~< A /\ B ~<_ A) -> (A u. B) ~<_ (A X. A))
Theorem	sucxpdom 4996	Cross product dominates successor for set with cardinality greater than 1. Proposition 10.38 of [TakeutiZaring] p. 93 (but generalized to arbitrary sets, not just ordinals, with a proof using AC).
|- (1o ~< A -> suc A ~<_ (A X. A))
Theorem	sdomel 4997	Strict dominance implies ordinal membership.
|- ((A e. On /\ B e. On) -> (A ~< B -> A e. B))
Theorem	sdomsdomcard 4998	A set strictly dominates iff its cardinal strictly dominates.
|- (A ~< B <-> A ~< (card` B))
Theorem	cardidm 4999	The cardinality function is idempotent. Proposition 10.11 of [TakeutiZaring] p. 85.
|- (card` (card` A)) = (card` A)
Theorem	canth3 5000	Cantor's theorem in terms of cardinals. This theorem tells us that no matter how largei a cardinal number is, there is a still larger cardinal number. Theorem 18.12 of [Monk1] p. 133.
|- (A e. B -> (card` A) e. (card` P~A))