P. 98 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9701-9800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cardf2 9701*	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 9702	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 9703*	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 9704	A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ dom card)
Theorem	ennum 9705	Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ dom card ↔ 𝐵 ∈ dom card))
Theorem	finnum 9706	Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card)
Theorem	onenon 9707	Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ On → 𝐴 ∈ dom card)
Theorem	tskwe 9708*	A Tarski set is well-orderable. (Contributed by Mario Carneiro, 19-Apr-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → 𝐴 ∈ dom card)
Theorem	xpnum 9709	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 9710*	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 9711	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 9712	A set is numerable iff it is equinumerous with its cardinal. (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ dom card ↔ (card‘𝐴) ≈ 𝐴)
Theorem	oncardval 9713*	The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 10302, 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 9714	Any ordinal number is equinumerous to its cardinal number. Unlike cardid 10303, this theorem does not require the Axiom of Choice. (Contributed by NM, 26-Jul-2004.)
⊢ (𝐴 ∈ On → (card‘𝐴) ≈ 𝐴)
Theorem	cardonle 9715	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 9716	The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.)
⊢ (card‘∅) = ∅
Theorem	cardidm 9717	The cardinality function is idempotent. Proposition 10.11 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.)
⊢ (card‘(card‘𝐴)) = (card‘𝐴)
Theorem	oncard 9718*	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 9719	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 9720	A finite set is equinumerous to its cardinal number. (Contributed by Mario Carneiro, 21-Sep-2013.)
⊢ (𝐴 ∈ Fin → (card‘𝐴) ≈ 𝐴)
Theorem	cardnn 9721	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 9722	The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013.)
⊢ (𝐴 ∈ dom card → ((card‘𝐴) = ∅ ↔ 𝐴 = ∅))
Theorem	cardne 9723	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 9724	If two sets have equal nonzero cardinalities, then they are equinumerous. This assertion and carden2b 9725 are meant to replace carden 10307 in ZF without AC. (Contributed by Mario Carneiro, 9-Jan-2013.)
⊢ (((card‘𝐴) = (card‘𝐵) ∧ (card‘𝐴) ≠ ∅) → 𝐴 ≈ 𝐵)
Theorem	carden2b 9725	If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a 9724 are meant to replace carden 10307 in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.)
⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) = (card‘𝐵))
Theorem	card1 9726*	A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013.)
⊢ ((card‘𝐴) = 1o ↔ ∃𝑥 𝐴 = {𝑥})
Theorem	cardsn 9727	A singleton has cardinality one. (Contributed by Mario Carneiro, 10-Jan-2013.)
⊢ (𝐴 ∈ 𝑉 → (card‘{𝐴}) = 1o)
Theorem	carddomi2 9728	Two sets have the dominance relationship if their cardinalities have the subset relationship and one is numerable. See also carddom 10310, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ 𝑉) → ((card‘𝐴) ⊆ (card‘𝐵) → 𝐴 ≼ 𝐵))
Theorem	sdomsdomcardi 9729	A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013.)
⊢ (𝐴 ≺ (card‘𝐵) → 𝐴 ≺ 𝐵)
Theorem	cardlim 9730	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 9731	A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. This is half of the assertion cardsdomel 9732 and can be proven without the AC. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ (𝐴 ∈ (card‘𝐵) → 𝐴 ≺ 𝐵)
Theorem	cardsdomel 9732	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 9733*	Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013.)
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴))
Theorem	iscard2 9734*	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 9735	Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 10310, 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 9736	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 9737*	Lemma for cardprc 9738. (Contributed by Mario Carneiro, 22-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ 𝐴 = {𝑥 ∣ (card‘𝑥) = 𝑥}    ⇒   ⊢ ¬ 𝐴 ∈ V
Theorem	cardprc 9738	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 10317 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs 9303 to construct (effectively) (ℵ‘suc 𝐴) from (ℵ‘𝐴), which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013.)
⊢ {𝑥 ∣ (card‘𝑥) = 𝑥} ∉ V
Theorem	carduni 9739*	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 9740*	The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003.)
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵 → (card‘∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 𝐵))
Theorem	cardennn 9741	If 𝐴 is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013.)
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ ω) → (card‘𝐴) = 𝐵)
Theorem	cardsucinf 9742	The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013.)
⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (card‘suc 𝐴) = (card‘𝐴))
Theorem	cardsucnn 9743	The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 9742. (Contributed by NM, 7-Nov-2008.)
⊢ (𝐴 ∈ ω → (card‘suc 𝐴) = suc (card‘𝐴))
Theorem	cardom 9744	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 9745	Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden 10307, the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) = (card‘𝐵) ↔ 𝐴 ≈ 𝐵))
Theorem	cardsdom2 9746	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 9747	Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴))
Theorem	nnsdomel 9748	Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ 𝐴 ≺ 𝐵))
Theorem	cardval2 9749*	An alternate version of the value of the cardinal number of a set. Compare cardval 10302. This theorem could be used to give a simpler definition of card in place of df-card 9697. It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003.)
⊢ (𝐴 ∈ dom card → (card‘𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})
Theorem	isinffi 9750*	An infinite set contains subsets equinumerous to every finite set. Extension of isinf 9036 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐵–1-1→𝐴)
Theorem	fidomtri 9751	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 9752	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 9753	The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ dom card → 𝐴 ≺ (har‘𝐴))
Theorem	onsdom 9754*	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 9755*	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 9756	The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.)
⊢ (𝐴 ∈ ω → (har‘𝐴) = suc 𝐴)
Theorem	cardmin2 9757*	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 9758*	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 9726), 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 9759. (Contributed by NM, 4-Nov-2013.)
⊢ (𝐴 ≈ 1o ↔ 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o})
Theorem	pm54.43 9759	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 9726), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o} which is the same as 𝐴 ≈ 1o by pm54.43lem 9758. 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 9929 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.)
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o))
Theorem	pr2nelem 9760	Lemma for pr2ne 9761. (Contributed by FL, 17-Aug-2008.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o)
Theorem	pr2ne 9761	If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵))
Theorem	prdom2 9762	An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐵} ≼ 2o)
Theorem	en2eqpr 9763	Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ≠ 𝐵 → 𝐶 = {𝐴, 𝐵}))
Theorem	en2eleq 9764	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 9765	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 9766	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 9767*	Lexicographical order is a well-ordering of On × On. Proposition 7.56(1) of [TakeutiZaring] p. 54. Note that unlike r0weon 9768, 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 9768*	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 9769*	Lemma for infxpen 9770. (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 9770	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 9771	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 9772	The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω)
Theorem	infxpidm2 9773	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 10318. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
Theorem	infxpenc 9774*	A canonical version of infxpen 9770, by a completely different approach (although it uses infxpen 9770 via xpomen 9771). Using Cantor's normal form, we can show that 𝐴 ↑o 𝐵 respects equinumerosity (oef1o 9456), 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 9464.) (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 9775*	Lemma for infxpenc2 9778. (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 9776*	Lemma for infxpenc2 9778. (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 9777*	Lemma for infxpenc2 9778. (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→𝑏))
Theorem	infxpenc2 9778*	Existence form of infxpenc 9774. A "uniform" or "canonical" version of infxpen 9770, asserting the existence of a single function 𝑔 that simultaneously demonstrates product idempotence of all ordinals below a given bound. (Contributed by Mario Carneiro, 30-May-2015.)
⊢ (𝐴 ∈ On → ∃𝑔∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → (𝑔‘𝑏):(𝑏 × 𝑏)–1-1-onto→𝑏))
Theorem	iunmapdisj 9779*	The union ∪ 𝑛 ∈ 𝐶(𝐴 ↑m 𝑛) is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.)
⊢ ∃*𝑛 ∈ 𝐶 𝐵 ∈ (𝐴 ↑m 𝑛)
Theorem	fseqenlem1 9780*	Lemma for fseqen 9783. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)    &   ⊢ 𝐺 = seqω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {⟨∅, 𝐵⟩})    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑m 𝐶)–1-1→𝐴)
Theorem	fseqenlem2 9781*	Lemma for fseqen 9783. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)    &   ⊢ 𝐺 = seqω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {⟨∅, 𝐵⟩})    &   ⊢ 𝐾 = (𝑦 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘) ↦ ⟨dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)⟩)    ⇒   ⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)–1-1→(ω × 𝐴))
Theorem	fseqdom 9782*	One half of fseqen 9783. (Contributed by Mario Carneiro, 18-Nov-2014.)
⊢ (𝐴 ∈ 𝑉 → (ω × 𝐴) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))
Theorem	fseqen 9783*	A set that is equinumerous to its Cartesian product is equinumerous to the set of finite sequences on it. (This can be proven more easily using some choice but this proof avoids it.) (Contributed by Mario Carneiro, 18-Nov-2014.)
⊢ (((𝐴 × 𝐴) ≈ 𝐴 ∧ 𝐴 ≠ ∅) → ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ≈ (ω × 𝐴))
Theorem	infpwfidom 9784	The collection of finite subsets of a set dominates the set. (We use the weaker sethood assumption (𝒫 𝐴 ∩ Fin) ∈ V because this theorem also implies that 𝐴 is a set if 𝒫 𝐴 ∩ Fin is.) (Contributed by Mario Carneiro, 17-May-2015.)
⊢ ((𝒫 𝐴 ∩ Fin) ∈ V → 𝐴 ≼ (𝒫 𝐴 ∩ Fin))
Theorem	dfac8alem 9785*	Lemma for dfac8a 9786. If the power set of a set has a choice function, then the set is numerable. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 5-Jan-2013.)
⊢ 𝐹 = recs(𝐺)    &   ⊢ 𝐺 = (𝑓 ∈ V ↦ (𝑔‘(𝐴 ∖ ran 𝑓)))    ⇒   ⊢ (𝐴 ∈ 𝐶 → (∃𝑔∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝑔‘𝑦) ∈ 𝑦) → 𝐴 ∈ dom card))
Theorem	dfac8a 9786*	Numeration theorem: every set with a choice function on its power set is numerable. With AC, this reduces to the statement that every set is numerable. Similar to Theorem 10.3 of [TakeutiZaring] p. 84. (Contributed by NM, 10-Feb-1997.) (Revised by Mario Carneiro, 5-Jan-2013.)
⊢ (𝐴 ∈ 𝐵 → (∃ℎ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (ℎ‘𝑦) ∈ 𝑦) → 𝐴 ∈ dom card))
Theorem	dfac8b 9787*	The well-ordering theorem: every numerable set is well-orderable. (Contributed by Mario Carneiro, 5-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ (𝐴 ∈ dom card → ∃𝑥 𝑥 We 𝐴)
Theorem	dfac8clem 9788*	Lemma for dfac8c 9789. (Contributed by Mario Carneiro, 10-Jan-2013.)
⊢ 𝐹 = (𝑠 ∈ (𝐴 ∖ {∅}) ↦ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
Theorem	dfac8c 9789*	If the union of a set is well-orderable, then the set has a choice function. (Contributed by Mario Carneiro, 5-Jan-2013.)
⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
Theorem	ac10ct 9790*	A proof of the well-ordering theorem weth 10251, an Axiom of Choice equivalent, restricted to sets dominated by some ordinal (in particular finite sets and countable sets), proven in ZF without AC. (Contributed by Mario Carneiro, 5-Jan-2013.)
⊢ (∃𝑦 ∈ On 𝐴 ≼ 𝑦 → ∃𝑥 𝑥 We 𝐴)
Theorem	ween 9791*	A set is numerable iff it can be well-ordered. (Contributed by Mario Carneiro, 5-Jan-2013.)
⊢ (𝐴 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐴)
Theorem	ac5num 9792*	A version of ac5b 10234 with the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ ((∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥))
Theorem	ondomen 9793	If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card)
Theorem	numdom 9794	A set dominated by a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card)
Theorem	ssnum 9795	A subset of a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ dom card)
Theorem	onssnum 9796	All subsets of the ordinals are numerable. (Contributed by Mario Carneiro, 12-Feb-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On) → 𝐴 ∈ dom card)
Theorem	indcardi 9797*	Indirect strong induction on the cardinality of a finite or numerable set. (Contributed by Stefan O'Rear, 24-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ dom card)    &   ⊢ ((𝜑 ∧ 𝑅 ≼ 𝑇 ∧ ∀𝑦(𝑆 ≺ 𝑅 → 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)    &   ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	acnrcl 9798	Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑋 ∈ AC 𝐴 → 𝐴 ∈ V)
Theorem	acneq 9799	Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 = 𝐶 → AC 𝐴 = AC 𝐶)
Theorem	isacn 9800*	The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑓 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)))