Metamath Proof Explorer - mmtheorems37

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Statement List for Metamath Proof Explorer - 3601-3700 - Page 37 of 58

Type	Label	Description
Statement
Theorem	numthcor 3601	Any set is strictly dominated by some ordinal.
⊢ (A ∈ B → ∃x ∈ On A ≺ x)
Theorem	weth 3602	Well-ordering theorem: any set A can be well-ordered. This is an equivalent of the Axiom of Choice. Theorem 6 of [Suppes] p. 242.
⊢ A ∈ V    ⇒   ⊢ ∃x x We A
Theorem	zornlem1 3603	Lemma for Zorn's lemma.
⊢ A ∈ V    &   ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}    &   ⊢ F = ∪B    &   ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}    &   ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}    &   ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}    ⇒   ⊢ ((x ∈ On ∧ (w We A ∧ ¬ D = ∅)) → (F ‘x) ∈ D)
Theorem	zornlem2 3604	Lemma for Zorn's lemma.
⊢ A ∈ V    &   ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}    &   ⊢ F = ∪B    &   ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}    &   ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}    &   ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}    ⇒   ⊢ ((x ∈ On ∧ (w We A ∧ ¬ D = ∅)) → (y ∈ x → (F ‘y)R(F ‘x)))
Theorem	zornlem3 3605	Lemma for Zorn's lemma.
⊢ A ∈ V    &   ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}    &   ⊢ F = ∪B    &   ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}    &   ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}    &   ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}    ⇒   ⊢ ((R Po A ∧ (x ∈ On ∧ (w We A ∧ ¬ D = ∅))) → (y ∈ x → ¬ (F ‘x) = (F ‘y)))
Theorem	zornlem4 3606	Lemma for Zorn's lemma.
⊢ A ∈ V    &   ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}    &   ⊢ F = ∪B    &   ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}    &   ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}    &   ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}    ⇒   ⊢ ((R Po A ∧ w We A) → ∃x ∈ On D = ∅)
Theorem	zornlem5 3607	Lemma for Zorn's lemma.
⊢ A ∈ V    &   ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}    &   ⊢ F = ∪B    &   ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}    &   ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}    &   ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}    &   ⊢ H = {z ∈ A∣∀g ∈ (F “ y)gRz}    ⇒   ⊢ (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → (F “ x) ⊆ A)
Theorem	zornlem6 3608	Lemma for Zorn's lemma.
⊢ A ∈ V    &   ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}    &   ⊢ F = ∪B    &   ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}    &   ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}    &   ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}    &   ⊢ H = {z ∈ A∣∀g ∈ (F “ y)gRz}    ⇒   ⊢ (R Po A → (((w We A ∧ x ∈ On) ∧ ∀y ∈ x ¬ H = ∅) → R Or (F “ x)))
Theorem	zornlem7 3609	Lemma for Zorn's lemma.
⊢ A ∈ V    &   ⊢ B = {f∣∃h ∈ On (f Fn h ∧ ∀t ∈ h (f ‘t) = (G ‘(f ↾ t)))}    &   ⊢ F = ∪B    &   ⊢ C = {z ∈ A∣∀g ∈ ran fgRz}    &   ⊢ D = {z ∈ A∣∀g ∈ (F “ x)gRz}    &   ⊢ G = {⟨f, t⟩∣t = ∪{v ∈ C∣∀u ∈ C ¬ uwv}}    &   ⊢ H = {z ∈ A∣∀g ∈ (F “ y)gRz}    ⇒   ⊢ ((R Po A ∧ ∀s((s ⊆ A ∧ R Or s) → ∃a ∈ A ∀r ∈ s (rRa ∨ r = a))) → ∃a ∈ A ∀b ∈ A ¬ aRb)
Theorem	zorn2lem 3610	Lemma for zorn2 3612.
⊢ (z{⟨x, y⟩∣x ⊂ y}w ↔ z ⊂ w)
Theorem	zorn 3611	Zorn's Lemma of [Monk1] p. 117. This theorem is equivalent to the Axiom of Choice and states that every partially ordered set A (with an ordering relation R) in which every totally ordered subset has an upper bound, contains at least one maximal element. The main proof consists of lemmas zornlem1 3603 through zornlem7 3609; this final piece mainly changes bound variables to eliminate the hypotheses of zornlem7 3609.
⊢ A ∈ V    ⇒   ⊢ ((R Po A ∧ ∀w((w ⊆ A ∧ R Or w) → ∃x ∈ A ∀z ∈ w (zRx ∨ z = x))) → ∃x ∈ A ∀y ∈ A ¬ xRy)
Theorem	zorn2 3612	Zorn's Lemma. If the union of every chain (with respect to inclusion) in a set belongs to the set, then the set contains a maximal element. This theorem is equivalent to the Axiom of Choice. Theorem 6M of [Enderton] p. 151.
⊢ A ∈ V    ⇒   ⊢ (∀z((z ⊆ A ∧ ∀x ∈ z ∀y ∈ z (x ⊆ y ∨ y ⊆ x)) → ∪z ∈ A) → ∃x ∈ A ∀y ∈ A ¬ x ⊂ y)
Theorem	fodom 3613	An onto function implies dominance of range over domain. Lemma 10.20 of [Kunen] p. 30. This theorem uses the Axiom of Choice ac7g 3570.
⊢ A ∈ V    ⇒   ⊢ (F:A–onto→B → B ≼ A)
Theorem	fodomg 3614	An onto function implies dominance of range over domain.
⊢ (A ∈ C → (F:A–onto→B → B ≼ A))
Theorem	fodomb 3615	Equivalence of an onto mapping and dominance for a non-empty set. Proposition 10.35 of [TakeutiZaring] p. 93.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ((¬ A = ∅ ∧ ∃f f:A–onto→B) ↔ (∅ ≺ B ∧ B ≼ A))
Theorem	imadomg 3616	An image of a function under a set is dominated by the set. Proposition 10.34 of [TakeutiZaring] p. 92.
⊢ (A ∈ B → (Fun F → (F “ A) ≼ A))
Theorem	fnrndomg 3617	The range of a function is dominated by its domain.
⊢ (A ∈ B → (F Fn A → ran F ≼ A))
Theorem	htalem 3618	Lemma for defining an emulation of Hilbert's epsilon. Hilbert's epsilon is described at http://plato.stanford.edu/entries/epsilon-calculus/. This theorem is equivalent to Hilbert's "transfinite axiom," described on that page, with the additional R We A antecedent. The element B is the epsilon that the theorem emulates.
⊢ A ∈ V    &   ⊢ B = ∪{x ∈ A∣∀y ∈ A ¬ yRx}    ⇒   ⊢ ((R We A ∧ ¬ A = ∅) → B ∈ A)
Theorem	hta 3619	A ZFC emulation of Hilbert's transfinite axiom. The set B has the properties of Hilbert's epsilon, except that it also depends on a well-ordering R. This theorem arose from discussions with Raph Levien on 5-Mar-04 about translating the HOL proof language, which uses Hilbert's epsilon. Hilbert's epsilon is described at http://plato.stanford.edu/entries/epsilon-calculus/. This theorem differs from Hilbert's transfinite axiom described on that page in that it requires R We A as an antecedent. Class A collects the sets of least rank for which φ(x) is true. Class B, which emulates the epsilon, is the minimum element in a well-ordering R on A. If a well-ordering R on A can be expressed in a closed form, as might be the case if we are working with say natural numbers, we can eliminate the antecedent with modus ponens, giving us the exact equivalent of Hilbert's transfinite axiom. Otherwise, we replace R with a dummy set variable, say w, and attach w We A as an antecedent in each step of the ZFC version of the HOL proof until the epsilon is eliminated. At that point, B (which will have w as a free variable) will no longer be present, and we can eliminate w We A by applying 19.23aiv 952 and weth 3602, using scottexs 3543 to establish the existence of A. For a version of this theorem scheme using class (meta)variables instead of wff (meta)variables, see htalem 3618.
⊢ A = {x∣(φ ∧ ∀y([y / x]φ → (rank ‘x) ⊆ (rank ‘y)))}    &   ⊢ B = ∪{x ∈ A∣∀y ∈ A ¬ yRx}    ⇒   ⊢ (R We A → (φ → [B / x]φ))
Syntax	ccrd 3620	Extend class definition to include the cardinal size function.
class card
Syntax	cale 3621	Extend class definition to include the aleph function.
class ℵ
Syntax	ccf 3622	Extend class definition to include the cofinality function.
class cf
Definition	df-card 3623	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 3633 for its value, cardval2 3661 for a simpler version of its value. The principle theorem relating cardinality to equinumerosity is carden 3638. Our notation is from Enderton. Other textbooks often use a double bar over the set to express this function.
⊢ card = {⟨x, y⟩∣y = ∩{z ∈ On∣z ≈ x}}
Definition	df-aleph 3624	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 3669, alephsuc 3672, and alephlim 3670. 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.
⊢ ℵ = rec({⟨x, y⟩∣y = ∩{z ∈ On∣x ≺ z}}, ω)
Definition	df-cf 3625	Define the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx. See cfval 3701 for its value and a description.
⊢ cf = {⟨x, y⟩∣(x ∈ On ∧ y = ∩{z∣∃w(z = (card ‘w) ∧ (w ⊆ x ∧ ∀v ∈ x ∃u ∈ w v ⊆ u))})}
Theorem	oncardval 3626	The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 3633, this theorem does not require the Axiom of Choice.
⊢ (A ∈ On → (card ‘A) = ∩{x ∈ On∣x ≈ A})
Theorem	oncardon 3627	The cardinal number of an ordinal number is an ordinal number. Unlike cardon 3634, this theorem does not require the Axiom of Choice.
⊢ (A ∈ On → (card ‘A) ∈ On)
Theorem	oncardid 3628	Any ordinal number is equinumerous to its cardinal number. Unlike cardid 3635, this theorem does not require the Axiom of Choice.
⊢ (A ∈ On → (card ‘A) ≈ A)
Theorem	cardonle 3629	The cardinal of an ordinal number is less than or equal to the ordinal number. Proposition 10.6(3) of [TakeutiZaring] p. 85.
⊢ (A ∈ On → (card ‘A) ⊆ A)
Theorem	card0 3630	The cardinality of the empty set is the empty set.
⊢ (card ‘∅) = ∅
Theorem	cardnn 3631	The cardinality of a natural number is the number. Corollary 10.23 of [TakeutiZaring] p. 90.
⊢ (A ∈ ω → (card ‘A) = A)
Theorem	cardom 3632	The set of natural numbers is a cardinal number. Theorem 18.11 of [Monk1] p. 133.
⊢ (card ‘ω) = ω
Theorem	cardval 3633	The value of the cardinal number function. Definition 10.4 of [TakeutiZaring] p. 85. See cardval2 3661 for a simpler version of its value.
⊢ (card ‘A) = ∩{x ∈ On∣x ≈ A}
Theorem	cardon 3634	The cardinal number of a set is an ordinal number. Proposition 10.6(1) of [TakeutiZaring] p. 85. Unlike Takeuti/Zaring's proposition, we need the Axiom of Choice (in cardval 3633) because of our slightly different definition of of cardinal number.
⊢ (card ‘A) ∈ On
Theorem	cardid 3635	Any set is equinumerous to its cardinal number. Proposition 10.5 of [TakeutiZaring] p. 85.
⊢ (card ‘A) ≈ A
Theorem	oncard 3636	A set is a cardinal number iff it equals its own cardinal number. Proposition 10.9 of [TakeutiZaring] p. 85.
⊢ (∃x A = (card ‘x) ↔ A = (card ‘A))
Theorem	cardne 3637	No member of a cardinal number of a set is equinumerous to the set. Proposition 10.6(2) of [TakeutiZaring] p. 85.
⊢ (A ∈ (card ‘B) → ¬ A ≈ B)
Theorem	carden 3638	Two sets are equinumerous iff their cardinal numbers are equal. This important theorem expresses the essential concept behind "cardinality" or "size". This theorem appears as Proposition 10.10 of [TakeutiZaring] p. 85, Theorem 7P of [Enderton] p. 197, and Theorem 9 of [Suppes] p. 242 (among others). The Axiom of Choice is required for its proof. The theory of cardinality can also be developed without AC by introducing "card" as a primitive notion and stating this theorem as an axiom, as is done with the axiom for cardinal numbers in [Suppes] p. 111. Finally, if we allow the Axiom of Regularity, we can avoid AC by defining the cardinal number of a set as the set of all sets equinumerous to it and having least possible rank (see karden 3551).
⊢ ((A ∈ C ∧ B ∈ D) → ((card ‘A) = (card ‘B) ↔ A ≈ B))
Theorem	cardeq0 3639	Only the empty set has cardinality zero.
⊢ (A ∈ B → ((card ‘A) = ∅ ↔ A = ∅))
Theorem	cardsn 3640	A singleton has cardinality one.
⊢ (A ∈ B → (card ‘{A}) = 1o)
Theorem	carddomi 3641	Two sets have the dominance relationship if their cardinalities have the subset relationship.
⊢ (A ∈ C → ((card ‘A) ⊆ (card ‘B) → A ≼ B))
Theorem	carddom 3642	Two sets have the dominance relationship iff their cardinalities have the subset relationship. Equation (i) of [Quine] p. 232.
⊢ ((A ∈ C ∧ B ∈ D) → ((card ‘A) ⊆ (card ‘B) ↔ A ≼ B))
Theorem	cardsdom 3643	Two sets have the strict dominance relationship iff their cardinalities have the membership relationship. Corollary 19.7(2) of [Eisenberg] p. 310.
⊢ ((A ∈ C ∧ B ∈ D) → ((card ‘A) ∈ (card ‘B) ↔ A ≺ B))
Theorem	domtri 3644	Trichotomy law for dominance and strict dominance. This theorem is equivalent to the Axiom of Choice.
⊢ ((A ∈ C ∧ B ∈ D) → (A ≼ B ↔ ¬ B ≺ A))
Theorem	entri 3645	Trichotomy of equinumerosity and strict dominance. This theorem is equivalent to the Axiom of Choice. Theorem 8 of [Suppes] p. 242.
⊢ ((A ∈ C ∧ B ∈ D) → (A ≺ B ∨ A ≈ B ∨ B ≺ A))
Theorem	entri2 3646	Trichotomy of dominance and strict dominance.
⊢ ((A ∈ C ∧ B ∈ D) → (A ≼ B ∨ B ≺ A))
Theorem	entri3 3647	Trichotomy of dominance. This theorem is equivalent to the Axiom of Choice. Part of Proposition 4.42(d) of [Mendelson] p. 275.
⊢ ((A ∈ C ∧ B ∈ D) → (A ≼ B ∨ B ≼ A))
Theorem	sucdom 3648	Strict dominance of a set over a natural number is the same as dominance over its successor. The proof uses AC and Infinity. It is unclear if a proof without using these is possible, unlike the weaker versions omsucdom 3418, sucdomi 3419, and finsucdom 3421.
⊢ ((A ∈ ω ∧ B ∈ C) → (A ≺ B ↔ suc A ≼ B))
Theorem	unxpdomlem 3649	Lemma for unxpdom 3650.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ((1o ≺ A ∧ 1o ≺ B) → (A ∪ B) ≼ (A × B))
Theorem	unxpdom 3650	Cross product dominates union for sets with cardinality greater than 1. Proposition 10.36 of [TakeutiZaring] p. 93.
⊢ ((1o ≺ A ∧ 1o ≺ B) → (A ∪ B) ≼ (A × B))
Theorem	unxpdom2 3651	Corollary of unxpdom 3650.
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ ((1o ≺ A ∧ B ≼ A) → (A ∪ B) ≼ (A × A))
Theorem	sucxpdom 3652	Cross product dominates successor for set with cardinality greater than 1. Proposition 10.38 of [TakeutiZaring] p. 93 (but generalized to arbitrary sets, not just ordinals, with a proof using AC).
⊢ (1o ≺ A → suc A ≼ (A × A))
Theorem	sdomel 3653	Strict dominance implies ordinal membership.
⊢ ((A ∈ On ∧ B ∈ On) → (A ≺ B → A ∈ B))
Theorem	sdomsdomcard 3654	A set strictly dominates iff its cardinal strictly dominates.
⊢ (A ≺ B ↔ A ≺ (card ‘B))
Theorem	cardcard 3655	The cardinality of the cardinality of a set equals the cardinality of the set. Proposition 10.11 of [TakeutiZaring] p. 85.
⊢ (card ‘(card ‘A)) = (card ‘A)
Theorem	canth3 3656	Cantor's theorem in terms of cardinals. This theorem tells us that no matter how large a cardinal number is, there is a still larger cardinal number. Theorem 18.12 of [Monk1] p. 133.
⊢ (A ∈ B → (card ‘A) ∈ (card ‘℘A))
Theorem	cardlim 3657	An infinite cardinal is a limit ordinal. Equivalent to Exercise 4 of [TakeutiZaring] p. 91.
⊢ (ω ⊆ (card ‘A) ↔ Lim (card ‘A))
Theorem	cardsdomel 3658	A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93 (use cardsdom 3643 to obtain the exact proposition from this one).
⊢ (A ∈ On → (A ≺ B ↔ A ∈ (card ‘B)))
Theorem	iscard 3659	Two ways to express the property of being a cardinal number.
⊢ ((card ‘A) = A ↔ (A ∈ On ∧ ∀x ∈ A x ≺ A))
Theorem	iscard2 3660	Two ways to express the property of being a cardinal number. Definition 8 of [Suppes] p. 225.
⊢ ((card ‘A) = A ↔ (A ∈ On ∧ ∀x ∈ On (A ≈ x → A ⊆ x)))
Theorem	cardval2 3661	An alternate version of the value of the cardinal number of a set. Compare cardval 3633. This theorem could be used to give us a simpler definition of card in place of df-card 3623. It apparently does not occur in the literature.
⊢ (card ‘A) = {x ∈ On∣x ≺ A}
Theorem	ondomon 3662	The collection of ordinal numbers dominated by a set is an ordinal number. (In general, not all collections of ordinal numbers are ordinal.) Theorem 56 of [Suppes] p. 227.
⊢ (A ∈ B → {x ∈ On∣x ≼ A} ∈ On)
Theorem	ondomcard 3663	The class of ordinal numbers dominated by a set is a cardinal number. Theorem 59 of [Suppes] p. 228.
⊢ (A ∈ B → (card ‘{x ∈ On∣x ≼ A}) = {x ∈ On∣x ≼ A})
Theorem	carduni 3664	The union of a set of cardinals is a cardinal. Theorem 18.14 of [Monk1] p. 133.
⊢ (A ∈ B → (∀x ∈ A (card ‘x) = x → (card ‘∪A) = ∪A))
Theorem	cardiun 3665	The indexed union of a set of cardinals is a cardinal.
⊢ (A ∈ C → (∀x ∈ A (card ‘B) = B → (card ‘∪x ∈ A B) = ∪x ∈ A B))
Theorem	cardmin 3666	The smallest ordinal that strictly dominates a set is a cardinal.
⊢ (A ∈ B → (card ‘∩{x ∈ On∣A ≺ x}) = ∩{x ∈ On∣A ≺ x})
Theorem	cardprc 3667	The class of all cardinal numbers is not a set (i.e. is a proper class). Theorem 19.8 of [Eisenberg] p. 310.
⊢ ¬ {x∣(card ‘x) = x} ∈ V
Theorem	alephfnon 3668	The aleph function is a function on the class of ordinal numbers.
⊢ ℵ Fn On
Theorem	aleph0 3669	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 Kuratowski and Mostowski, Set Theory, 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."
⊢ (ℵ ‘∅) = ω
Theorem	alephlim 3670	Value of the aleph function at a limit ordinal. Definition 12(iii) of [Suppes] p. 91.
⊢ ((A ∈ B ∧ Lim A) → (ℵ ‘A) = ∪x ∈ A (ℵ ‘x))
Theorem	alephon 3671	An aleph is an ordinal number.
⊢ (ℵ ‘A) ∈ On
Theorem	alephsuc 3672	Value of the aleph function at a successor ordinal. Definition 12(ii) of [Suppes] p. 91.
⊢ (A ∈ On → (ℵ ‘suc A) = ∩{x ∈ On∣(ℵ ‘A) ≺ x})
Theorem	alephcard 3673	Every aleph is a cardinal number. Theorem 65 of [Suppes] p. 229.
⊢ (card ‘(ℵ ‘A)) = (ℵ ‘A)
Theorem	alephnbtwn 3674	No cardinal can be sandwiched between an aleph and its successor aleph. Theorem 67 of [Suppes] p. 229.
⊢ ((card ‘B) = B → ¬ ((ℵ ‘A) ∈ B ∧ B ∈ (ℵ ‘suc A)))
Theorem	alephnbtwn2 3675	No set has equinumerosity between an aleph and its successor aleph.
⊢ ¬ ((ℵ ‘A) ≺ B ∧ B ≺ (ℵ ‘suc A))
Theorem	aleph1 3676	The set exponentiation of 2 to the aleph-zero has cardinality of at least aleph-one. (If we were to assume the Continuum Hypothesis, their cardinalities would be the same.)
⊢ (ℵ ‘1o) ≼ (2o ↑m (ℵ ‘∅))
Theorem	alephordlem1 3677	Lemma for alephordi 3679.
⊢ (A ∈ On → (ℵ ‘A) ≺ (ℵ ‘suc A))
Theorem	alephordlem2 3678	Lemma for alephordi 3679.
⊢ ((B ∈ V ∧ Lim B) → (A ∈ B → (ℵ ‘A) ≼ (ℵ ‘B)))
Theorem	alephordi 3679	Strict ordering property of the aleph function.
⊢ (B ∈ On → (A ∈ B → (ℵ ‘A) ≺ (ℵ ‘B)))
Theorem	alephord 3680	Ordering property of the aleph function.
⊢ ((A ∈ On ∧ B ∈ On) → (A ∈ B ↔ (ℵ ‘A) ≺ (ℵ ‘B)))
Theorem	alephord2 3681	Ordering property of the aleph function. Theorem 8A(a) of [Enderton] p. 213 and its converse.
⊢ ((A ∈ On ∧ B ∈ On) → (A ∈ B ↔ (ℵ ‘A) ∈ (ℵ ‘B)))
Theorem	alephord2i 3682	Ordering property of the aleph function. Theorem 66 of [Suppes] p. 229.
⊢ (B ∈ On → (A ∈ B → (ℵ ‘A) ∈ (ℵ ‘B)))
Theorem	alephord3 3683	Ordering property of the aleph function.
⊢ ((A ∈ On ∧ B ∈ On) → (A ⊆ B ↔ (ℵ ‘A) ⊆ (ℵ ‘B)))
Theorem	aleph11 3684	The aleph function is one-to-one.
⊢ ((A ∈ On ∧ B ∈ On) → ((ℵ ‘A) = (ℵ ‘B) ↔ A = B))
Theorem	alephsucdom 3685	A set dominated by an aleph is strictly dominated by its successor aleph and vice-versa.
⊢ (B ∈ On → (A ≼ (ℵ ‘B) ↔ A ≺ (ℵ ‘suc B)))
Theorem	alephsuc2 3686	An alternate representation of a successor aleph. Using this theorem we could define the aleph function with {z ∈ On∣z ≼ x} in place of ∩{z ∈ On∣x ≺ z} in df-aleph 3624.
⊢ (A ∈ On → (ℵ ‘suc A) = {x ∈ On∣x ≼ (ℵ ‘A)})
Theorem	alephgeom 3687	Every aleph is greater than or equal to the set of natural numbers.
⊢ (A ∈ On ↔ ω ⊆ (ℵ ‘A))
Theorem	alephislim 3688	Every aleph is a limit ordinal.
⊢ (A ∈ On ↔ Lim (ℵ ‘A))
Theorem	alephle 3689	The argument of the aleph function is less than or equal to its value. Exercise 2 of [TakeutiZaring] p. 91. (Later, in alephfp2 (future), we will that equality can sometimes hold.)
⊢ (A ∈ On → A ⊆ (ℵ ‘A))
Theorem	cardaleph 3690	Given any transfinite cardinal number A, there is exactly one aleph that is equal to it. Here we compute that aleph explicitly.
⊢ ((ω ⊆ A ∧ (card ‘A) = A) → A = (ℵ ‘∩{x ∈ On∣A ⊆ (ℵ ‘x)}))
Theorem	cardalephex 3691	Every transfinite cardinal is an aleph and vice-versa. Theorem 8A(b) of [Enderton] p. 213 and its converse.
⊢ (ω ⊆ A → ((card ‘A) = A ↔ ∃x ∈ On A = (ℵ ‘x)))
Theorem	isinfcard 3692	Two ways of expressing the property of being a transfinite cardinal.
⊢ ((ω ⊆ A ∧ (card ‘A) = A) ↔ A ∈ ran ℵ)
Theorem	iscard3 3693	Two ways of expressing the property of being a cardinal number.
⊢ ((card ‘A) = A ↔ A ∈ (ω ∪ ran ℵ))
Theorem	cardnum 3694	Two ways of expressing the class of all cardinal numbers, which consists of the finite ordinals in ω plus the transfinite alephs.
⊢ {x∣(card ‘x) = x} = (ω ∪ ran ℵ)
Theorem	carduniima 3695	The union of the image of a mapping to cardinals is a cardinal. Proposition 11.16 of [TakeutiZaring] p. 104.
⊢ (A ∈ B → (F:A–→(ω ∪ ran ℵ) → ∪(F “ A) ∈ (ω ∪ ran ℵ)))
Theorem	cardinfima 3696	If a mapping to cardinals has an infinite value, then the union of its image is an infinite cardinal. Corollary 11.17 of [TakeutiZaring] p. 104.
⊢ (A ∈ B → ((F:A–→(ω ∪ ran ℵ) ∧ ∃x ∈ A (F ‘x) ∈ ran ℵ) → ∪(F “ A) ∈ ran ℵ))
Theorem	alephiso 3697	Aleph is an order isomorphism of the class of ordinal numbers onto the class of infinite cardinals. Definition 10.27 of [TakeutiZaring] p. 90.
⊢ ℵ Isom E, E (On, {x∣(ω ⊆ x ∧ (card ‘x) = x)})
Theorem	alephprc 3698	The class of all transfinite cardinal numbers (the range of the aleph function) is a proper class. Proposition 10.26 of [TakeutiZaring] p. 90.
⊢ ¬ ran ℵ ∈ V
Theorem	alephsson 3699	The class of transfinite cardinals (the range of the aleph function) is a subclass of the class of ordinal numbers.
⊢ ran ℵ ⊆ On
Theorem	cflem 3700	A lemma used to simplify cofinality computations, showing the existence of the cardinal of an unbounded subset of a set A.
⊢ (A ∈ B → ∃x∃y(x = (card ‘y) ∧ (y ⊆ A ∧ ∀z ∈ A ∃w ∈ y z ⊆ w)))