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	domtri2 9901	Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴))
Theorem	nnsdomel 9902	Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014.)
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ 𝐴 ≺ 𝐵))
Theorem	cardval2 9903*	An alternate version of the value of the cardinal number of a set. Compare cardval 10456. This theorem could be used to give a simpler definition of card in place of df-card 9851. It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003.)
⊢ (𝐴 ∈ dom card → (card‘𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴})
Theorem	isinffi 9904*	An infinite set contains subsets equinumerous to every finite set. Extension of isinf 9165 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.)
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐵–1-1→𝐴)
Theorem	fidomtri 9905	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 9906	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 9907	The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ dom card → 𝐴 ≺ (har‘𝐴))
Theorem	onsdom 9908*	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 9909*	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 9910	The next cardinal after a finite ordinal is the successor ordinal. (Contributed by RP, 5-Nov-2023.)
⊢ (𝐴 ∈ ω → (har‘𝐴) = suc 𝐴)
Theorem	cardmin2 9911*	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 9912*	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 9880), 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 9913. (Contributed by NM, 4-Nov-2013.)
⊢ (𝐴 ≈ 1o ↔ 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o})
Theorem	pm54.43 9913	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 9880), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o} which is the same as 𝐴 ≈ 1o by pm54.43lem 9912. 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 10084 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.)
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o))
Theorem	enpr2 9914	An unordered pair with distinct elements is equinumerous to ordinal two. This is a closed-form version of enpr2d 8985. (Contributed by FL, 17-Aug-2008.) Avoid ax-pow 5310, ax-un 7680. (Revised by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o)
Theorem	pr2ne 9915	If an unordered pair has two elements, then they are different. (Contributed by FL, 14-Feb-2010.) Avoid ax-pow 5310, ax-un 7680. (Revised by BTernaryTau, 30-Dec-2024.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵))
Theorem	prdom2 9916	An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011.)
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐵} ≼ 2o)
Theorem	en2eqpr 9917	Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
⊢ ((𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ≠ 𝐵 → 𝐶 = {𝐴, 𝐵}))
Theorem	en2eleq 9918	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 9919	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 9920	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 9921*	Lexicographical order is a well-ordering of On × On. Proposition 7.56(1) of [TakeutiZaring] p. 54. Note that unlike r0weon 9922, 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 9922*	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 9923*	Lemma for infxpen 9924. (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 9924	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 9925	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 9926	The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017.)
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω)
Theorem	infxpidm2 9927	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 10472. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴)
Theorem	infxpenc 9928*	A canonical version of infxpen 9924, by a completely different approach (although it uses infxpen 9924 via xpomen 9925). Using Cantor's normal form, we can show that 𝐴 ↑o 𝐵 respects equinumerosity (oef1o 9607), 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 9615.) (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 9929*	Lemma for infxpenc2 9932. (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 9930*	Lemma for infxpenc2 9932. (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 9931*	Lemma for infxpenc2 9932. (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 9932*	Existence form of infxpenc 9928. A "uniform" or "canonical" version of infxpen 9924, 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 9933*	The union ∪ 𝑛 ∈ 𝐶(𝐴 ↑m 𝑛) is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.)
⊢ ∃*𝑛 ∈ 𝐶 𝐵 ∈ (𝐴 ↑m 𝑛)
Theorem	fseqenlem1 9934*	Lemma for fseqen 9937. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)    &   ⊢ 𝐺 = seqω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {⟨∅, 𝐵⟩})    ⇒   ⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑m 𝐶)–1-1→𝐴)
Theorem	fseqenlem2 9935*	Lemma for fseqen 9937. (Contributed by Mario Carneiro, 17-May-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴)    &   ⊢ 𝐺 = seqω((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑m suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {⟨∅, 𝐵⟩})    &   ⊢ 𝐾 = (𝑦 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘) ↦ ⟨dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)⟩)    ⇒   ⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑m 𝑘)–1-1→(ω × 𝐴))
Theorem	fseqdom 9936*	One half of fseqen 9937. (Contributed by Mario Carneiro, 18-Nov-2014.)
⊢ (𝐴 ∈ 𝑉 → (ω × 𝐴) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛))
Theorem	fseqen 9937*	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 9938	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 9939*	Lemma for dfac8a 9940. 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 9940*	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 9941*	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 9942*	Lemma for dfac8c 9943. (Contributed by Mario Carneiro, 10-Jan-2013.)
⊢ 𝐹 = (𝑠 ∈ (𝐴 ∖ {∅}) ↦ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎))    ⇒   ⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧)))
Theorem	dfac8c 9943*	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 9944*	A proof of the well-ordering theorem weth 10405, 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 9945*	A set is numerable iff it can be well-ordered. (Contributed by Mario Carneiro, 5-Jan-2013.)
⊢ (𝐴 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐴)
Theorem	ac5num 9946*	A version of ac5b 10388 with the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ ((∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥))
Theorem	ondomen 9947	If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card)
Theorem	numdom 9948	A set dominated by a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card)
Theorem	ssnum 9949	A subset of a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ dom card)
Theorem	onssnum 9950	All subsets of the ordinals are numerable. (Contributed by Mario Carneiro, 12-Feb-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On) → 𝐴 ∈ dom card)
Theorem	indcardi 9951*	Indirect strong induction on the cardinality of a finite or numerable set. (Contributed by Stefan O'Rear, 24-Aug-2015.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑇 ∈ dom card)    &   ⊢ ((𝜑 ∧ 𝑅 ≼ 𝑇 ∧ ∀𝑦(𝑆 ≺ 𝑅 → 𝜒)) → 𝜓)    &   ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆)    &   ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇)    ⇒   ⊢ (𝜑 → 𝜃)
Theorem	acnrcl 9952	Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑋 ∈ AC 𝐴 → 𝐴 ∈ V)
Theorem	acneq 9953	Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 = 𝐶 → AC 𝐴 = AC 𝐶)
Theorem	isacn 9954*	The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑓 ∈ ((𝒫 𝑋 ∖ {∅}) ↑m 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)))
Theorem	acni 9955*	The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝑋 ∈ AC 𝐴 ∧ 𝐹:𝐴⟶(𝒫 𝑋 ∖ {∅})) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝐹‘𝑥))
Theorem	acni2 9956*	The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝑋 ∈ AC 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝐵 ⊆ 𝑋 ∧ 𝐵 ≠ ∅)) → ∃𝑔(𝑔:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ 𝐵))
Theorem	acni3 9957*	The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑦 = (𝑔‘𝑥) → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((𝑋 ∈ AC 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝑋 𝜑) → ∃𝑔(𝑔:𝐴⟶𝑋 ∧ ∀𝑥 ∈ 𝐴 𝜓))
Theorem	acnlem 9958*	Construct a mapping satisfying the consequent of isacn 9954. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑓‘𝑥)) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥))
Theorem	numacn 9959	A well-orderable set has choice sequences of every length. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ∈ 𝑉 → (𝑋 ∈ dom card → 𝑋 ∈ AC 𝐴))
Theorem	finacn 9960	Every set has finite choice sequences. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ∈ Fin → AC 𝐴 = V)
Theorem	acndom 9961	A set with long choice sequences also has shorter choice sequences, where "shorter" here means the new index set is dominated by the old index set. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ≼ 𝐵 → (𝑋 ∈ AC 𝐵 → 𝑋 ∈ AC 𝐴))
Theorem	acnnum 9962	A set 𝑋 which has choice sequences on it of length 𝒫 𝑋 is well-orderable (and hence has choice sequences of every length). (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑋 ∈ AC 𝒫 𝑋 ↔ 𝑋 ∈ dom card)
Theorem	acnen 9963	The class of choice sets of length 𝐴 is a cardinal invariant. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ≈ 𝐵 → AC 𝐴 = AC 𝐵)
Theorem	acndom2 9964	A set smaller than one with choice sequences of length 𝐴 also has choice sequences of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑋 ≼ 𝑌 → (𝑌 ∈ AC 𝐴 → 𝑋 ∈ AC 𝐴))
Theorem	acnen2 9965	The class of sets with choice sequences of length 𝐴 is a cardinal invariant. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝑋 ≈ 𝑌 → (𝑋 ∈ AC 𝐴 ↔ 𝑌 ∈ AC 𝐴))
Theorem	fodomacn 9966	A version of fodom 10433 that doesn't require the Axiom of Choice ax-ac 10369. If 𝐴 has choice sequences of length 𝐵, then any surjection from 𝐴 to 𝐵 can be inverted to an injection the other way. (Contributed by Mario Carneiro, 31-Aug-2015.)
⊢ (𝐴 ∈ AC 𝐵 → (𝐹:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴))
Theorem	fodomnum 9967	A version of fodom 10433 that doesn't require the Axiom of Choice ax-ac 10369. (Contributed by Mario Carneiro, 28-Feb-2013.) (Revised by Mario Carneiro, 28-Apr-2015.)
⊢ (𝐴 ∈ dom card → (𝐹:𝐴–onto→𝐵 → 𝐵 ≼ 𝐴))
Theorem	fonum 9968	A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ∈ dom card)
Theorem	numwdom 9969	A surjection maps numerable sets to numerable sets. (Contributed by Mario Carneiro, 27-Aug-2015.)
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼* 𝐴) → 𝐵 ∈ dom card)
Theorem	fodomfi2 9970	Onto functions define dominance when a finite number of choices need to be made. (Contributed by Stefan O'Rear, 28-Feb-2015.)
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ∧ 𝐹:𝐴–onto→𝐵) → 𝐵 ≼ 𝐴)
Theorem	wdomfil 9971	Weak dominance agrees with normal for finite left sets. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ (𝑋 ∈ Fin → (𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌))
Theorem	infpwfien 9972	Any infinite well-orderable set is equinumerous to its set of finite subsets. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (𝒫 𝐴 ∩ Fin) ≈ 𝐴)
Theorem	inffien 9973	The set of finite intersections of an infinite well-orderable set is equinumerous to the set itself. (Contributed by Mario Carneiro, 18-May-2015.)
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (fi‘𝐴) ≈ 𝐴)
Theorem	wdomnumr 9974	Weak dominance agrees with normal for numerable right sets. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by Mario Carneiro, 5-May-2015.)
⊢ (𝐵 ∈ dom card → (𝐴 ≼* 𝐵 ↔ 𝐴 ≼ 𝐵))
Theorem	alephfnon 9975	The aleph function is a function on the class of ordinal numbers. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ ℵ Fn On
Theorem	aleph0 9976	The first infinite cardinal number, discovered by Georg Cantor in 1873, has the same size as the set of natural numbers ω (and under our particular definition is also equal to it). In the literature, the argument of the aleph function is often written as a subscript, and the first aleph is written ℵ0. Exercise 3 of [TakeutiZaring] p. 91. Also Definition 12(i) of [Suppes] p. 228. From Moshé Machover, Set Theory, Logic, and Their Limitations, p. 95: "Aleph ... the first letter in the Hebrew alphabet ... is also the first letter of the Hebrew word ... (einsoph, meaning infinity), which is a cabbalistic appellation of the deity. The notation is due to Cantor, who was deeply interested in mysticism." (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ (ℵ‘∅) = ω
Theorem	alephlim 9977*	Value of the aleph function at a limit ordinal. Definition 12(iii) of [Suppes] p. 91. (Contributed by NM, 21-Oct-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ ((𝐴 ∈ 𝑉 ∧ Lim 𝐴) → (ℵ‘𝐴) = ∪ 𝑥 ∈ 𝐴 (ℵ‘𝑥))
Theorem	alephsuc 9978	Value of the aleph function at a successor ordinal. Definition 12(ii) of [Suppes] p. 91. Here we express the successor aleph in terms of the Hartogs function df-har 9462, which gives the smallest ordinal that strictly dominates its argument (or the supremum of all ordinals that are dominated by the argument). (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ On → (ℵ‘suc 𝐴) = (har‘(ℵ‘𝐴)))
Theorem	alephon 9979	An aleph is an ordinal number. (Contributed by NM, 10-Nov-2003.) (Revised by Mario Carneiro, 13-Sep-2013.)
⊢ (ℵ‘𝐴) ∈ On
Theorem	alephcard 9980	Every aleph is a cardinal number. Theorem 65 of [Suppes] p. 229. (Contributed by NM, 25-Oct-2003.) (Revised by Mario Carneiro, 2-Feb-2013.)
⊢ (card‘(ℵ‘𝐴)) = (ℵ‘𝐴)
Theorem	alephnbtwn 9981	No cardinal can be sandwiched between an aleph and its successor aleph. Theorem 67 of [Suppes] p. 229. (Contributed by NM, 10-Nov-2003.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ ((card‘𝐵) = 𝐵 → ¬ ((ℵ‘𝐴) ∈ 𝐵 ∧ 𝐵 ∈ (ℵ‘suc 𝐴)))
Theorem	alephnbtwn2 9982	No set has equinumerosity between an aleph and its successor aleph. (Contributed by NM, 3-Nov-2003.) (Revised by Mario Carneiro, 2-Feb-2013.)
⊢ ¬ ((ℵ‘𝐴) ≺ 𝐵 ∧ 𝐵 ≺ (ℵ‘suc 𝐴))
Theorem	alephordilem1 9983	Lemma for alephordi 9984. (Contributed by NM, 23-Oct-2009.) (Revised by Mario Carneiro, 15-May-2015.)
⊢ (𝐴 ∈ On → (ℵ‘𝐴) ≺ (ℵ‘suc 𝐴))
Theorem	alephordi 9984	Strict ordering property of the aleph function. (Contributed by Mario Carneiro, 2-Feb-2013.)
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (ℵ‘𝐴) ≺ (ℵ‘𝐵)))
Theorem	alephord 9985	Ordering property of the aleph function. (Contributed by NM, 26-Oct-2003.) (Revised by Mario Carneiro, 9-Feb-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (ℵ‘𝐴) ≺ (ℵ‘𝐵)))
Theorem	alephord2 9986	Ordering property of the aleph function. Theorem 8A(a) of [Enderton] p. 213 and its converse. (Contributed by NM, 3-Nov-2003.) (Revised by Mario Carneiro, 9-Feb-2013.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ 𝐵 ↔ (ℵ‘𝐴) ∈ (ℵ‘𝐵)))
Theorem	alephord2i 9987	Ordering property of the aleph function. Theorem 66 of [Suppes] p. 229. (Contributed by NM, 25-Oct-2003.)
⊢ (𝐵 ∈ On → (𝐴 ∈ 𝐵 → (ℵ‘𝐴) ∈ (ℵ‘𝐵)))
Theorem	alephord3 9988	Ordering property of the aleph function. (Contributed by NM, 11-Nov-2003.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (ℵ‘𝐴) ⊆ (ℵ‘𝐵)))
Theorem	alephsucdom 9989	A set dominated by an aleph is strictly dominated by its successor aleph and vice-versa. (Contributed by NM, 3-Nov-2003.) (Revised by Mario Carneiro, 2-Feb-2013.)
⊢ (𝐵 ∈ On → (𝐴 ≼ (ℵ‘𝐵) ↔ 𝐴 ≺ (ℵ‘suc 𝐵)))
Theorem	alephsuc2 9990*	An alternate representation of a successor aleph. The aleph function is the function obtained from the hartogs 9449 function by transfinite recursion, starting from ω. Using this theorem we could define the aleph function with {𝑧 ∈ On ∣ 𝑧 ≼ 𝑥} in place of ∩ {𝑧 ∈ On ∣ 𝑥 ≺ 𝑧} in df-aleph 9852. (Contributed by NM, 3-Nov-2003.) (Revised by Mario Carneiro, 2-Feb-2013.)
⊢ (𝐴 ∈ On → (ℵ‘suc 𝐴) = {𝑥 ∈ On ∣ 𝑥 ≼ (ℵ‘𝐴)})
Theorem	alephdom 9991	Relationship between inclusion of ordinal numbers and dominance of infinite initial ordinals. (Contributed by Jeff Hankins, 23-Oct-2009.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (ℵ‘𝐴) ≼ (ℵ‘𝐵)))
Theorem	alephgeom 9992	Every aleph is greater than or equal to the set of natural numbers. (Contributed by NM, 11-Nov-2003.)
⊢ (𝐴 ∈ On ↔ ω ⊆ (ℵ‘𝐴))
Theorem	alephislim 9993	Every aleph is a limit ordinal. (Contributed by NM, 11-Nov-2003.)
⊢ (𝐴 ∈ On ↔ Lim (ℵ‘𝐴))
Theorem	aleph11 9994	The aleph function is one-to-one. (Contributed by NM, 3-Aug-2004.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((ℵ‘𝐴) = (ℵ‘𝐵) ↔ 𝐴 = 𝐵))
Theorem	alephf1 9995	The aleph function is a one-to-one mapping from the ordinals to the infinite cardinals. See also alephf1ALT 10013. (Contributed by Mario Carneiro, 2-Feb-2013.)
⊢ ℵ:On–1-1→On
Theorem	alephsdom 9996	If an ordinal is smaller than an initial ordinal, it is strictly dominated by it. (Contributed by Jeff Hankins, 24-Oct-2009.) (Proof shortened by Mario Carneiro, 20-Sep-2014.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∈ (ℵ‘𝐵) ↔ 𝐴 ≺ (ℵ‘𝐵)))
Theorem	alephdom2 9997	A dominated initial ordinal is included. (Contributed by Jeff Hankins, 24-Oct-2009.)
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((ℵ‘𝐴) ⊆ 𝐵 ↔ (ℵ‘𝐴) ≼ 𝐵))
Theorem	alephle 9998	The argument of the aleph function is less than or equal to its value. Exercise 2 of [TakeutiZaring] p. 91. (Later, in alephfp2 10019, we will that equality can sometimes hold.) (Contributed by NM, 9-Nov-2003.) (Proof shortened by Mario Carneiro, 22-Feb-2013.)
⊢ (𝐴 ∈ On → 𝐴 ⊆ (ℵ‘𝐴))
Theorem	cardaleph 9999*	Given any transfinite cardinal number 𝐴, there is exactly one aleph that is equal to it. Here we compute that aleph explicitly. (Contributed by NM, 9-Nov-2003.) (Revised by Mario Carneiro, 2-Feb-2013.)
⊢ ((ω ⊆ 𝐴 ∧ (card‘𝐴) = 𝐴) → 𝐴 = (ℵ‘∩ {𝑥 ∈ On ∣ 𝐴 ⊆ (ℵ‘𝑥)}))
Theorem	cardalephex 10000*	Every transfinite cardinal is an aleph and vice-versa. Theorem 8A(b) of [Enderton] p. 213 and its converse. (Contributed by NM, 5-Nov-2003.)
⊢ (ω ⊆ 𝐴 → ((card‘𝐴) = 𝐴 ↔ ∃𝑥 ∈ On 𝐴 = (ℵ‘𝑥)))