P. 101 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 10001-10100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	djuss 10001	A disjoint union is a subclass of a Cartesian product. (Contributed by AV, 25-Jun-2022.)
⊢ (𝐴 ⊔ 𝐵) ⊆ ({∅, 1o} × (𝐴 ∪ 𝐵))
Theorem	djuunxp 10002	The union of a disjoint union and its inversion is the Cartesian product of an unordered pair and the union of the left and right classes of the disjoint unions. (Proposed by GL, 4-Jul-2022.) (Contributed by AV, 4-Jul-2022.)
⊢ ((𝐴 ⊔ 𝐵) ∪ (𝐵 ⊔ 𝐴)) = ({∅, 1o} × (𝐴 ∪ 𝐵))
Theorem	djuexALT 10003	Alternate proof of djuex 9989, which is shorter, but based indirectly on the definitions of inl and inr. (Proposed by BJ, 28-Jun-2022.) (Contributed by AV, 28-Jun-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ∈ V)
Theorem	eldju1st 10004	The first component of an element of a disjoint union is either ∅ or 1o. (Contributed by AV, 26-Jun-2022.)
⊢ (𝑋 ∈ (𝐴 ⊔ 𝐵) → ((1st ‘𝑋) = ∅ ∨ (1st ‘𝑋) = 1o))
Theorem	eldju2ndl 10005	The second component of an element of a disjoint union is an element of the left class of the disjoint union if its first component is the empty set. (Contributed by AV, 26-Jun-2022.)
⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1st ‘𝑋) = ∅) → (2nd ‘𝑋) ∈ 𝐴)
Theorem	eldju2ndr 10006	The second component of an element of a disjoint union is an element of the right class of the disjoint union if its first component is not the empty set. (Contributed by AV, 26-Jun-2022.)
⊢ ((𝑋 ∈ (𝐴 ⊔ 𝐵) ∧ (1st ‘𝑋) ≠ ∅) → (2nd ‘𝑋) ∈ 𝐵)
Theorem	djuun 10007	The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.)
⊢ ((inl “ 𝐴) ∪ (inr “ 𝐵)) = (𝐴 ⊔ 𝐵)
Theorem	1stinl 10008	The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.)
⊢ (𝑋 ∈ 𝑉 → (1st ‘(inl‘𝑋)) = ∅)
Theorem	2ndinl 10009	The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.)
⊢ (𝑋 ∈ 𝑉 → (2nd ‘(inl‘𝑋)) = 𝑋)
Theorem	1stinr 10010	The first component of the value of a right injection is 1o. (Contributed by AV, 27-Jun-2022.)
⊢ (𝑋 ∈ 𝑉 → (1st ‘(inr‘𝑋)) = 1o)
Theorem	2ndinr 10011	The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.)
⊢ (𝑋 ∈ 𝑉 → (2nd ‘(inr‘𝑋)) = 𝑋)
Theorem	updjudhf 10012*	The mapping of an element of the disjoint union to the value of the corresponding function is a function. (Contributed by AV, 26-Jun-2022.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))))    ⇒   ⊢ (𝜑 → 𝐻:(𝐴 ⊔ 𝐵)⟶𝐶)
Theorem	updjudhcoinlf 10013*	The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))))    ⇒   ⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹)
Theorem	updjudhcoinrg 10014*	The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the right injection equals the second function. (Contributed by AV, 27-Jun-2022.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)    &   ⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))))    ⇒   ⊢ (𝜑 → (𝐻 ∘ (inr ↾ 𝐵)) = 𝐺)
Theorem	updjud 10015*	Universal property of the disjoint union. This theorem shows that the disjoint union, together with the left and right injections df-inl 9983 and df-inr 9984, is the coproduct in the category of sets, see Wikipedia "Coproduct", https://en.wikipedia.org/wiki/Coproduct 9984 (25-Aug-2023). This is a special case of Example 1 of coproducts in Section 10.67 of [Adamek] p. 185. (Proposed by BJ, 25-Jun-2022.) (Contributed by AV, 28-Jun-2022.)
⊢ (𝜑 → 𝐹:𝐴⟶𝐶)    &   ⊢ (𝜑 → 𝐺:𝐵⟶𝐶)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    ⇒   ⊢ (𝜑 → ∃!ℎ(ℎ:(𝐴 ⊔ 𝐵)⟶𝐶 ∧ (ℎ ∘ (inl ↾ 𝐴)) = 𝐹 ∧ (ℎ ∘ (inr ↾ 𝐵)) = 𝐺))
2.6.14  Cardinal numbers
Syntax	ccrd 10016	Extend class definition to include the cardinal size function.
class card
Syntax	cale 10017	Extend class definition to include the aleph function.
class ℵ
Syntax	ccf 10018	Extend class definition to include the cofinality function.
class cf
Syntax	wacn 10019	The axiom of choice for limited-length sequences.
class AC 𝐴
Definition	df-card 10020*	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 10630 for its value and cardval2 10072 for a simpler version of its value. The principal theorem relating cardinality to equinumerosity is carden 10635. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function. (Contributed by NM, 21-Oct-2003.)
⊢ card = (𝑥 ∈ V ↦ ∩ {𝑦 ∈ On ∣ 𝑦 ≈ 𝑥})
Definition	df-aleph 10021	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 10145, alephsuc 10147, and alephlim 10146. 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. (Contributed by NM, 21-Oct-2003.)
⊢ ℵ = rec(har, ω)
Definition	df-cf 10022*	Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 10324 for its value and a description. (Contributed by NM, 1-Apr-2004.)
⊢ cf = (𝑥 ∈ On ↦ ∩ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢))})
Definition	df-acn 10023*	Define a local and length-limited version of the axiom of choice. The definition of the predicate 𝑋 ∈ AC 𝐴 is that for all families of nonempty subsets of 𝑋 indexed on 𝐴 (i.e. functions 𝐴⟶𝒫 𝑋 ∖ {∅}), there is a function which selects an element from each set in the family. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ AC 𝐴 = {𝑥 ∣ (𝐴 ∈ V ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))}
Theorem	cardf2 10024*	The cardinality function is a function with domain the well-orderable sets. Assuming AC, this is the universe. (Contributed by Mario Carneiro, 6-Jun-2013.) (Revised by Mario Carneiro, 20-Sep-2014.)
⊢ card:{𝑥 ∣ ∃𝑦 ∈ On 𝑦 ≈ 𝑥}⟶On
Theorem	cardon 10025	The cardinal number of a set is an ordinal number. Proposition 10.6(1) of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ (card‘𝐴) ∈ On
Theorem	isnum2 10026*	A way to express well-orderability without bound or distinct variables. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ (𝐴 ∈ dom card ↔ ∃𝑥 ∈ On 𝑥 ≈ 𝐴)
Theorem	isnumi 10027	A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ dom card)
Theorem	ennum 10028	Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ dom card ↔ 𝐵 ∈ dom card))
Theorem	finnum 10029	Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)
Theorem	onenon 10030	Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ On → 𝐴 ∈ dom card)
Theorem	tskwe 10031*	A Tarski set is well-orderable. (Contributed by Mario Carneiro, 19-Apr-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → 𝐴 ∈ dom card)
Theorem	xpnum 10032	The cartesian product of numerable sets is numerable. (Contributed by Mario Carneiro, 3-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 × 𝐵) ∈ dom card)
Theorem	cardval3 10033*	An alternate definition of the value of (card‘𝐴) that does not require AC to prove. (Contributed by Mario Carneiro, 7-Jan-2013.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ (𝐴 ∈ dom card → (card‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝑥 ≈ 𝐴})
Theorem	cardid2 10034	Any numerable set is equinumerous to its cardinal number. Proposition 10.5 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.)
⊢ (𝐴 ∈ dom card → (card‘𝐴) ≈ 𝐴)
Theorem	isnum3 10035	A set is numerable iff it is equinumerous with its cardinal. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ dom card ↔ (card‘𝐴) ≈ 𝐴)
Theorem	oncardval 10036*	The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 10630, this theorem does not require the Axiom of Choice. (Contributed by NM, 24-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ (𝐴 ∈ On → (card‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝑥 ≈ 𝐴})
Theorem	oncardid 10037	Any ordinal number is equinumerous to its cardinal number. Unlike cardid 10631, this theorem does not require the Axiom of Choice. (Contributed by NM, 26-Jul-2004.)
⊢ (𝐴 ∈ On → (card‘𝐴) ≈ 𝐴)
Theorem	cardonle 10038	The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85. (Contributed by NM, 22-Oct-2003.)
⊢ (𝐴 ∈ On → (card‘𝐴) ⊆ 𝐴)
Theorem	card0 10039	The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)
⊢ (card‘∅) = ∅
Theorem	cardidm 10040	The cardinality function is idempotent. Proposition 10.11 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.)
⊢ (card‘(card‘𝐴)) = (card‘𝐴)
Theorem	oncard 10041*	A set is a cardinal number iff it equals its own cardinal number. Proposition 10.9 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.)
⊢ (∃𝑥 𝐴 = (card‘𝑥) ↔ 𝐴 = (card‘𝐴))
Theorem	ficardom 10042	The cardinal number of a finite set is a finite ordinal. (Contributed by Paul Chapman, 11-Apr-2009.) (Revised by Mario Carneiro, 4-Feb-2013.)
⊢ (𝐴 ∈ Fin → (card‘𝐴) ∈ ω)
Theorem	ficardid 10043	A finite set is equinumerous to its cardinal number. (Contributed by Mario Carneiro, 21-Sep-2013.)
⊢ (𝐴 ∈ Fin → (card‘𝐴) ≈ 𝐴)
Theorem	cardnn 10044	The cardinality of a natural number is the number. Corollary 10.23 of [TakeutiZaring] p. 90. (Contributed by Mario Carneiro, 7-Jan-2013.)
⊢ (𝐴 ∈ ω → (card‘𝐴) = 𝐴)
Theorem	cardnueq0 10045	The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013.)
⊢ (𝐴 ∈ dom card → ((card‘𝐴) = ∅ ↔ 𝐴 = ∅))
Theorem	cardne 10046	No member of a cardinal number of a set is equinumerous to the set. Proposition 10.6(2) of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 9-Jan-2013.)
⊢ (𝐴 ∈ (card‘𝐵) → ¬ 𝐴 ≈ 𝐵)
Theorem	carden2a 10047	If two sets have equal nonzero cardinalities, then they are equinumerous. This assertion and carden2b 10048 are meant to replace carden 10635 in ZF without AC. (Contributed by Mario Carneiro, 9-Jan-2013.)
⊢ (((card‘𝐴) = (card‘𝐵) ∧ (card‘𝐴) ≠ ∅) → 𝐴 ≈ 𝐵)
Theorem	carden2b 10048	If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a 10047 are meant to replace carden 10635 in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) = (card‘𝐵))
Theorem	card1 10049*	A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013.)
⊢ ((card‘𝐴) = 1o ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	cardsn 10050	A singleton has cardinality one. (Contributed by Mario Carneiro, 10-Jan-2013.)
⊢ (𝐴 ∈ 𝑉 → (card‘{𝐴}) = 1o)
Theorem	carddomi2 10051	Two sets have the dominance relationship if their cardinalities have the subset relationship and one is numerable. See also carddom 10638, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ 𝑉) → ((card‘𝐴) ⊆ (card‘𝐵) → 𝐴 ≼ 𝐵))
Theorem	sdomsdomcardi 10052	A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ (𝐴 ≺ (card‘𝐵) → 𝐴 ≺ 𝐵)
Theorem	cardlim 10053	An infinite cardinal is a limit ordinal. Equivalent to Exercise 4 of [TakeutiZaring] p. 91. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ (ω ⊆ (card‘𝐴) ↔ Lim (card‘𝐴))
Theorem	cardsdomelir 10054	A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. This is half of the assertion cardsdomel 10055 and can be proven without the AC. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ (𝐴 ∈ (card‘𝐵) → 𝐴 ≺ 𝐵)
Theorem	cardsdomel 10055	A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. (Contributed by Mario Carneiro, 15-Jan-2013.) (Revised by Mario Carneiro, 4-Jun-2015.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ dom card) → (𝐴 ≺ 𝐵 ↔ 𝐴 ∈ (card‘𝐵)))
Theorem	iscard 10056*	Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴))
Theorem	iscard2 10057*	Two ways to express the property of being a cardinal number. Definition 8 of [Suppes] p. 225. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ On (𝐴 ≈ 𝑥 → 𝐴 ⊆ 𝑥)))
Theorem	carddom2 10058	Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 10638, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ⊆ (card‘𝐵) ↔ 𝐴 ≼ 𝐵))
Theorem	harcard 10059	The class of ordinal numbers dominated by a set is a cardinal number. Theorem 59 of [Suppes] p. 228. (Contributed by Mario Carneiro, 20-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (card‘(har‘𝐴)) = (har‘𝐴)
Theorem	cardprclem 10060*	Lemma for cardprc 10061. (Contributed by Mario Carneiro, 22-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ 𝐴 = {𝑥 ∣ (card‘𝑥) = 𝑥}    ⇒   ⊢ ¬ 𝐴 ∈ V
Theorem	cardprc 10061	The class of all cardinal numbers is not a set (i.e. is a proper class). Theorem 19.8 of [Eisenberg] p. 310. In this proof (which does not use AC), we cannot use Cantor's construction canth3 10645 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs 9538 to construct (effectively) (ℵ‘suc 𝐴) from (ℵ‘𝐴), which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013.)
⊢ {𝑥 ∣ (card‘𝑥) = 𝑥} ∉ V
Theorem	carduni 10062*	The union of a set of cardinals is a cardinal. Theorem 18.14 of [Monk1] p. 133. (Contributed by Mario Carneiro, 20-Jan-2013.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝑥) = 𝑥 → (card‘∪ 𝐴) = ∪ 𝐴))
Theorem	cardiun 10063*	The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵 → (card‘∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 𝐵))
Theorem	cardennn 10064	If 𝐴 is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ ω) → (card‘𝐴) = 𝐵)
Theorem	cardsucinf 10065	The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013.)
⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (card‘suc 𝐴) = (card‘𝐴))
Theorem	cardsucnn 10066	The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 10065. (Contributed by NM, 7-Nov-2008.)
⊢ (𝐴 ∈ ω → (card‘suc 𝐴) = suc (card‘𝐴))
Theorem	cardom 10067	The set of natural numbers is a cardinal number. Theorem 18.11 of [Monk1] p. 133. (Contributed by NM, 28-Oct-2003.)
⊢ (card‘ω) = ω
Theorem	carden2 10068	Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden 10635, the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) = (card‘𝐵) ↔ 𝐴 ≈ 𝐵))
Theorem	cardsdom2 10069	A numerable set is strictly dominated by another iff their cardinalities are strictly ordered. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) ∈ (card‘𝐵) ↔ 𝐴 ≺ 𝐵))
Theorem	domtri2 10070	Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴))
Theorem	nnsdomel 10071	Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ 𝐴 ≺ 𝐵))
Theorem	cardval2 10072*	An alternate version of the value of the cardinal number of a set. Compare cardval 10630. This theorem could be used to give a simpler definition of card in place of df-card 10020. It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003.)
⊢ (𝐴 ∈ dom card → (card‘𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})
Theorem	isinffi 10073*	An infinite set contains subsets equinumerous to every finite set. Extension of isinf 9256 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐵–1-1→𝐴)
Theorem	fidomtri 10074	Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 27-Apr-2015.)
⊢ ((𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴))
Theorem	fidomtri2 10075	Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014.) (Revised by Mario Carneiro, 7-May-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴))
Theorem	harsdom 10076	The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ dom card → 𝐴 ≺ (har‘𝐴))
Theorem	onsdom 10077*	Any well-orderable set is strictly dominated by an ordinal number. (Contributed by Jeff Hankins, 22-Oct-2009.) (Proof shortened by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ dom card → ∃𝑥 ∈ On 𝐴 ≺ 𝑥)
Theorem	harval2 10078*	An alternate expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥})
Theorem	harsucnn 10079	The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.)
⊢ (𝐴 ∈ ω → (har‘𝐴) = suc 𝐴)
Theorem	cardmin2 10080*	The smallest ordinal that strictly dominates a set is a cardinal, if it exists. (Contributed by Mario Carneiro, 2-Feb-2013.)
⊢ (∃𝑥 ∈ On 𝐴 ≺ 𝑥 ↔ (card‘∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥}) = ∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥})
Theorem	pm54.43lem 10081*	In Theorem *54.43 of [WhiteheadRussell] p. 360, the number 1 is defined as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 10049), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o}. Here we show that this is equivalent to 𝐴 ≈ 1o so that we can use the latter more convenient notation in pm54.43 10082. (Contributed by NM, 4-Nov-2013.)
⊢ (𝐴 ≈ 1o ↔ 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o})
Theorem	pm54.43 10082	Theorem *54.43 of [WhiteheadRussell] p. 360. "From this proposition it will follow, when arithmetical addition has been defined, that 1+1=2." See http://en.wikipedia.org/wiki/Principia_Mathematica#Quotations. This theorem states that two sets of cardinality 1 are disjoint iff their union has cardinality 2. Whitehead and Russell define 1 as the collection of all sets with cardinality 1 (i.e. all singletons; see card1 10049), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o} which is the same as 𝐴 ≈ 1o by pm54.43lem 10081. We do not have several of their earlier lemmas available (which would otherwise be unused by our different approach to arithmetic), so our proof is longer. (It is also longer because we must show every detail.) Theorem dju1p1e2 10252 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.)
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o))
Theorem	enpr2 10083	An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d 9076. (Contributed by FL, 17-Aug-2008.) Avoid ax-pow 5326, ax-un 7751. (Revised by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o)
Theorem	pr2ne 10084	If an unordered pair has two elements, then they are different. (Contributed by FL, 14-Feb-2010.) Avoid ax-pow 5326, ax-un 7751. (Revised by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵))
Theorem	prdom2 10085	An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐵} ≼ 2o)
Theorem	en2eqpr 10086	Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ≠ 𝐵 → 𝐶 = {𝐴, 𝐵}))
Theorem	en2eleq 10087	Express a set of pair cardinality as the unordered pair of a given element and the other element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → 𝑃 = {𝑋, ∪ (𝑃 ∖ {𝑋})})
Theorem	en2other2 10088	Taking the other element twice in a pair gets back to the original element. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ ((𝑋 ∈ 𝑃 ∧ 𝑃 ≈ 2o) → ∪ (𝑃 ∖ {∪ (𝑃 ∖ {𝑋})}) = 𝑋)
Theorem	dif1card 10089	The cardinality of a nonempty finite set is one greater than the cardinality of the set with one element removed. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 2-Feb-2013.)
⊢ ((𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐴) → (card‘𝐴) = suc (card‘(𝐴 ∖ {𝑋})))
Theorem	leweon 10090*	Lexicographical order is a well-ordering of On × On. Proposition 7.56(1) of [TakeutiZaring] p. 54. Note that unlike r0weon 10091, this order is not set-like, as the preimage of ⟨1o, ∅⟩ is the proper class ({∅} × On). (Contributed by Mario Carneiro, 9-Mar-2013.)
⊢ 𝐿 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))}    ⇒   ⊢ 𝐿 We (On × On)
Theorem	r0weon 10091*	A set-like well-ordering of the class of ordinal pairs. Proposition 7.58(1) of [TakeutiZaring] p. 54. (Contributed by Mario Carneiro, 7-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐿 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))}    &   ⊢ 𝑅 = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))}    ⇒   ⊢ (𝑅 We (On × On) ∧ 𝑅 Se (On × On))
Theorem	infxpenlem 10092*	Lemma for infxpen 10093. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ 𝐿 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On)) ∧ ((1st ‘𝑥) ∈ (1st ‘𝑦) ∨ ((1st ‘𝑥) = (1st ‘𝑦) ∧ (2nd ‘𝑥) ∈ (2nd ‘𝑦))))}    &   ⊢ 𝑅 = {⟨𝑧, 𝑤⟩ ∣ ((𝑧 ∈ (On × On) ∧ 𝑤 ∈ (On × On)) ∧ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) ∈ ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∨ (((1st ‘𝑧) ∪ (2nd ‘𝑧)) = ((1st ‘𝑤) ∪ (2nd ‘𝑤)) ∧ 𝑧𝐿𝑤)))}    &   ⊢ 𝑄 = (𝑅 ∩ ((𝑎 × 𝑎) × (𝑎 × 𝑎)))    &   ⊢ (𝜑 ↔ ((𝑎 ∈ On ∧ ∀𝑚 ∈ 𝑎 (ω ⊆ 𝑚 → (𝑚 × 𝑚) ≈ 𝑚)) ∧ (ω ⊆ 𝑎 ∧ ∀𝑚 ∈ 𝑎 𝑚 ≺ 𝑎)))    &   ⊢ 𝑀 = ((1st ‘𝑤) ∪ (2nd ‘𝑤))    &   ⊢ 𝐽 = OrdIso(𝑄, (𝑎 × 𝑎))    ⇒   ⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
Theorem	infxpen 10093	Every infinite ordinal is equinumerous to its Cartesian square. Proposition 10.39 of [TakeutiZaring] p. 94, whose proof we follow closely. The key idea is to show that the relation 𝑅 is a well-ordering of (On × On) with the additional property that 𝑅-initial segments of (𝑥 × 𝑥) (where 𝑥 is a limit ordinal) are of cardinality at most 𝑥. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 26-Jun-2015.)
⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
Theorem	xpomen 10094	The Cartesian product of omega (the set of ordinal natural numbers) with itself is equinumerous to omega. Exercise 1 of [Enderton] p. 133. (Contributed by NM, 23-Jul-2004.) (Revised by Mario Carneiro, 9-Mar-2013.)
⊢ (ω × ω) ≈ ω
Theorem	xpct 10095	The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω)
Theorem	infxpidm2 10096	Every infinite well-orderable set is equinumerous to its Cartesian square. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of [TakeutiZaring] p. 95. See also infxpidm 10646. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
Theorem	infxpenc 10097*	A canonical version of infxpen 10093, by a completely different approach (although it uses infxpen 10093 via xpomen 10094). Using Cantor's normal form, we can show that 𝐴 ↑o 𝐵 respects equinumerosity (oef1o 9699), so that all the steps of (ω↑𝑊) · (ω↑𝑊) ≈ ω↑(2𝑊) ≈ (ω↑2)↑𝑊 ≈ ω↑𝑊 can be verified using bijections to do the ordinal commutations. (The assumption on 𝑁 can be satisfied using cnfcom3c 9707.) (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ω ⊆ 𝐴)    &   ⊢ (𝜑 → 𝑊 ∈ (On ∖ 1o))    &   ⊢ (𝜑 → 𝐹:(ω ↑o 2o)–1-1-onto→ω)    &   ⊢ (𝜑 → (𝐹‘∅) = ∅)    &   ⊢ (𝜑 → 𝑁:𝐴–1-1-onto→(ω ↑o 𝑊))    &   ⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑o 2o) ↑m 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊))))    &   ⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑o 2o) CNF 𝑊))    &   ⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑m (𝑊 ·o 2o)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦 ∘ ◡(𝑌 ∘ ◡𝑋))))    &   ⊢ 𝑋 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·o 𝑧) +o 𝑤))    &   ⊢ 𝑌 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((2o ·o 𝑤) +o 𝑧))    &   ⊢ 𝐽 = (((ω CNF (2o ·o 𝑊)) ∘ 𝐿) ∘ ◡(ω CNF (𝑊 ·o 2o)))    &   ⊢ 𝑍 = (𝑥 ∈ (ω ↑o 𝑊), 𝑦 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑥) +o 𝑦))    &   ⊢ 𝑇 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ ⟨(𝑁‘𝑥), (𝑁‘𝑦)⟩)    &   ⊢ 𝐺 = (◡𝑁 ∘ (((𝐻 ∘ 𝐽) ∘ 𝑍) ∘ 𝑇))    ⇒   ⊢ (𝜑 → 𝐺:(𝐴 × 𝐴)–1-1-onto→𝐴)
Theorem	infxpenc2lem1 10098*	Lemma for infxpenc2 10101. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))    &   ⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1o) ↦ (ω ↑o 𝑥))‘ran (𝑛‘𝑏))    ⇒   ⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝑊 ∈ (On ∖ 1o) ∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑊)))
Theorem	infxpenc2lem2 10099*	Lemma for infxpenc2 10101. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))    &   ⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1o) ↦ (ω ↑o 𝑥))‘ran (𝑛‘𝑏))    &   ⊢ (𝜑 → 𝐹:(ω ↑o 2o)–1-1-onto→ω)    &   ⊢ (𝜑 → (𝐹‘∅) = ∅)    &   ⊢ 𝐾 = (𝑦 ∈ {𝑥 ∈ ((ω ↑o 2o) ↑m 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊))))    &   ⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑o 2o) CNF 𝑊))    &   ⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑m (𝑊 ·o 2o)) ∣ 𝑥 finSupp ∅} ↦ (( I ↾ ω) ∘ (𝑦 ∘ ◡(𝑌 ∘ ◡𝑋))))    &   ⊢ 𝑋 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((𝑊 ·o 𝑧) +o 𝑤))    &   ⊢ 𝑌 = (𝑧 ∈ 2o, 𝑤 ∈ 𝑊 ↦ ((2o ·o 𝑤) +o 𝑧))    &   ⊢ 𝐽 = (((ω CNF (2o ·o 𝑊)) ∘ 𝐿) ∘ ◡(ω CNF (𝑊 ·o 2o)))    &   ⊢ 𝑍 = (𝑥 ∈ (ω ↑o 𝑊), 𝑦 ∈ (ω ↑o 𝑊) ↦ (((ω ↑o 𝑊) ·o 𝑥) +o 𝑦))    &   ⊢ 𝑇 = (𝑥 ∈ 𝑏, 𝑦 ∈ 𝑏 ↦ ⟨((𝑛‘𝑏)‘𝑥), ((𝑛‘𝑏)‘𝑦)⟩)    &   ⊢ 𝐺 = (◡(𝑛‘𝑏) ∘ (((𝐻 ∘ 𝐽) ∘ 𝑍) ∘ 𝑇))    ⇒   ⊢ (𝜑 → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
Theorem	infxpenc2lem3 10100*	Lemma for infxpenc2 10101. (Contributed by Mario Carneiro, 30-May-2015.) (Revised by AV, 7-Jul-2019.)
⊢ (𝜑 → 𝐴 ∈ On)    &   ⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖ 1o)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑o 𝑤)))    &   ⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1o) ↦ (ω ↑o 𝑥))‘ran (𝑛‘𝑏))    &   ⊢ (𝜑 → 𝐹:(ω ↑o 2o)–1-1-onto→ω)    &   ⊢ (𝜑 → (𝐹‘∅) = ∅)    ⇒   ⊢ (𝜑 → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))