HomeHome New Foundations Explorer
Theorem List (p. 45 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 - 4401-4500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem0cnsuc 4401 Cardinal zero is not a successor. Compare Theorem X.1.2 of [Rosser] p. 275. (Contributed by SF, 14-Jan-2015.)
(A +c 1c) ≠ 0c
 
Theorempeano1 4402 Cardinal zero is a finite cardinal. Theorem X.1.4 of [Rosser] p. 276. (Contributed by SF, 14-Jan-2015.)
0c Nn
 
Theorempeano2 4403 The finite cardinals are closed under addition of one. Theorem X.1.5 of [Rosser] p. 276. (Contributed by SF, 14-Jan-2015.)
(A Nn → (A +c 1c) Nn )
 
Theorempeano3 4404 The successor of a finite cardinal is not zero. (Contributed by SF, 14-Jan-2015.)
(A Nn → (A +c 1c) ≠ 0c)
 
Theoremaddcid1 4405 Cardinal zero is a fixed point for cardinal addition. Theorem X.1.8 of [Rosser] p. 276. (Contributed by SF, 16-Jan-2015.)
(A +c 0c) = A
 
Theoremaddccom 4406 Cardinal sum commutes. Theorem X.1.9 of [Rosser] p. 276. (Contributed by SF, 15-Jan-2015.)
(A +c B) = (B +c A)
 
Theoremaddcid2 4407 Cardinal zero is a fixed point for cardinal addition. Theorem X.1.8 of [Rosser] p. 276. (Contributed by SF, 16-Jan-2015.)
(0c +c A) = A
 
Theorem1cnnc 4408 Cardinal one is a finite cardinal. Theorem X.1.12 of [Rosser] p. 277. (Contributed by SF, 16-Jan-2015.)
1c Nn
 
Theorempeano5 4409* The principle of mathematical induction: a set containing cardinal zero and closed under the successor operator is a superset of the finite cardinals. Theorem X.1.6 of [Rosser] p. 276. (Contributed by SF, 14-Jan-2015.)
((A V 0c A x Nn (x A → (x +c 1c) A)) → Nn A)
 
Theoremfindsd 4410* Principle of finite induction over the finite cardinals, using implicit substitutions. The first hypothesis ensures stratification of φ, the next four set up the substitutions, and the last two set up the base case and induction hypothesis. This version allows for an extra deduction clause that may make proving stratification simpler. Compare Theorem X.1.13 of [Rosser] p. 277. (Contributed by SF, 31-Jul-2019.)
(η → {x φ} V)    &   (x = 0c → (φψ))    &   (x = y → (φχ))    &   (x = (y +c 1c) → (φθ))    &   (x = A → (φτ))    &   (ηψ)    &   ((y Nn η) → (χθ))       ((A Nn η) → τ)
 
Theoremfinds 4411* Principle of finite induction over the finite cardinals, using implicit substitutions. The first hypothesis ensures stratification of φ, the next four set up the substitutions, and the last two set up the base case and induction hypothesis. Compare Theorem X.1.13 of [Rosser] p. 277. (Contributed by SF, 14-Jan-2015.)
{x φ} V    &   (x = 0c → (φψ))    &   (x = y → (φχ))    &   (x = (y +c 1c) → (φθ))    &   (x = A → (φτ))    &   ψ    &   (y Nn → (χθ))       (A Nnτ)
 
Theoremnnc0suc 4412* All naturals are either zero or a successor. Theorem X.1.7 of [Rosser] p. 276. (Contributed by SF, 14-Jan-2015.)
(A Nn ↔ (A = 0c x Nn A = (x +c 1c)))
 
Theoremelsuc 4413* Membership in a successor. Theorem X.1.16 of [Rosser] p. 279. (Contributed by SF, 16-Jan-2015.)
(A (M +c 1c) ↔ b M x bA = (b ∪ {x}))
 
Theoremelsuci 4414 Lemma for ncfinraise 4481. Take a natural and a disjoint union and compute membership in the successor natural. (Contributed by SF, 22-Jan-2015.)
X V       ((A N ¬ X A) → (A ∪ {X}) (N +c 1c))
 
Theoremaddcass 4415 Cardinal addition is associative. Theorem X.1.11, corollary 1 of [Rosser] p. 277. (Contributed by SF, 17-Jan-2015.)
((A +c B) +c C) = (A +c (B +c C))
 
Theoremaddc32 4416 Swap arguments two and three in cardinal addition. (Contributed by SF, 22-Jan-2015.)
((A +c B) +c C) = ((A +c C) +c B)
 
Theoremaddc4 4417 Swap arguments two and three in quadruple cardinal addition. (Contributed by SF, 25-Jan-2015.)
((A +c B) +c (C +c D)) = ((A +c C) +c (B +c D))
 
Theoremaddc6 4418 Rearrange cardinal summation of six arguments. (Contributed by SF, 13-Mar-2015.)
(((A +c B) +c (C +c D)) +c (E +c F)) = (((A +c C) +c E) +c ((B +c D) +c F))
 
Theoremnncaddccl 4419 The finite cardinals are closed under addition. Theorem X.1.14 of [Rosser] p. 278. (Contributed by SF, 17-Jan-2015.)
((A Nn B Nn ) → (A +c B) Nn )
 
Theoremelfin 4420* Membership in the set of finite sets. (Contributed by SF, 19-Jan-2015.)
(A Finx Nn A x)
 
Theoremel0c 4421 Membership in cardinal zero. (Contributed by SF, 22-Jan-2015.)
(A 0cA = )
 
Theoremnulel0c 4422 The empty set is a member of cardinal zero. (Contributed by SF, 13-Feb-2015.)
0c
 
Theorem0fin 4423 The empty set is finite. (Contributed by SF, 19-Jan-2015.)
Fin
 
Theoremnnsucelrlem1 4424* Lemma for nnsucelr 4428. Establish stratification for the inductive hypothesis. (Contributed by SF, 15-Jan-2015.)
{m ax((¬ x a (a ∪ {x}) (m +c 1c)) → a m)} V
 
Theoremnnsucelrlem2 4425 Lemma for nnsucelr 4428. Subtracting a non-element from a set adjoined with the non-element retrieves the original set. (Contributed by SF, 15-Jan-2015.)
B A → ((A ∪ {B}) {B}) = A)
 
Theoremnnsucelrlem3 4426 Lemma for nnsucelr 4428. Rearrange union and difference for a particular group of classes. (Contributed by SF, 15-Jan-2015.)
X V       ((XY (A ∪ {X}) = (B ∪ {Y}) ¬ Y B) → B = ((A {Y}) ∪ {X}))
 
Theoremnnsucelrlem4 4427 Lemma for nnsucelr 4428. Remove and re-adjoin an element to a set. (Contributed by SF, 15-Jan-2015.)
(A B → ((B {A}) ∪ {A}) = B)
 
Theoremnnsucelr 4428 Transfer membership in the successor of a natural into membership of the natural itself. Theorem X.1.17 of [Rosser] p. 525. (Contributed by SF, 14-Jan-2015.)
A V    &   X V       ((M Nn X A (A ∪ {X}) (M +c 1c))) → A M)
 
Theoremnndisjeq 4429 Either two naturals are disjoint or they are the same natural. Theorem X.1.18 of [Rosser] p. 526. (Contributed by SF, 17-Jan-2015.)
((M Nn N Nn ) → ((MN) = M = N))
 
Theoremnnceleq 4430 If two naturals have an element in common, then they are equal. (Contributed by SF, 13-Feb-2015.)
(((M Nn N Nn ) (A M A N)) → M = N)
 
Theoremsnfi 4431 A singleton is finite. (Contributed by SF, 23-Feb-2015.)
{A} Fin
 
2.2.11  Deriving infinity
 
Syntaxclefin 4432 Extend class notation to include the less than or equal to relationship for finite cardinals.
class fin
 
Syntaxcltfin 4433 Extend class notation to include the less than relationship for finite cardinals.
class <fin
 
Syntaxcncfin 4434 Extend class notation to include the finite cardinal function.
class Ncfin A
 
Syntaxctfin 4435 Extend class notation to include the finite T operation.
class Tfin A
 
Syntaxcevenfin 4436 Extend class notation to include the (temporary) set of all even numbers.
class Evenfin
 
Syntaxcoddfin 4437 Extend class notation to include the (temporary) set of all odd numbers.
class Oddfin
 
Syntaxwsfin 4438 Extend wff notation to include the finite S relationship.
wff Sfin (A, B)
 
Syntaxcspfin 4439 Extend class notation to include the finite Sp set.
class Spfin
 
Definitiondf-lefin 4440* Define the less than or equal to relationship for finite cardinals. Definition from Ex. X.1.4 of [Rosser] p. 279. (Contributed by SF, 12-Jan-2015.)
fin = {x yz(x = ⟪y, z w Nn z = (y +c w))}
 
Definitiondf-ltfin 4441* Define the less than relationship for finite cardinals. Definition from [Rosser] p. 527. (Contributed by SF, 12-Jan-2015.)
<fin = {x mn(x = ⟪m, n (m p Nn n = ((m +c p) +c 1c)))}
 
Definitiondf-ncfin 4442* Define the finite cardinal function. Definition from [Rosser] p. 527. (Contributed by SF, 12-Jan-2015.)
Ncfin A = (℩x(x Nn A x))
 
Definitiondf-tfin 4443* Define the finite T operator. Definition from [Rosser] p. 528. (Contributed by SF, 12-Jan-2015.)
Tfin M = if(M = , , (℩n(n Nn a M 1a n)))
 
Definitiondf-evenfin 4444* Define the temporary set of all even numbers. This differs from the final definition due to the non-null condition. Definition from [Rosser] p. 529. (Contributed by SF, 12-Jan-2015.)
Evenfin = {x (n Nn x = (n +c n) x)}
 
Definitiondf-oddfin 4445* Define the temporary set of all odd numbers. This differs from the final definition due to the non-null condition. Definition from [Rosser] p. 529. (Contributed by SF, 12-Jan-2015.)
Oddfin = {x (n Nn x = ((n +c n) +c 1c) x)}
 
Definitiondf-sfin 4446* Define the finite S relationship. This relationship encapsulates the idea of M being a "smaller" number than N. Definition from [Rosser] p. 530. (Contributed by SF, 12-Jan-2015.)
( Sfin (M, N) ↔ (M Nn N Nn a(1a M a N)))
 
Definitiondf-spfin 4447* Define the finite Sp set. Definition from [Rosser] p. 533. (Contributed by SF, 12-Jan-2015.)
Spfin = {a ( Ncfin V a x a z( Sfin (z, x) → z a))}
 
Theoremopklefing 4448* Kuratowski ordered pair membership in finite less than or equal to. (Contributed by SF, 18-Jan-2015.)
((A V B W) → (⟪A, Bfinx Nn B = (A +c x)))
 
Theoremopkltfing 4449* Kuratowski ordered pair membership in finite less than. (Contributed by SF, 27-Jan-2015.)
((A V B W) → (⟪A, B <fin ↔ (A x Nn B = ((A +c x) +c 1c))))
 
Theoremlefinaddc 4450 Cardinal sum always yields a larger set. (Contributed by SF, 27-Jan-2015.)
((A V N Nn ) → ⟪A, (A +c N)⟫ fin )
 
Theoremprepeano4 4451 Assuming a non-null successor, cardinal successor is one-to-one. Theorem X.1.19 of [Rosser] p. 526. (Contributed by SF, 18-Jan-2015.)
(((M Nn N Nn ) ((M +c 1c) = (N +c 1c) (M +c 1c) ≠ )) → M = N)
 
Theoremaddcnul1 4452 Cardinal addition with the empty set. Theorem X.1.20, corollary 1 of [Rosser] p. 526. (Contributed by SF, 18-Jan-2015.)
(A +c ) =
 
Theoremaddcnnul 4453 If cardinal addition is non-empty, then both addends are non-empty. Theorem X.1.20 of [Rosser] p. 526. (Contributed by SF, 18-Jan-2015.)
((A +c B) ≠ → (A B))
 
Theorempreaddccan2lem1 4454* Lemma for preaddccan2 4455. Establish stratification for the induction step. (Contributed by SF, 30-Mar-2021.)
((N Nn P Nn ) → {m (((m +c N) ≠ (m +c N) = (m +c P)) → N = P)} V)
 
Theorempreaddccan2 4455 Cancellation law for natural addition with a non-null condition. (Contributed by SF, 29-Jan-2015.)
(((M Nn N Nn P Nn ) (M +c N) ≠ ) → ((M +c N) = (M +c P) ↔ N = P))
 
Theoremnulge 4456 If the empty set is a finite cardinal, then it is a maximal element. (Contributed by SF, 19-Jan-2015.)
(( Nn A V) → ⟪A, fin )
 
Theoremltfinirr 4457 Irreflexive law for finite less than. (Contributed by SF, 29-Jan-2015.)
(A Nn → ¬ ⟪A, A <fin )
 
Theoremleltfintr 4458 Transitivity law for finite less than and less than or equal. (Contributed by SF, 2-Feb-2015.)
((A Nn B Nn C Nn ) → ((⟪A, Bfin B, C <fin ) → ⟪A, C <fin ))
 
Theoremltfintr 4459 Transitivity law for finite less than. (Contributed by SF, 29-Jan-2015.)
((A Nn B Nn C Nn ) → ((⟪A, B <fin B, C <fin ) → ⟪A, C <fin ))
 
Theoremltfinasym 4460 Asymmetry law for finite less than. (Contributed by SF, 29-Jan-2015.)
((A Nn B Nn ) → (⟪A, B <fin → ¬ ⟪B, A <fin ))
 
Theorem0cminle 4461 Cardinal zero is a minimal element for finite less than or equal. (Contributed by SF, 29-Jan-2015.)
(A Nn → ⟪0c, Afin )
 
Theoremltfinp1 4462 One plus a finite cardinal is strictly greater. (Contributed by SF, 29-Jan-2015.)
((A V A) → ⟪A, (A +c 1c)⟫ <fin )
 
Theoremlefinlteq 4463 Transfer from less than or equal to less than. (Contributed by SF, 29-Jan-2015.)
((A V B W A) → (⟪A, Bfin ↔ (⟪A, B <fin A = B)))
 
Theoremltfinex 4464 Finite less than is stratified. (Contributed by SF, 29-Jan-2015.)
<fin V
 
Theoremltfintrilem1 4465* Lemma for ltfintri 4466. Establish stratification for induction. (Contributed by SF, 29-Jan-2015.)
{m (n Nn → (m → (⟪m, n <fin m = n n, m <fin )))} V
 
Theoremltfintri 4466 Trichotomy law for finite less than. (Contributed by SF, 29-Jan-2015.)
((M Nn N Nn M) → (⟪M, N <fin M = N N, M <fin ))
 
Theoremlefinrflx 4467 Less than or equal to is reflexive. (Contributed by SF, 2-Feb-2015.)
(A V → ⟪A, Afin )
 
Theoremltlefin 4468 Less than implies less than or equal. (Contributed by SF, 2-Feb-2015.)
((A V B W) → (⟪A, B <fin → ⟪A, Bfin ))
 
Theoremlenltfin 4469 Less than or equal is the same as negated less than. (Contributed by SF, 2-Feb-2015.)
((A Nn B Nn ) → (⟪A, Bfin ↔ ¬ ⟪B, A <fin ))
 
Theoremssfin 4470 A subset of a finite set is itself finite. Theorem X.1.21 of [Rosser] p. 527. (Contributed by SF, 19-Jan-2015.)
((A V B Fin A B) → A Fin )
 
Theoremvfinnc 4471* If the universe is finite, then there is a unique natural containing any set. Theorem X.1.22 of [Rosser] p. 527. (Contributed by SF, 19-Jan-2015.)
((A V V Fin ) → ∃!x Nn A x)
 
Theoremncfinex 4472 The finite cardinality of a set exists. (Contributed by SF, 27-Jan-2015.)
Ncfin A V
 
Theoremncfineq 4473 Equality theorem for finite cardinality. (Contributed by SF, 20-Jan-2015.)
(A = BNcfin A = Ncfin B)
 
Theoremncfinprop 4474 Properties of finite cardinal number. Theorem X.1.23 of [Rosser] p. 527 (Contributed by SF, 20-Jan-2015.)
((V Fin A V) → ( Ncfin A Nn A Ncfin A))
 
Theoremncfindi 4475 Distribution law for finite cardinality. (Contributed by SF, 30-Jan-2015.)
(((V Fin A V) B W (AB) = ) → Ncfin (AB) = ( Ncfin A +c Ncfin B))
 
Theoremncfinsn 4476 If the universe is finite, then the cardinality of a singleton is 1c. (Contributed by SF, 30-Jan-2015.)
((V Fin A V) → Ncfin {A} = 1c)
 
Theoremncfineleq 4477 Equality law for finite cardinality. Theorem X.1.24 of [Rosser] p. 527. (Contributed by SF, 20-Jan-2015.)
((V Fin A V B W) → (A Ncfin BNcfin A = Ncfin B))
 
Theoremeqpwrelk 4478 Represent equality to power class via a Kuratowski relationship. (Contributed by SF, 26-Jan-2015.)
A V    &   B V       (⟪{A}, B ∼ (( Ins2k SkIns3k SIk Sk ) “k 111c) ↔ B = A)
 
Theoremeqpw1relk 4479 Represent equality to unit power class via a Kuratowski relationship. (Contributed by SF, 21-Jan-2015.)
A V    &   B V       (⟪A, {B}⟫ ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ↔ A = 1B)
 
Theoremncfinraiselem2 4480* Lemma for ncfinraise 4481. Show stratification for induction. (Contributed by SF, 22-Jan-2015.)
{m a m b m n Nn (1a n 1b n)} V
 
Theoremncfinraise 4481* If two sets are in a particular finite cardinal, then their unit power sets are in the same natural. Theorem X.1.25 of [Rosser] p. 527. (Contributed by SF, 21-Jan-2015.)
((M Nn A M B M) → n Nn (1A n 1B n))
 
Theoremncfinlowerlem1 4482* Lemma for ncfinlower 4483. Set up stratification for induction. (Contributed by SF, 22-Jan-2015.)
{m ab((1a m 1b m) → n Nn (a n b n))} V
 
Theoremncfinlower 4483* If the unit power classes of two sets are in the same natural, then so are the sets themselves. Theorem X.1.26 of [Rosser] p. 527. (Contributed by SF, 22-Jan-2015.)
((M Nn 1A M 1B M) → n Nn (A n B n))
 
Theoremnnpw1ex 4484* For any non-empty finite cardinal, there is a unique natural containing a unit power class of one of its elements. Theorem X.1.27 of [Rosser] p. 528. (Contributed by SF, 22-Jan-2015.)
((M Nn M) → ∃!n Nn a M 1a n)
 
Theoremtfinex 4485 The finite T operator is always a set. (Contributed by SF, 26-Jan-2015.)
Tfin A V
 
Theoremeqtfinrelk 4486 Equality to a T raising expressed via a Kuratowski relationship. (Contributed by SF, 29-Jan-2015.)
M V    &   X V       (⟪{M}, X (({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) ↔ X = Tfin M)
 
Theoremtfinrelkex 4487 The expression at the core of eqtfinrelk 4486 exists. (Contributed by SF, 30-Jan-2015.)
(({{}} ×k {}) ∪ ( ∼ (( Ins2k SkIns3k (( Ins3k k Sk Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk SkIns3k (( Ins3k SIk ((1c ×k V) (( Ins3k SkIns2k SIk Sk ) “k 1111c)) ∩ Ins2k Sk ) “k 111c)) “k 1111c)) ⊕ Ins3k Ik ) “k 11c)) “k 11c)) “k 111c) ({{}} ×k V))) V
 
Theoremtfineq 4488 Equality theorem for the finite T operator. (Contributed by SF, 24-Jan-2015.)
(A = BTfin A = Tfin B)
 
Theoremtfinprop 4489* Properties of the finite T operator for a non-empty natural. Theorem X.1.28 of [Rosser] p. 528. (Contributed by SF, 22-Jan-2015.)
((M Nn M) → ( Tfin M Nn a M 1a Tfin M))
 
Theoremtfinnnul 4490 If M is a non-empty natural, then Tfin M is also non-empty. Corollary 1 of Theorem X.1.28 of [Rosser] p. 528. (Contributed by SF, 23-Jan-2015.)
((M Nn M) → Tfin M)
 
Theoremtfinnul 4491 The finite T operator applied to the empty set is empty. Theorem X.1.29 of [Rosser] p. 528. (Contributed by SF, 22-Jan-2015.)
Tfin =
 
Theoremtfincl 4492 Closure law for finite T operation. (Contributed by SF, 2-Feb-2015.)
(N NnTfin N Nn )
 
Theoremtfin11 4493 The finite T operator is one-to-one over the naturals. Theorem X.1.30 of [Rosser] p. 528. (Contributed by SF, 24-Jan-2015.)
((M Nn N Nn Tfin M = Tfin N) → M = N)
 
Theoremtfinpw1 4494 The finite T operator on a natural contains the unit power class of any element of the natural. Theorem X.1.31 of [Rosser] p. 528. (Contributed by SF, 24-Jan-2015.)
((M Nn A M) → 1A Tfin M)
 
Theoremncfintfin 4495 Relationship between finite T operator and finite Nc operation in a finite universe. Corollary of Theorem X.1.31 of [Rosser] p. 529. (Contributed by SF, 24-Jan-2015.)
((V Fin A V) → Tfin Ncfin A = Ncfin 1A)
 
Theoremtfindi 4496 The finite T operation distributes over non-empty cardinal sum. Theorem X.1.32 of [Rosser] p. 529. (Contributed by SF, 26-Jan-2015.)
((M Nn N Nn (M +c N) ≠ ) → Tfin (M +c N) = ( Tfin M +c Tfin N))
 
Theoremtfin0c 4497 The finite T operator is fixed at 0c. (Contributed by SF, 29-Jan-2015.)
Tfin 0c = 0c
 
Theoremtfinsuc 4498 The finite T operator over a successor. (Contributed by SF, 30-Jan-2015.)
((A Nn (A +c 1c) ≠ ) → Tfin (A +c 1c) = ( Tfin A +c 1c))
 
Theoremtfin1c 4499 The finite T operator is idempotent over 1c. Theorem X.1.34(a) of [Rosser] p. 529. (Contributed by SF, 30-Jan-2015.)
Tfin 1c = 1c
 
Theoremtfinltfinlem1 4500 Lemma for tfinltfin 4501. Prove the forward direction of the theorem. (Contributed by SF, 2-Feb-2015.)
((M Nn N Nn ) → (⟪M, N <fin → ⟪ Tfin M, Tfin N <fin ))
    < 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 >