![]() |
Metamath
Proof Explorer Theorem List (p. 92 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-acn 9101* | 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 ∧ ∀𝑓 ∈ ((𝒫 𝑥 ∖ {∅}) ↑𝑚 𝐴)∃𝑔∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝑓‘𝑦))} | ||
Theorem | cardf2 9102* | 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 9103 | 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 9104* | 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 9105 | A set equinumerous to an ordinal is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ On ∧ 𝐴 ≈ 𝐵) → 𝐵 ∈ dom card) | ||
Theorem | ennum 9106 | Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ dom card ↔ 𝐵 ∈ dom card)) | ||
Theorem | finnum 9107 | Every finite set is numerable. (Contributed by Mario Carneiro, 4-Feb-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ Fin → 𝐴 ∈ dom card) | ||
Theorem | onenon 9108 | Every ordinal number is numerable. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ On → 𝐴 ∈ dom card) | ||
Theorem | tskwe 9109* | A Tarski set is well-orderable. (Contributed by Mario Carneiro, 19-Apr-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ 𝑉 ∧ {𝑥 ∈ 𝒫 𝐴 ∣ 𝑥 ≺ 𝐴} ⊆ 𝐴) → 𝐴 ∈ dom card) | ||
Theorem | xpnum 9110 | 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 9111* | 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 9112 | 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 9113 | A set is numerable iff it is equinumerous with its cardinal. (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ (𝐴 ∈ dom card ↔ (card‘𝐴) ≈ 𝐴) | ||
Theorem | oncardval 9114* | The value of the cardinal number function with an ordinal number as its argument. Unlike cardval 9703, 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 9115 | Any ordinal number is equinumerous to its cardinal number. Unlike cardid 9704, this theorem does not require the Axiom of Choice. (Contributed by NM, 26-Jul-2004.) |
⊢ (𝐴 ∈ On → (card‘𝐴) ≈ 𝐴) | ||
Theorem | cardonle 9116 | 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 9117 | The cardinality of the empty set is the empty set. (Contributed by NM, 25-Oct-2003.) |
⊢ (card‘∅) = ∅ | ||
Theorem | cardidm 9118 | The cardinality function is idempotent. Proposition 10.11 of [TakeutiZaring] p. 85. (Contributed by Mario Carneiro, 7-Jan-2013.) |
⊢ (card‘(card‘𝐴)) = (card‘𝐴) | ||
Theorem | oncard 9119* | 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 9120 | 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 9121 | A finite set is equinumerous to its cardinal number. (Contributed by Mario Carneiro, 21-Sep-2013.) |
⊢ (𝐴 ∈ Fin → (card‘𝐴) ≈ 𝐴) | ||
Theorem | cardnn 9122 | 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 9123 | The empty set is the only numerable set with cardinality zero. (Contributed by Mario Carneiro, 7-Jan-2013.) |
⊢ (𝐴 ∈ dom card → ((card‘𝐴) = ∅ ↔ 𝐴 = ∅)) | ||
Theorem | cardne 9124 | 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 9125 | If two sets have equal nonzero cardinalities, then they are equinumerous. (This assertion and carden2b 9126 are meant to replace carden 9708 in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013.) |
⊢ (((card‘𝐴) = (card‘𝐵) ∧ (card‘𝐴) ≠ ∅) → 𝐴 ≈ 𝐵) | ||
Theorem | carden2b 9126 | If two sets are equinumerous, then they have equal cardinalities. (This assertion and carden2a 9125 are meant to replace carden 9708 in ZF without AC.) (Contributed by Mario Carneiro, 9-Jan-2013.) (Proof shortened by Mario Carneiro, 27-Apr-2015.) |
⊢ (𝐴 ≈ 𝐵 → (card‘𝐴) = (card‘𝐵)) | ||
Theorem | card1 9127* | A set has cardinality one iff it is a singleton. (Contributed by Mario Carneiro, 10-Jan-2013.) |
⊢ ((card‘𝐴) = 1o ↔ ∃𝑥 𝐴 = {𝑥}) | ||
Theorem | cardsn 9128 | A singleton has cardinality one. (Contributed by Mario Carneiro, 10-Jan-2013.) |
⊢ (𝐴 ∈ 𝑉 → (card‘{𝐴}) = 1o) | ||
Theorem | carddomi2 9129 | Two sets have the dominance relationship if their cardinalities have the subset relationship and one is numerable. See also carddom 9711, which uses AC. (Contributed by Mario Carneiro, 11-Jan-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ 𝑉) → ((card‘𝐴) ⊆ (card‘𝐵) → 𝐴 ≼ 𝐵)) | ||
Theorem | sdomsdomcardi 9130 | A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013.) |
⊢ (𝐴 ≺ (card‘𝐵) → 𝐴 ≺ 𝐵) | ||
Theorem | cardlim 9131 | 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 9132 | A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of [TakeutiZaring] p. 93. This is half of the assertion cardsdomel 9133 and can be proven without the AC. (Contributed by Mario Carneiro, 15-Jan-2013.) |
⊢ (𝐴 ∈ (card‘𝐵) → 𝐴 ≺ 𝐵) | ||
Theorem | cardsdomel 9133 | 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 9134* | Two ways to express the property of being a cardinal number. (Contributed by Mario Carneiro, 15-Jan-2013.) |
⊢ ((card‘𝐴) = 𝐴 ↔ (𝐴 ∈ On ∧ ∀𝑥 ∈ 𝐴 𝑥 ≺ 𝐴)) | ||
Theorem | iscard2 9135* | 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 9136 | Two numerable sets have the dominance relationship iff their cardinalities have the subset relationship. See also carddom 9711, 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 9137 | 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 9138* | Lemma for cardprc 9139. (Contributed by Mario Carneiro, 22-Jan-2013.) (Revised by Mario Carneiro, 15-May-2015.) |
⊢ 𝐴 = {𝑥 ∣ (card‘𝑥) = 𝑥} ⇒ ⊢ ¬ 𝐴 ∈ V | ||
Theorem | cardprc 9139 | 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 9718 to ensure that there is always a cardinal larger than a given cardinal, but we can use Hartogs' construction hartogs 8738 to construct (effectively) (ℵ‘suc 𝐴) from (ℵ‘𝐴), which achieves the same thing. (Contributed by Mario Carneiro, 22-Jan-2013.) |
⊢ {𝑥 ∣ (card‘𝑥) = 𝑥} ∉ V | ||
Theorem | carduni 9140* | 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 9141* | The indexed union of a set of cardinals is a cardinal. (Contributed by NM, 3-Nov-2003.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥 ∈ 𝐴 (card‘𝐵) = 𝐵 → (card‘∪ 𝑥 ∈ 𝐴 𝐵) = ∪ 𝑥 ∈ 𝐴 𝐵)) | ||
Theorem | cardennn 9142 | If 𝐴 is equinumerous to a natural number, then that number is its cardinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
⊢ ((𝐴 ≈ 𝐵 ∧ 𝐵 ∈ ω) → (card‘𝐴) = 𝐵) | ||
Theorem | cardsucinf 9143 | The cardinality of the successor of an infinite ordinal. (Contributed by Mario Carneiro, 11-Jan-2013.) |
⊢ ((𝐴 ∈ On ∧ ω ⊆ 𝐴) → (card‘suc 𝐴) = (card‘𝐴)) | ||
Theorem | cardsucnn 9144 | The cardinality of the successor of a finite ordinal (natural number). This theorem does not hold for infinite ordinals; see cardsucinf 9143. (Contributed by NM, 7-Nov-2008.) |
⊢ (𝐴 ∈ ω → (card‘suc 𝐴) = suc (card‘𝐴)) | ||
Theorem | cardom 9145 | 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 9146 | Two numerable sets are equinumerous iff their cardinal numbers are equal. Unlike carden 9708, the Axiom of Choice is not required. (Contributed by Mario Carneiro, 22-Sep-2013.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → ((card‘𝐴) = (card‘𝐵) ↔ 𝐴 ≈ 𝐵)) | ||
Theorem | cardsdom2 9147 | 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 9148 | Trichotomy of dominance for numerable sets (does not use AC). (Contributed by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ∈ dom card) → (𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴)) | ||
Theorem | nnsdomel 9149 | Strict dominance and elementhood are the same for finite ordinals. (Contributed by Stefan O'Rear, 2-Nov-2014.) |
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ 𝐴 ≺ 𝐵)) | ||
Theorem | cardval2 9150* | An alternate version of the value of the cardinal number of a set. Compare cardval 9703. This theorem could be used to give a simpler definition of card in place of df-card 9098. It apparently does not occur in the literature. (Contributed by NM, 7-Nov-2003.) |
⊢ (𝐴 ∈ dom card → (card‘𝐴) = {𝑥 ∈ On ∣ 𝑥 ≺ 𝐴}) | ||
Theorem | isinffi 9151* | An infinite set contains subsets equinumerous to every finite set. Extension of isinf 8461 from finite ordinals to all finite sets. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
⊢ ((¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin) → ∃𝑓 𝑓:𝐵–1-1→𝐴) | ||
Theorem | fidomtri 9152 | 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 9153 | 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 9154 | The Hartogs number of a well-orderable set strictly dominates the set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ dom card → 𝐴 ≺ (har‘𝐴)) | ||
Theorem | onsdom 9155* | 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 9156* | An alternate expression for the Hartogs number of a well-orderable set. (Contributed by Mario Carneiro, 15-May-2015.) |
⊢ (𝐴 ∈ dom card → (har‘𝐴) = ∩ {𝑥 ∈ On ∣ 𝐴 ≺ 𝑥}) | ||
Theorem | cardmin2 9157* | 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 9158* | 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 9127), 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 9159. (Contributed by NM, 4-Nov-2013.) |
⊢ (𝐴 ≈ 1o ↔ 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o}) | ||
Theorem | pm54.43 9159 |
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 9127), so that their 𝐴 ∈ 1 means, in our notation, 𝐴 ∈ {𝑥 ∣ (card‘𝑥) = 1o} which is the same as 𝐴 ≈ 1o by pm54.43lem 9158. 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 pm110.643 9334 shows the derivation of 1+1=2 for cardinal numbers from this theorem. (Contributed by NM, 4-Apr-2007.) |
⊢ ((𝐴 ≈ 1o ∧ 𝐵 ≈ 1o) → ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐴 ∪ 𝐵) ≈ 2o)) | ||
Theorem | pr2nelem 9160 | Lemma for pr2ne 9161. (Contributed by FL, 17-Aug-2008.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ∧ 𝐴 ≠ 𝐵) → {𝐴, 𝐵} ≈ 2o) | ||
Theorem | pr2ne 9161 | If an unordered pair has two elements they are different. (Contributed by FL, 14-Feb-2010.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ({𝐴, 𝐵} ≈ 2o ↔ 𝐴 ≠ 𝐵)) | ||
Theorem | prdom2 9162 | An unordered pair has at most two elements. (Contributed by FL, 22-Feb-2011.) |
⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → {𝐴, 𝐵} ≼ 2o) | ||
Theorem | en2eqpr 9163 | Building a set with two elements. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.) |
⊢ ((𝐶 ≈ 2o ∧ 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → (𝐴 ≠ 𝐵 → 𝐶 = {𝐴, 𝐵})) | ||
Theorem | en2eleq 9164 | 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 9165 | 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 9166 | 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 9167* | Lexicographical order is a well-ordering of On × On. Proposition 7.56(1) of [TakeutiZaring] p. 54. Note that unlike r0weon 9168, 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 9168* | 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 9169* | Lemma for infxpen 9170. (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 9170 | 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 9171 | 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 9172 | The cartesian product of two countable sets is countable. (Contributed by Thierry Arnoux, 24-Sep-2017.) |
⊢ ((𝐴 ≼ ω ∧ 𝐵 ≼ ω) → (𝐴 × 𝐵) ≼ ω) | ||
Theorem | infxpidm2 9173 | The Cartesian product of an infinite set with itself is idempotent. This theorem provides the basis for infinite cardinal arithmetic. Proposition 10.40 of [TakeutiZaring] p. 95. See also infxpidm 9719. (Contributed by Mario Carneiro, 9-Mar-2013.) (Revised by Mario Carneiro, 29-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ ω ≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) | ||
Theorem | infxpenc 9174* | A canonical version of infxpen 9170, by a completely different approach (although it uses infxpen 9170 via xpomen 9171). Using Cantor's normal form, we can show that 𝐴 ↑o 𝐵 respects equinumerosity (oef1o 8892), 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 8900.) (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) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) & ⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑o 2o) CNF 𝑊)) & ⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚 (𝑊 ·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 9175* | Lemma for infxpenc2 9178. (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 9176* | Lemma for infxpenc2 9178. (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) ↑𝑚 𝑊) ∣ 𝑥 finSupp ∅} ↦ (𝐹 ∘ (𝑦 ∘ ◡( I ↾ 𝑊)))) & ⊢ 𝐻 = (((ω CNF 𝑊) ∘ 𝐾) ∘ ◡((ω ↑o 2o) CNF 𝑊)) & ⊢ 𝐿 = (𝑦 ∈ {𝑥 ∈ (ω ↑𝑚 (𝑊 ·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 9177* | Lemma for infxpenc2 9178. (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 9178* | Existence form of infxpenc 9174. A "uniform" or "canonical" version of infxpen 9170, 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 9179* | The union ∪ 𝑛 ∈ 𝐶(𝐴 ↑𝑚 𝑛) is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.) |
⊢ ∃*𝑛 ∈ 𝐶 𝐵 ∈ (𝐴 ↑𝑚 𝑛) | ||
Theorem | fseqenlem1 9180* | Lemma for fseqen 9183. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) & ⊢ 𝐺 = seq𝜔((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ ω) → (𝐺‘𝐶):(𝐴 ↑𝑚 𝐶)–1-1→𝐴) | ||
Theorem | fseqenlem2 9181* | Lemma for fseqen 9183. (Contributed by Mario Carneiro, 17-May-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:(𝐴 × 𝐴)–1-1-onto→𝐴) & ⊢ 𝐺 = seq𝜔((𝑛 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (𝐴 ↑𝑚 suc 𝑛) ↦ ((𝑓‘(𝑥 ↾ 𝑛))𝐹(𝑥‘𝑛)))), {〈∅, 𝐵〉}) & ⊢ 𝐾 = (𝑦 ∈ ∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘) ↦ 〈dom 𝑦, ((𝐺‘dom 𝑦)‘𝑦)〉) ⇒ ⊢ (𝜑 → 𝐾:∪ 𝑘 ∈ ω (𝐴 ↑𝑚 𝑘)–1-1→(ω × 𝐴)) | ||
Theorem | fseqdom 9182* | One half of fseqen 9183. (Contributed by Mario Carneiro, 18-Nov-2014.) |
⊢ (𝐴 ∈ 𝑉 → (ω × 𝐴) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) | ||
Theorem | fseqen 9183* | 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.) |
⊢ (((𝐴 × 𝐴) ≈ 𝐴 ∧ 𝐴 ≠ ∅) → ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ≈ (ω × 𝐴)) | ||
Theorem | infpwfidom 9184 | 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 9185* | Lemma for dfac8a 9186. 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 9186* | 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 9187* | 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 9188* | Lemma for dfac8c 9189. (Contributed by Mario Carneiro, 10-Jan-2013.) |
⊢ 𝐹 = (𝑠 ∈ (𝐴 ∖ {∅}) ↦ (℩𝑎 ∈ 𝑠 ∀𝑏 ∈ 𝑠 ¬ 𝑏𝑟𝑎)) ⇒ ⊢ (𝐴 ∈ 𝐵 → (∃𝑟 𝑟 We ∪ 𝐴 → ∃𝑓∀𝑧 ∈ 𝐴 (𝑧 ≠ ∅ → (𝑓‘𝑧) ∈ 𝑧))) | ||
Theorem | dfac8c 9189* | 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 9190* | A proof of the well-ordering theorem weth 9652, 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 9191* | A set is numerable iff it can be well-ordered. (Contributed by Mario Carneiro, 5-Jan-2013.) |
⊢ (𝐴 ∈ dom card ↔ ∃𝑟 𝑟 We 𝐴) | ||
Theorem | ac5num 9192* | A version of ac5b 9635 with the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015.) |
⊢ ((∪ 𝐴 ∈ dom card ∧ ¬ ∅ ∈ 𝐴) → ∃𝑓(𝑓:𝐴⟶∪ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑓‘𝑥) ∈ 𝑥)) | ||
Theorem | ondomen 9193 | If a set is dominated by an ordinal, then it is numerable. (Contributed by Mario Carneiro, 5-Jan-2013.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | numdom 9194 | A set dominated by a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | ssnum 9195 | A subset of a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015.) |
⊢ ((𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴) → 𝐵 ∈ dom card) | ||
Theorem | onssnum 9196 | All subsets of the ordinals are numerable. (Contributed by Mario Carneiro, 12-Feb-2013.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐴 ⊆ On) → 𝐴 ∈ dom card) | ||
Theorem | indcardi 9197* | Indirect strong induction on the cardinality of a finite or numerable set. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑇 ∈ dom card) & ⊢ ((𝜑 ∧ 𝑅 ≼ 𝑇 ∧ ∀𝑦(𝑆 ≺ 𝑅 → 𝜒)) → 𝜓) & ⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 𝑦 → 𝑅 = 𝑆) & ⊢ (𝑥 = 𝐴 → 𝑅 = 𝑇) ⇒ ⊢ (𝜑 → 𝜃) | ||
Theorem | acnrcl 9198 | Reverse closure for the choice set predicate. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝑋 ∈ AC 𝐴 → 𝐴 ∈ V) | ||
Theorem | acneq 9199 | Equality theorem for the choice set function. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ (𝐴 = 𝐶 → AC 𝐴 = AC 𝐶) | ||
Theorem | isacn 9200* | The property of being a choice set of length 𝐴. (Contributed by Mario Carneiro, 31-Aug-2015.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑋 ∈ AC 𝐴 ↔ ∀𝑓 ∈ ((𝒫 𝑋 ∖ {∅}) ↑𝑚 𝐴)∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |