HomeHome New Foundations Explorer
Theorem List (p. 64 of 64)
< Previous  Wrap >
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 - 6301-6336   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremnchoicelem14 6301 Lemma for nchoice 6307. When the special set generator yields a singleton, then the cardinal is not raisable. (Contributed by SF, 19-Mar-2015.)
((M NC Nc ( SpacM) = 1c) → ¬ (Mc 0c) NC )
 
Theoremnchoicelem15 6302 Lemma for nchoice 6307. When the special set generator does not yield a singleton, then the cardinal is raisable. (Contributed by SF, 19-Mar-2015.)
((M NC 1c <c Nc ( SpacM)) → (Mc 0c) NC )
 
Theoremnchoicelem16 6303* Lemma for nchoice 6307. Set up stratification for nchoicelem17 6304. (Contributed by SF, 19-Mar-2015.)
{t ( ≤c We NCm NC ( Nc ( Spacm) = (1c +c t) → (( SpacTc m) Fin ( Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 1c) Nc ( SpacTc m) = ( Tc Nc ( Spacm) +c 2c)))))} V
 
Theoremnchoicelem17 6304 Lemma for nchoice 6307. If the special set of a cardinal is finite, then so is the special set of its T-raising, and there is a calculable relationship between their sizes. Theorem 7.2 of [Specker] p. 974. (Contributed by SF, 19-Mar-2015.)
(( ≤c We NC M NC ( SpacM) Fin ) → (( SpacTc M) Fin ( Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 1c) Nc ( SpacTc M) = ( Tc Nc ( SpacM) +c 2c))))
 
Theoremnchoicelem18 6305 Lemma for nchoice 6307. Set up stratification for nchoicelem19 6306. (Contributed by SF, 20-Mar-2015.)
{x ( Spacx) Fin } V
 
Theoremnchoicelem19 6306 Lemma for nchoice 6307. Assuming well-ordering, there is a cardinal with a finite special set that is its own T-raising. Theorem 7.3 of [Specker] p. 974. (Contributed by SF, 20-Mar-2015.)
( ≤c We NCm NC (( Spacm) Fin Tc m = m))
 
Theoremnchoice 6307 Cardinal less than or equal does not well-order the cardinals. This is equivalent to saying that the axiom of choice from ZFC is false in NF. Theorem 7.5 of [Specker] p. 974. (Contributed by SF, 20-Mar-2015.)
¬ ≤c We NC
 
2.4.7  Finite recursion
 
Syntaxcfrec 6308 Extend the definition of a class to include the finite recursive function generator.
class FRec (F, I)
 
Definitiondf-frec 6309* Define the finite recursive function generator. This is a function over Nn that obeys the standard recursion relationship. Definition adapted from theorem XI.3.24 of [Rosser] p. 412. (Contributed by Scott Fenton, 30-Jul-2019.)
FRec (F, I) = Clos1 ({0c, I}, PProd ((x V (x +c 1c)), F))
 
Theoremfreceq12 6310 Equality theorem for finite recursive function generator. (Contributed by Scott Fenton, 31-Jul-2019.)
((F = G I = J) → FRec (F, I) = FRec (G, J))
 
Theoremfrecexg 6311 The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
F = FRec (G, I)       (G VF V)
 
Theoremfrecex 6312 The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
F = FRec (G, I)    &   G V       F V
 
Theoremfrecxp 6313 Subset relationship for the finite recursive function generator. (Contributed by Scott Fenton, 30-Jul-2019.)
F = FRec (G, I)    &   G V       F ( Nn × (ran G ∪ {I}))
 
Theoremfrecxpg 6314 Subset relationship for the finite recursive function generator. (Contributed by Scott Fenton, 31-Jul-2019.)
F = FRec (G, I)       (G VF ( Nn × (ran G ∪ {I})))
 
Theoremdmfrec 6315 The domain of the finite recursive function generator is the naturals. (Contributed by Scott Fenton, 31-Jul-2019.)
F = FRec (G, I)    &   (φG V)    &   (φI dom G)    &   (φ → ran G dom G)       (φ → dom F = Nn )
 
Theoremfnfreclem1 6316* Lemma for fnfrec 6319. Establish stratification for induction. (Contributed by Scott Fenton, 31-Jul-2019.)
(F V → {w yz((wFy wFz) → y = z)} V)
 
Theoremfnfreclem2 6317 Lemma for fnfrec 6319. Calculate the unique value of F at zero. (Contributed by Scott Fenton, 31-Jul-2019.)
F = FRec (G, I)    &   (φG V)    &   (φI dom G)    &   (φ → ran G dom G)       (φ → (0cFXX = I))
 
Theoremfnfreclem3 6318* Lemma for fnfrec 6319. The value of F at a successor is G related to a previous element. (Contributed by Scott Fenton, 31-Jul-2019.)
F = FRec (G, I)    &   (φG V)    &   (φI dom G)    &   (φ → ran G dom G)    &   (φX Nn )    &   (φ → (X +c 1c)FY)       (φz(XFz zGY))
 
Theoremfnfrec 6319 The recursive function generator is a function over the finite cardinals. (Contributed by Scott Fenton, 31-Jul-2019.)
F = FRec (G, I)    &   (φG Funs )    &   (φI dom G)    &   (φ → ran G dom G)       (φF Fn Nn )
 
Theoremfrec0 6320 Calculate the value of the finite recursive function generator at zero. (Contributed by Scott Fenton, 31-Jul-2019.)
F = FRec (G, I)    &   (φG Funs )    &   (φI dom G)    &   (φ → ran G dom G)       (φ → (F ‘0c) = I)
 
Theoremfrecsuc 6321 Calculate the value of the finite recursive function generator at a successor. (Contributed by Scott Fenton, 31-Jul-2019.)
F = FRec (G, I)    &   (φG Funs )    &   (φI dom G)    &   (φ → ran G dom G)    &   (φX Nn )       (φ → (F ‘(X +c 1c)) = (G ‘(FX)))
 
2.5  Cantorian and Strongly Cantorian Sets
 
Syntaxccan 6322 Extend the definition of class to include the class of all Cantorian sets.
class Can
 
Definitiondf-can 6323 Define the class of all Cantorian sets. These are so-called because Cantor's Theorem Nc A <c Nc A holds for these sets. Definition from [Rosser] p. 347 and [Holmes] p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
Can = {x 1xx}
 
Syntaxcscan 6324 Extend the definition of class to include the class of all strongly Cantorian sets.
class SCan
 
Definitiondf-scan 6325* Define the class of strongly Cantorian sets. Unlike general Cantorian sets, this fixes a specific mapping between x and 1x. Definition from [Holmes] p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
SCan = {x (y x {y}) V}
 
Theoremdmsnfn 6326* The domain of the singleton function. (Contributed by Scott Fenton, 20-Apr-2021.)
dom (x A {x}) = A
 
Theoremepelcres 6327 Version of epelc 4765 with a restriction in place. (Contributed by Scott Fenton, 20-Apr-2021.)
Y V       (X A → (X( E A)YX Y))
 
Theoremelcan 6328 Membership in the class of Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
(A Can1AA)
 
Theoremelscan 6329* Membership in the class of strongly Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
(A SCan ↔ (x A {x}) V)
 
Theoremscancan 6330 Strongly Cantorian implies Cantorian. Observation from [Holmes], p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
(A SCanA Can )
 
Theoremcanncb 6331 The cardinality of a Cantorian set is equal to the cardinality of its unit power set. (Contributed by Scott Fenton, 23-Apr-2021.)
(A V → (A CanNc 1A = Nc A))
 
Theoremcannc 6332 The cardinality of a Cantorian set is equal to the cardinality of its unit power set. (Contributed by Scott Fenton, 21-Apr-2021.)
(A CanNc 1A = Nc A)
 
Theoremcanltpw 6333 The cardinality of a Cantorian set is strictly less than the cardinality of its power set. (Contributed by Scott Fenton, 21-Apr-2021.)
(A CanNc A <c Nc A)
 
Theoremcantcb 6334 The cardinality of a Cantorian set is equal to the Tc raising of that cardinal. (Contributed by Scott Fenton, 23-Apr-2021.)
(A V → (A CanTc Nc A = Nc A))
 
Theoremcantc 6335 The cardinality of a Cantorian set is equal to the Tc raising of that cardinal. (Contributed by Scott Fenton, 22-Apr-2021.)
(A CanTc Nc A = Nc A)
 
Theoremvncan 6336 The universe is not Cantorian. Theorem XI.1.8 of [Rosser] p. 348. (Contributed by Scott Fenton, 22-Apr-2021.)
¬ V Can
    < Previous  Wrap >

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  Wrap >