HomeHome New Foundations Explorer
Theorem List (p. 63 of 64)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  NFE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for New Foundations Explorer - 6201-6300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremncpw1pwneg 6201 The cardinality of a unit power class is not equal to the cardinality of the power class. Theorem XI.2.4 of [Rosser] p. 372. (Contributed by SF, 10-Mar-2015.)
(A VNc 1ANc A)
 
Theoremltcpw1pwg 6202 The cardinality of a unit power class is strictly less than the cardinality of the power class. Theorem XI.2.17 of [Rosser] p. 376. (Contributed by SF, 10-Mar-2015.)
(A VNc 1A <c Nc A)
 
Theoremsbthlem1 6203 Lemma for sbth 6206. Set up similarity with a range. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 11-Mar-2015.)
R V    &   X V    &   G = Clos1 ((X ran R), R)    &   A = (XG)    &   B = (X G)    &   C = (ran RG)    &   D = (ran R G)       (((Fun R Fun R) (X dom R ran R X)) → ran RX)
 
Theoremsbthlem2 6204 Lemma for sbth 6206. Eliminate hypotheses from sbthlem1 6203. Theorem XI.1.14 of [Rosser] p. 350. (Contributed by SF, 10-Mar-2015.)
R V       (((Fun R Fun R) (B V B dom R ran R B)) → ran RB)
 
Theoremsbthlem3 6205 Lemma for sbth 6206. If A is equinumerous with a subset of B and vice-versa, then A is equinumerous with B. Theorem XI.1.15 of [Rosser] p. 353. (Contributed by SF, 10-Mar-2015.)
(((AC C B) (BD D A)) → AB)
 
Theoremsbth 6206 The Schroder-Bernstein Theorem. This theorem gives the antisymmetry law for cardinal less than or equal. Translated out, it means that, if A is no larger than B and B is no larger than A, then Nc A = Nc B. Theorem XI.2.20 of [Rosser] p. 376. (Contributed by SF, 11-Mar-2015.)
((A NC B NC ) → ((Ac B Bc A) → A = B))
 
Theoremltlenlec 6207 Cardinal less than is equivalent to one-way cardinal less than or equal. Theorem XI.2.21 of [Rosser] p. 377. (Contributed by SF, 11-Mar-2015.)
((M NC N NC ) → (M <c N ↔ (Mc N ¬ Nc M)))
 
Theoremaddlec 6208 For non-empty sets, cardinal sum always increases cardinal less than or equal. Theorem XI.2.19 of [Rosser] p. 376. (Contributed by SF, 11-Mar-2015.)
((M V N W (M +c N) ≠ ) → Mc (M +c N))
 
Theoremaddlecncs 6209 For cardinals, cardinal sum always increases cardinal less than or equal. Corollary of theorem XI.2.19 of [Rosser] p. 376. (Contributed by SF, 11-Mar-2015.)
((M NC N NC ) → Mc (M +c N))
 
Theoremdflec2 6210* Cardinal less than or equal in terms of cardinal addition. Theorem XI.2.22 of [Rosser] p. 377. (Contributed by SF, 11-Mar-2015.)
((M NC N NC ) → (Mc Np NC N = (M +c p)))
 
Theoremlectr 6211 Cardinal less than or equal is transitive. (Contributed by SF, 12-Mar-2015.)
((A NC B NC C NC ) → ((Ac B Bc C) → Ac C))
 
Theoremleltctr 6212 Transitivity law for cardinal less than or equal and less than. (Contributed by SF, 16-Mar-2015.)
((A NC B NC C NC ) → ((Ac B B <c C) → A <c C))
 
Theoremlecponc 6213 Cardinal less than or equal partially orders the cardinals. (Contributed by SF, 12-Mar-2015.)
c Po NC
 
Theoremleaddc1 6214 Addition law for cardinal less than. Theorem XI.2.23 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
(((M NC N NC P NC ) Mc N) → (M +c P) ≤c (N +c P))
 
Theoremleaddc2 6215 Addition law for cardinal less than. Theorem XI.2.23 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
(((M NC N NC P NC ) Nc P) → (M +c N) ≤c (M +c P))
 
Theoremnc0le1 6216 Any cardinal is either zero or no greater than one. Theorem XI.2.24 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
(N NC → (N = 0c 1cc N))
 
Theoremnc0suc 6217* Any cardinal is either zero or the successor of a cardinal. Corollary of theorem XI.2.24 of [Rosser] p. 377. (Contributed by SF, 12-Mar-2015.)
(N NC → (N = 0c m NC N = (m +c 1c)))
 
Theoremleconnnc 6218 Cardinal less than or equal is total over the naturals. (Contributed by SF, 12-Mar-2015.)
((A Nn B Nn ) → (Ac B Bc A))
 
Theoremaddceq0 6219 The sum of two cardinals is zero iff both addends are zero. (Contributed by SF, 12-Mar-2015.)
((A NC B NC ) → ((A +c B) = 0c ↔ (A = 0c B = 0c)))
 
Theoremce2lt 6220 Ordering law for cardinal exponentiation to two. Theorem XI.2.71 of [Rosser] p. 390. (Contributed by SF, 13-Mar-2015.)
((M NC (Mc 0c) NC ) → M <c (2cc M))
 
Theoremdflec3 6221* Another potential definition of cardinal inequality. (Contributed by SF, 23-Mar-2015.)
((M NC N NC ) → (Mc Na M b N f f:a1-1b))
 
Theoremnclenc 6222* Comparison rule for cardinalities. (Contributed by SF, 24-Mar-2015.)
A V    &   B V       ( Nc Ac Nc Bf f:A1-1B)
 
Theoremlenc 6223* Less than or equal condition for the cardinality of a number. (Contributed by SF, 18-Mar-2015.)
A V       (M NC → (Mc Nc Ax M x A))
 
Theoremtcncg 6224 Compute the T-raising of a cardinality. (Contributed by SF, 23-Apr-2021.)
(A VTc Nc A = Nc 1A)
 
Theoremtcnc 6225 Compute the T-raising of a cardinality. (Contributed by SF, 4-Mar-2015.)
A V        Tc Nc A = Nc 1A
 
Theoremtcncv 6226 Compute the T-raising of the cardinality of the universe. Part of Theorem 5.2 of [Specker] p. 973. (Contributed by SF, 4-Mar-2015.)
Tc Nc V = Nc 1c
 
Theoremtcnc1c 6227 Compute the T-raising of the cardinality of one. Part of Theorem 5.2 of [Specker] p. 973. (Contributed by SF, 4-Mar-2015.)
Tc Nc 1c = Nc 11c
 
Theoremtc11 6228 Cardinal T is one-to-one. Based on theorem 2.4 of [Specker] p. 972. (Contributed by SF, 10-Mar-2015.)
((M NC N NC ) → ( Tc M = Tc NM = N))
 
Theoremtaddc 6229* T raising rule for cardinal sum. (Contributed by SF, 11-Mar-2015.)
(((A NC B NC X NC ) Tc A = ( Tc B +c X)) → c NC X = Tc c)
 
Theoremtlecg 6230 T-raising perserves order for cardinals. Theorem 5.5 of [Specker] p. 973. (Contributed by SF, 11-Mar-2015.)
((M NC N NC ) → (Mc NTc Mc Tc N))
 
Theoremletc 6231* If a cardinal is less than or equal to a T-raising, then it is also a T-raising. Theorem 5.6 of [Specker] p. 973. (Contributed by SF, 11-Mar-2015.)
((M NC N NC Mc Tc N) → p NC M = Tc p)
 
Theoremce0t 6232* If (Mc 0c) is a cardinal, then M is a T-raising of some cardinal. (Contributed by SF, 17-Mar-2015.)
((M NC (Mc 0c) NC ) → n NC M = Tc n)
 
Theoremce2le 6233 Partial ordering law for base two cardinal exponentiation. Theorem 4.8 of [Specker] p. 973. (Contributed by SF, 16-Mar-2015.)
(((M NC N NC (Nc 0c) NC ) Mc N) → (2cc M) ≤c (2cc N))
 
Theoremcet 6234 The exponent of a T-raising to a T-raising is always a cardinal. (Contributed by SF, 13-Mar-2015.)
((M NC N NC ) → ( Tc Mc Tc N) NC )
 
Theoremce2t 6235 The exponent of two to a T-raising is always a cardinal. Theorem 5.8 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
(M NC → (2cc Tc M) NC )
 
Theoremtce2 6236 Distributive law for T-raising and cardinal exponentiation to two. (Contributed by SF, 13-Mar-2015.)
((M NC (Mc 0c) NC ) → Tc (2cc M) = (2cc Tc M))
 
Theoremte0c 6237 A T-raising raised to zero is always a cardinal. (Contributed by SF, 16-Mar-2015.)
(M NC → ( Tc Mc 0c) NC )
 
Theoremce0tb 6238* (Mc 0c) is a cardinal iff M is a T-raising of some cardinal. (Contributed by SF, 17-Mar-2015.)
(M NC → ((Mc 0c) NCn NC M = Tc n))
 
Theoremce0lenc1 6239 Cardinal exponentiation to zero is a cardinal iff the number is less than the size of cardinal one. (Contributed by SF, 18-Mar-2015.)
(M NC → ((Mc 0c) NCMc Nc 1c))
 
Theoremtlenc1c 6240 A T-raising is less than or equal to the cardinality of cardinal one. (Contributed by SF, 16-Mar-2015.)
(M NCTc Mc Nc 1c)
 
Theorem1ne0c 6241 Cardinal one is not zero. (Contributed by SF, 4-Mar-2015.)
1c ≠ 0c
 
Theorem2ne0c 6242 Cardinal two is not zero. (Contributed by SF, 4-Mar-2015.)
2c ≠ 0c
 
Theoremfinnc 6243 A set is finite iff its cardinality is a natural. (Contributed by SF, 18-Mar-2015.)
(A FinNc A Nn )
 
Theoremtcfnex 6244 The stratified T raising function is a set. (Contributed by SF, 18-Mar-2015.)
TcFn V
 
Theoremfntcfn 6245 Functionhood statement for the stratified T-raising function. (Contributed by SF, 18-Mar-2015.)
TcFn Fn 1c
 
Theorembrtcfn 6246 Binary relationship form of the stratified T-raising function. (Contributed by SF, 18-Mar-2015.)
A V       ({A}TcFnBB = Tc A)
 
Theoremncfin 6247 The cardinality of a set is a natural iff the set is finite. (Contributed by SF, 19-Mar-2015.)
A V       ( Nc A NnA Fin )
 
Theoremnclennlem1 6248* Lemma for nclenn 6249. Set up stratification for induction. (Contributed by SF, 19-Mar-2015.)
{x n NC (nc xn Nn )} V
 
Theoremnclenn 6249 A cardinal that is less than or equal to a natural is a natural. Theorem XI.3.3 of [Rosser] p. 391. (Contributed by SF, 19-Mar-2015.)
((M NC N Nn Mc N) → M Nn )
 
Theoremaddcdi 6250 Distributivity law for cardinal addition and multiplication. Theorem XI.2.31 of [Rosser] p. 379. (Contributed by Scott Fenton, 31-Jul-2019.)
((A NC B NC C NC ) → (A ·c (B +c C)) = ((A ·c B) +c (A ·c C)))
 
Theoremaddcdir 6251 Distributivity law for cardinal addition and multiplication. Theorem XI.2.30 of [Rosser] p. 379. (Contributed by Scott Fenton, 31-Jul-2019.)
((A NC B NC C NC ) → ((A +c B) ·c C) = ((A ·c C) +c (B ·c C)))
 
Theoremmuc0or 6252 The cardinal product of two cardinal numbers is zero iff one of the numbers is zero. Biconditional form of theorem XI.2.34 of [Rosser] p. 380. (Contributed by Scott Fenton, 31-Jul-2019.)
((A NC B NC ) → ((A ·c B) = 0c ↔ (A = 0c B = 0c)))
 
Theoremlemuc1 6253 Multiplication law for cardinal less than. Theorem XI.2.35 of [Rosser] p. 380. (Contributed by Scott Fenton, 31-Jul-2019.)
(((A NC B NC C NC ) Ac B) → (A ·c C) ≤c (B ·c C))
 
Theoremlemuc2 6254 Multiplication law for cardinal less than. (Contributed by Scott Fenton, 31-Jul-2019.)
(((A NC B NC C NC ) Bc C) → (A ·c B) ≤c (A ·c C))
 
Theoremncslemuc 6255 A cardinal is less than or equal to its product with another. Theorem XI.2.36 of [Rosser] p. 381. (Contributed by Scott Fenton, 31-Jul-2019.)
((M NC N NC N ≠ 0c) → Mc (M ·c N))
 
Theoremncvsq 6256 The product of the cardinality of V squared is just the cardinality of V. Theorem XI.2.37 of [Rosser] p. 381. (Contributed by Scott Fenton, 31-Jul-2019.)
( Nc V ·c Nc V) = Nc V
 
Theoremvvsqenvv 6257 There are exactly as many ordered pairs as there are sets. Corollary to theorem XI.2.37 of [Rosser] p. 381. (Contributed by Scott Fenton, 31-Jul-2019.)
(V × V) ≈ V
 
Theorem0lt1c 6258 Cardinal one is strictly greater than cardinal zero. (Contributed by Scott Fenton, 1-Aug-2019.)
0c <c 1c
 
Theoremcsucex 6259 The function mapping x to its cardinal successor exists. (Contributed by Scott Fenton, 30-Jul-2019.)
(x V (x +c 1c)) V
 
Theorembrcsuc 6260* Binary relationship form of the successor mapping function. (Contributed by Scott Fenton, 2-Aug-2019.)
A V    &   B V       (A(x V (x +c 1c))BB = (A +c 1c))
 
Theoremnnltp1clem1 6261 Lemma for nnltp1c 6262. Set up stratification. (Contributed by SF, 25-Mar-2015.)
{x x <c (x +c 1c)} V
 
Theoremnnltp1c 6262 Any natural is less than one plus itself. (Contributed by SF, 25-Mar-2015.)
(N NnN <c (N +c 1c))
 
Theoremaddccan2nclem1 6263* Lemma for addccan2nc 6265. Stratification helper theorem. (Contributed by Scott Fenton, 2-Aug-2019.)
(x( AddC (1st (V × {n})))yy = (x +c n))
 
Theoremaddccan2nclem2 6264* Lemma for addccan2nc 6265. Establish stratification for induction. (Contributed by Scott Fenton, 2-Aug-2019.)
((N V P W) → {x ((x +c N) = (x +c P) → N = P)} V)
 
Theoremaddccan2nc 6265 Cancellation law for addition over the cardinal numbers. Biconditional form of theorem XI.3.2 of [Rosser] p. 391. (Contributed by Scott Fenton, 2-Aug-2019.)
((M Nn N NC P NC ) → ((M +c N) = (M +c P) ↔ N = P))
 
Theoremlecadd2 6266 Cardinal addition preserves cardinal less than. Biconditional form of corollary 4 of theorem XI.3.2 of [Rosser] p. 391. (Contributed by Scott Fenton, 2-Aug-2019.)
((M Nn N NC P NC ) → ((M +c N) ≤c (M +c P) ↔ Nc P))
 
Theoremncslesuc 6267 Relationship between successor and cardinal less than or equal. (Contributed by Scott Fenton, 3-Aug-2019.)
((M NC N NC ) → (Mc (N +c 1c) ↔ (Mc N M = (N +c 1c))))
 
Theoremnmembers1lem1 6268* Lemma for nmembers1 6271. Set up stratification. (Contributed by SF, 25-Mar-2015.)
{x {m Nn (1cc m mc x)} Tc Tc x} V
 
Theoremnmembers1lem2 6269 Lemma for nmembers1 6271. The set of all elements between one and zero is empty. (Contributed by Scott Fenton, 1-Aug-2019.)
{m Nn (1cc m mc 0c)} 0c
 
Theoremnmembers1lem3 6270* Lemma for nmembers1 6271. If the interval from one to a natural is in a given natural, extending it by one puts it in the next natural. (Contributed by Scott Fenton, 3-Aug-2019.)
((A Nn B Nn ) → ({m Nn (1cc m mc A)} B → {m Nn (1cc m mc (A +c 1c))} (B +c 1c)))
 
Theoremnmembers1 6271* Count the number of elements in a natural interval. From nmembers1lem2 6269 and nmembers1lem3 6270, we would expect to arrive at {m Nn (1cc m mc N)} N, but this proposition is not stratifiable. Instead, we arrive at the weaker conclusion below. We can arrive at the earlier proposition once we add the Axiom of Counting, which we will do later. (Contributed by Scott Fenton, 3-Aug-2019.)
(N Nn → {m Nn (1cc m mc N)} Tc Tc N)
 
2.4.6  Specker's disproof of the axiom of choice
 
Syntaxcspac 6272 Extend the definition of a class to include the special set generator for the axiom of choice.
class Spac
 
Definitiondf-spac 6273* Define the special class generator for the disproof of the axiom of choice. Definition 6.1 of [Specker] p. 973. (Contributed by SF, 3-Mar-2015.)
Spac = (m NC Clos1 ({m}, {x, y (x NC y NC y = (2cc x))}))
 
Theoremnncdiv3lem1 6274 Lemma for nncdiv3 6276. Set up a helper for stratification. (Contributed by SF, 3-Mar-2015.)
(n, b ran ( Ins3 ((ran (1st ⊗ (1st ∩ 2nd )) ⊗ 2nd ) “ AddC ) ∩ (((1st 1st ) ⊗ ((2nd 1st ) ⊗ 2nd )) “ AddC )) ↔ b = ((n +c n) +c n))
 
Theoremnncdiv3lem2 6275* Lemma for nncdiv3 6276. Set up stratification for induction. (Contributed by SF, 2-Mar-2015.)
{a n Nn (a = ((n +c n) +c n) a = (((n +c n) +c n) +c 1c) a = (((n +c n) +c n) +c 2c))} V
 
Theoremnncdiv3 6276* Divisibility by three rule for finite cardinals. Part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 2-Mar-2015.)
(A Nnn Nn (A = ((n +c n) +c n) A = (((n +c n) +c n) +c 1c) A = (((n +c n) +c n) +c 2c)))
 
Theoremnnc3n3p1 6277 Three times a natural is not one more than three times a natural. Another part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
((A Nn B Nn ) → ¬ ((A +c A) +c A) = (((B +c B) +c B) +c 1c))
 
Theoremnnc3n3p2 6278 Three times a natural is not two more than three times a natural. Another part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 12-Mar-2015.)
((A Nn B Nn ) → ¬ ((A +c A) +c A) = (((B +c B) +c B) +c 2c))
 
Theoremnnc3p1n3p2 6279 One more than three times a natural is not two more than three times a natural. Final part of Theorem 3.4 of [Specker] p. 973. (Contributed by SF, 12-Mar-2015.)
((A Nn B Nn ) → ¬ (((A +c A) +c A) +c 1c) = (((B +c B) +c B) +c 2c))
 
Theoremspacvallem1 6280* Lemma for spacval 6281. Set up stratification for the recursive relationship. (Contributed by SF, 6-Mar-2015.)
{x, y (x NC y NC y = (2cc x))} V
 
Theoremspacval 6281* The value of the special set generator. (Contributed by SF, 4-Mar-2015.)
(N NC → ( SpacN) = Clos1 ({N}, {x, y (x NC y NC y = (2cc x))}))
 
Theoremfnspac 6282 The special set generator is a function over the cardinals. (Contributed by SF, 18-Mar-2015.)
Spac Fn NC
 
Theoremspacssnc 6283 The special set generator generates a set of cardinals. (Contributed by SF, 13-Mar-2015.)
(N NC → ( SpacN) NC )
 
Theoremspacid 6284 The initial value of the special set generator is an element. (Contributed by SF, 13-Mar-2015.)
(M NCM ( SpacM))
 
Theoremspaccl 6285 Closure law for the special set generator. (Contributed by SF, 13-Mar-2015.)
((M NC N ( SpacM) (Nc 0c) NC ) → (2cc N) ( SpacM))
 
Theoremspacind 6286* Inductive law for the special set generator. (Contributed by SF, 13-Mar-2015.)
(((M NC S V) (M S x ( SpacM)((x S (xc 0c) NC ) → (2cc x) S))) → ( SpacM) S)
 
Theoremspacis 6287* Induction scheme for the special set generator. (Contributed by SF, 13-Mar-2015.)
{x φ} V    &   (x = M → (φψ))    &   (x = y → (φχ))    &   (x = (2cc y) → (φθ))    &   (x = N → (φτ))    &   (M NCψ)    &   (((M NC y ( SpacM)) ((yc 0c) NC χ)) → θ)       ((M NC N ( SpacM)) → τ)
 
Theoremnchoicelem1 6288 Lemma for nchoice 6307. A finite cardinal is not one more than its T-raising. (Contributed by SF, 3-Mar-2015.)
(A Nn → ¬ A = ( Tc A +c 1c))
 
Theoremnchoicelem2 6289 Lemma for nchoice 6307. A finite cardinal is not two more than its T-raising. (Contributed by SF, 12-Mar-2015.)
(A Nn → ¬ A = ( Tc A +c 2c))
 
Theoremnchoicelem3 6290 Lemma for nchoice 6307. Compute the value of Spac when the argument is not exponentiable. Theorem 6.2 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
((M NC ¬ (Mc 0c) NC ) → ( SpacM) = {M})
 
Theoremnchoicelem4 6291 Lemma for nchoice 6307. The initial value of Spac is a minimum value. Theorem 6.4 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
((M NC N ( SpacM)) → Mc N)
 
Theoremnchoicelem5 6292 Lemma for nchoice 6307. A cardinal is not a member of the special set of itself raised to two. Theorem 6.5 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
((M NC (Mc 0c) NC ) → ¬ M ( Spac ‘(2cc M)))
 
Theoremnchoicelem6 6293 Lemma for nchoice 6307. Split the special set generator into base and inductive values. Theorem 6.6 of [Specker] p. 973. (Contributed by SF, 13-Mar-2015.)
((M NC (Mc 0c) NC ) → ( SpacM) = ({M} ∪ ( Spac ‘(2cc M))))
 
Theoremnchoicelem7 6294 Lemma for nchoice 6307. Calculate the cardinality of a special set generator. Theorem 6.7 of [Specker] p. 974. (Contributed by SF, 13-Mar-2015.)
((M NC (Mc 0c) NC ) → Nc ( SpacM) = ( Nc ( Spac ‘(2cc M)) +c 1c))
 
Theoremnchoicelem8 6295 Lemma for nchoice 6307. An anti-closure condition for cardinal exponentiation to zero. Theorem 4.5 of [Specker] p. 973. (Contributed by SF, 18-Mar-2015.)
(( ≤c We NC M NC ) → (¬ (Mc 0c) NCNc 1c <c M))
 
Theoremnchoicelem9 6296 Lemma for nchoice 6307. Calculate the cardinality of the special set generator when near the end of raisability. Theorem 6.8 of [Specker] p. 974. (Contributed by SF, 18-Mar-2015.)
(( ≤c We NC M NC ¬ (Mc 0c) NC ) → ( Nc ( SpacTc M) = 2c Nc ( SpacTc M) = 3c))
 
Theoremnchoicelem10 6297 Lemma for nchoice 6307. Stratification helper lemma. (Contributed by SF, 18-Mar-2015.)
S V    &   X V       (c, X ∼ (( Ins3 S Ins2 ∼ ran ( S ⊗ ( S Fix ( S ImageS)))) “ 1c) ↔ c = Clos1 (X, S))
 
Theoremnchoicelem11 6298* Lemma for nchoice 6307. Set up stratification for nchoicelem12 6299. (Contributed by SF, 18-Mar-2015.)
{t m NC (t = Nc ( SpacTc m) → Nc ( Spacm) Nn )} V
 
Theoremnchoicelem12 6299 Lemma for nchoice 6307. If the T-raising of a cardinal yields a finite special set, then so does the initial set. Theorem 7.1 of [Specker] p. 974. (Contributed by SF, 18-Mar-2015.)
((M NC ( SpacTc M) Fin ) → ( SpacM) Fin )
 
Theoremnchoicelem13 6300 Lemma for nchoice 6307. The cardinality of a special set is at least one. (Contributed by SF, 18-Mar-2015.)
(M NC → 1cc Nc ( SpacM))
    < Previous  Next >

Page List
Jump to page: Contents  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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6336
  Copyright terms: Public domain < Previous  Next >