P. 100 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9901-10000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	djueq2 9901	Equality theorem for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
⊢ (𝐴 = 𝐵 → (𝐶 ⊔ 𝐴) = (𝐶 ⊔ 𝐵))
Theorem	nfdju 9902	Bound-variable hypothesis builder for disjoint union. (Contributed by Jim Kingdon, 23-Jun-2022.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥(𝐴 ⊔ 𝐵)
Theorem	djuex 9903	The disjoint union of sets is a set. For a shorter proof using djuss 9915 see djuexALT 9917. (Contributed by AV, 28-Jun-2022.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⊔ 𝐵) ∈ V)
Theorem	djuexb 9904	The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023.)
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐴 ⊔ 𝐵) ∈ V)
Theorem	djulcl 9905	Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.)
⊢ (𝐶 ∈ 𝐴 → (inl‘𝐶) ∈ (𝐴 ⊔ 𝐵))
Theorem	djurcl 9906	Right closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022.)
⊢ (𝐶 ∈ 𝐵 → (inr‘𝐶) ∈ (𝐴 ⊔ 𝐵))
Theorem	djulf1o 9907	The left injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.)
⊢ inl:V–1-1-onto→({∅} × V)
Theorem	djurf1o 9908	The right injection function on all sets is one to one and onto. (Contributed by Jim Kingdon, 22-Jun-2022.)
⊢ inr:V–1-1-onto→({1o} × V)
Theorem	inlresf 9909	The left injection restricted to the left class of a disjoint union is a function from the left class into the disjoint union. (Contributed by AV, 27-Jun-2022.)
⊢ (inl ↾ 𝐴):𝐴⟶(𝐴 ⊔ 𝐵)
Theorem	inlresf1 9910	The left injection restricted to the left class of a disjoint union is an injective function from the left class into the disjoint union. (Contributed by AV, 28-Jun-2022.)
⊢ (inl ↾ 𝐴):𝐴–1-1→(𝐴 ⊔ 𝐵)
Theorem	inrresf 9911	The right injection restricted to the right class of a disjoint union is a function from the right class into the disjoint union. (Contributed by AV, 27-Jun-2022.)
⊢ (inr ↾ 𝐵):𝐵⟶(𝐴 ⊔ 𝐵)
Theorem	inrresf1 9912	The right injection restricted to the right class of a disjoint union is an injective function from the right class into the disjoint union. (Contributed by AV, 28-Jun-2022.)
⊢ (inr ↾ 𝐵):𝐵–1-1→(𝐴 ⊔ 𝐵)
Theorem	djuin 9913	The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.)
⊢ ((inl “ 𝐴) ∩ (inr “ 𝐵)) = ∅
Theorem	djur 9914*	A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.)
⊢ (𝐶 ∈ (𝐴 ⊔ 𝐵) → (∃𝑥 ∈ 𝐴 𝐶 = (inl‘𝑥) ∨ ∃𝑥 ∈ 𝐵 𝐶 = (inr‘𝑥)))
Theorem	djuss 9915	A disjoint union is a subclass of a Cartesian product. (Contributed by AV, 25-Jun-2022.)
⊢ (𝐴 ⊔ 𝐵) ⊆ ({∅, 1o} × (𝐴 ∪ 𝐵))
Theorem	djuunxp 9916	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 9917	Alternate proof of djuex 9903, 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 9918	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 9919	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 9920	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 9921	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 9922	The first component of the value of a left injection is the empty set. (Contributed by AV, 27-Jun-2022.)
⊢ (𝑋 ∈ 𝑉 → (1st ‘(inl‘𝑋)) = ∅)
Theorem	2ndinl 9923	The second component of the value of a left injection is its argument. (Contributed by AV, 27-Jun-2022.)
⊢ (𝑋 ∈ 𝑉 → (2nd ‘(inl‘𝑋)) = 𝑋)
Theorem	1stinr 9924	The first component of the value of a right injection is 1o. (Contributed by AV, 27-Jun-2022.)
⊢ (𝑋 ∈ 𝑉 → (1st ‘(inr‘𝑋)) = 1o)
Theorem	2ndinr 9925	The second component of the value of a right injection is its argument. (Contributed by AV, 27-Jun-2022.)
⊢ (𝑋 ∈ 𝑉 → (2nd ‘(inr‘𝑋)) = 𝑋)
Theorem	updjudhf 9926*	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 9927*	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 9928*	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 9929*	Universal property of the disjoint union. This theorem shows that the disjoint union, together with the left and right injections df-inl 9897 and df-inr 9898, is the coproduct in the category of sets, see Wikipedia "Coproduct", https://en.wikipedia.org/wiki/Coproduct 9898 (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.11  Cardinal numbers
Syntax	ccrd 9930	Extend class definition to include the cardinal size function.
class card
Syntax	cale 9931	Extend class definition to include the aleph function.
class ℵ
Syntax	ccf 9932	Extend class definition to include the cofinality function.
class cf
Syntax	wacn 9933	The axiom of choice for limited-length sequences.
class AC 𝐴
Definition	df-card 9934*	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 10541 for its value and cardval2 9986 for a simpler version of its value. The principal theorem relating cardinality to equinumerosity is carden 10546. 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 9935	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 10061, alephsuc 10063, and alephlim 10062. 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 9936*	Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). See cfval 10242 for its value and a description. (Contributed by NM, 1-Apr-2004.)
⊢ cf = (𝑥 ∈ On ↦ ∩ {𝑦 ∣ ∃𝑧(𝑦 = (card‘𝑧) ∧ (𝑧 ⊆ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ∃𝑢 ∈ 𝑧 𝑣 ⊆ 𝑢))})
Definition	df-acn 9937*	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 9938*	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 9939	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 9940*	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 9941	A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ dom card)
Theorem	ennum 9942	Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ dom card ↔ 𝐵 ∈ dom card))
Theorem	finnum 9943	Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)
Theorem	onenon 9944	Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ On → 𝐴 ∈ dom card)
Theorem	tskwe 9945*	A Tarski set is well-orderable. (Contributed by Mario Carneiro, 19-Apr-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → 𝐴 ∈ dom card)
Theorem	xpnum 9946	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 9947*	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 9948	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 9949	A set is numerable iff it is equinumerous with its cardinal. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ dom card ↔ (card‘𝐴) ≈ 𝐴)
Theorem	oncardval 9950*	The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 10541, 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 9951	Any ordinal number is equinumerous to its cardinal number. Unlike cardid 10542, this theorem does not require the Axiom of Choice. (Contributed by NM, 26-Jul-2004.)
⊢ (𝐴 ∈ On → (card‘𝐴) ≈ 𝐴)
Theorem	cardonle 9952	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 9953	The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)
⊢ (card‘∅) = ∅
Theorem	cardidm 9954	The cardinality function is idempotent. Proposition 10.11 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.)
⊢ (card‘(card‘𝐴)) = (card‘𝐴)
Theorem	oncard 9955*	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 9956	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 9957	A finite set is equinumerous to its cardinal number. (Contributed by Mario Carneiro, 21-Sep-2013.)
⊢ (𝐴 ∈ Fin → (card‘𝐴) ≈ 𝐴)
Theorem	cardnn 9958	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 9959	The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013.)
⊢ (𝐴 ∈ dom card → ((card‘𝐴) = ∅ ↔ 𝐴 = ∅))
Theorem	cardne 9960	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 9961	If two sets have equal nonzero cardinalities, then they are equinumerous. This assertion and carden2b 9962 are meant to replace carden 10546 in ZF without AC. (Contributed by Mario Carneiro, 9-Jan-2013.)
⊢ (((card‘𝐴) = (card‘𝐵) ∧ (card‘𝐴) ≠ ∅) → 𝐴 ≈ 𝐵)
Theorem	carden2b 9962	If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a 9961 are meant to replace carden 10546 in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) = (card‘𝐵))
Theorem	card1 9963*	A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013.)
⊢ ((card‘𝐴) = 1o ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	cardsn 9964	A singleton has cardinality one. (Contributed by Mario Carneiro, 10-Jan-2013.)
⊢ (𝐴 ∈ 𝑉 → (card‘{𝐴}) = 1o)
Theorem	carddomi2 9965	Two sets have the dominance relationship if their cardinalities have the subset relationship and one is numerable. See also carddom 10549, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ 𝑉) → ((card‘𝐴) ⊆ (card‘𝐵) → 𝐴 ≼ 𝐵))
Theorem	sdomsdomcardi 9966	A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ (𝐴 ≺ (card‘𝐵) → 𝐴 ≺ 𝐵)
Theorem	cardlim 9967	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 9968	A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. This is half of the assertion cardsdomel 9969 and can be proven without the AC. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ (𝐴 ∈ (card‘𝐵) → 𝐴 ≺ 𝐵)
Theorem	cardsdomel 9969	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 9970*	Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴))
Theorem	iscard2 9971*	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 9972	Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 10549, 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 9973	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 9974*	Lemma for cardprc 9975. (Contributed by Mario Carneiro, 22-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ 𝐴 = {𝑥 ∣ (card‘𝑥) = 𝑥}    ⇒   ⊢ ¬ 𝐴 ∈ V
Theorem	cardprc 9975	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 10556 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs 9539 to construct (effectively) (ℵ‘suc 𝐴) from (ℵ‘𝐴), which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013.)
⊢ {𝑥 ∣ (card‘𝑥) = 𝑥} ∉ V
Theorem	carduni 9976*	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 9977*	The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵 → (card‘∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 𝐵))
Theorem	cardennn 9978	If 𝐴 is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ ω) → (card‘𝐴) = 𝐵)
Theorem	cardsucinf 9979	The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013.)
⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (card‘suc 𝐴) = (card‘𝐴))
Theorem	cardsucnn 9980	The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 9979. (Contributed by NM, 7-Nov-2008.)
⊢ (𝐴 ∈ ω → (card‘suc 𝐴) = suc (card‘𝐴))
Theorem	cardom 9981	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 9982	Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden 10546, the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) = (card‘𝐵) ↔ 𝐴 ≈ 𝐵))
Theorem	cardsdom2 9983	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 9984	Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴))
Theorem	nnsdomel 9985	Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ 𝐴 ≺ 𝐵))
Theorem	cardval2 9986*	An alternate version of the value of the cardinal number of a set. Compare cardval 10541. This theorem could be used to give a simpler definition of card in place of df-card 9934. It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003.)
⊢ (𝐴 ∈ dom card → (card‘𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})
Theorem	isinffi 9987*	An infinite set contains subsets equinumerous to every finite set. Extension of isinf 9260 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐵–1-1→𝐴)
Theorem	fidomtri 9988	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 9989	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 9990	The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ dom card → 𝐴 ≺ (har‘𝐴))
Theorem	onsdom 9991*	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 9992*	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 9993	The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.)
⊢ (𝐴 ∈ ω → (har‘𝐴) = suc 𝐴)
Theorem	cardmin2 9994*	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 9995*	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 9963), 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 9996. (Contributed by NM, 4-Nov-2013.)
⊢ (𝐴 ≈ 1o ↔ 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o})
Theorem	pm54.43 9996	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 9963), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o} which is the same as 𝐴 ≈ 1o by pm54.43lem 9995. 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 10168 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.)
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o))
Theorem	enpr2 9997	An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d 9049. (Contributed by FL, 17-Aug-2008.) Avoid ax-pow 5364, ax-un 7725. (Revised by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o)
Theorem	pr2nelemOLD 9998	Obsolete version of enpr2 9997 as of 30-Dec-2024. (Contributed by FL, 17-Aug-2008.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o)
Theorem	pr2ne 9999	If an unordered pair has two elements, then they are different. (Contributed by FL, 14-Feb-2010.) Avoid ax-pow 5364, ax-un 7725. (Revised by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵))
Theorem	pr2neOLD 10000	Obsolete version of pr2ne 9999 as of 30-Dec-2024. (Contributed by FL, 14-Feb-2010.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵))