 Home New Foundations ExplorerTheorem 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-6337   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremnchoicelem13 6301 Lemma for nchoice 6308. The cardinality of a special set is at least one. (Contributed by SF, 18-Mar-2015.)
(M NC → 1cc Nc ( SpacM))

Theoremnchoicelem14 6302 Lemma for nchoice 6308. 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 6303 Lemma for nchoice 6308. 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 6304* Lemma for nchoice 6308. Set up stratification for nchoicelem17 6305. (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 6305 Lemma for nchoice 6308. 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 6306 Lemma for nchoice 6308. Set up stratification for nchoicelem19 6307. (Contributed by SF, 20-Mar-2015.)
{x ( Spacx) Fin } V

Theoremnchoicelem19 6307 Lemma for nchoice 6308. 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 6308 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 6309 Extend the definition of a class to include the finite recursive function generator.
class FRec (F, I)

Definitiondf-frec 6310* 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 6311 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 6312 The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
F = FRec (G, I)       (G VF V)

Theoremfrecex 6313 The finite recursive function generator preserves sethood. (Contributed by Scott Fenton, 30-Jul-2019.)
F = FRec (G, I)    &   G V       F V

Theoremfrecxp 6314 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 6315 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 6316 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 6317* Lemma for fnfrec 6320. Establish stratification for induction. (Contributed by Scott Fenton, 31-Jul-2019.)
(F V → {w yz((wFy wFz) → y = z)} V)

Theoremfnfreclem2 6318 Lemma for fnfrec 6320. 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 6319* Lemma for fnfrec 6320. 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 6320 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 6321 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 6322 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 6323 Extend the definition of class to include the class of all Cantorian sets.
class Can

Definitiondf-can 6324 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 6325 Extend the definition of class to include the class of all strongly Cantorian sets.
class SCan

Definitiondf-scan 6326* 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 6327* The domain of the singleton function. (Contributed by Scott Fenton, 20-Apr-2021.)
dom (x A {x}) = A

Theoremepelcres 6328 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 6329 Membership in the class of Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
(A Can1AA)

Theoremelscan 6330* Membership in the class of strongly Cantorian sets. (Contributed by Scott Fenton, 19-Apr-2021.)
(A SCan ↔ (x A {x}) V)

Theoremscancan 6331 Strongly Cantorian implies Cantorian. Observation from [Holmes], p. 134. (Contributed by Scott Fenton, 19-Apr-2021.)
(A SCanA Can )

Theoremcanncb 6332 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 6333 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 6334 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 6335 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 6336 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 6337 The universe is not Cantorian. Theorem XI.1.8 of [Rosser] p. 348. (Contributed by Scott Fenton, 22-Apr-2021.)
¬ V Can

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-6337
 Copyright terms: Public domain < Previous  Wrap >