P. 45 of Theorem List - New Foundations Explorer

Theorem List for New Foundations Explorer - 4401-4500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0nelsuc 4401	The empty class is not a member of a successor. (Contributed by SF, 14-Jan-2015.)
⊢ ¬ ∅ ∈ (A +c 1c)
Theorem	0cnsuc 4402	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
Theorem	peano1 4403	Cardinal zero is a finite cardinal. Theorem X.1.4 of [Rosser] p. 276. (Contributed by SF, 14-Jan-2015.)
⊢ 0c ∈ Nn
Theorem	peano2 4404	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 )
Theorem	peano3 4405	The successor of a finite cardinal is not zero. (Contributed by SF, 14-Jan-2015.)
⊢ (A ∈ Nn → (A +c 1c) ≠ 0c)
Theorem	addcid1 4406	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
Theorem	addccom 4407	Cardinal sum commutes. Theorem X.1.9 of [Rosser] p. 276. (Contributed by SF, 15-Jan-2015.)
⊢ (A +c B) = (B +c A)
Theorem	addcid2 4408	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
Theorem	1cnnc 4409	Cardinal one is a finite cardinal. Theorem X.1.12 of [Rosser] p. 277. (Contributed by SF, 16-Jan-2015.)
⊢ 1c ∈ Nn
Theorem	peano5 4410*	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)
Theorem	findsd 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. 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 ∧ η) → τ)
Theorem	finds 4412*	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 → τ)
Theorem	nnc0suc 4413*	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)))
Theorem	elsuc 4414*	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}))
Theorem	elsuci 4415	Lemma for ncfinraise 4482. 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))
Theorem	addcass 4416	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))
Theorem	addc32 4417	Swap arguments two and three in cardinal addition. (Contributed by SF, 22-Jan-2015.)
⊢ ((A +c B) +c C) = ((A +c C) +c B)
Theorem	addc4 4418	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))
Theorem	addc6 4419	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))
Theorem	nncaddccl 4420	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 )
Theorem	elfin 4421*	Membership in the set of finite sets. (Contributed by SF, 19-Jan-2015.)
⊢ (A ∈ Fin ↔ ∃x ∈ Nn A ∈ x)
Theorem	el0c 4422	Membership in cardinal zero. (Contributed by SF, 22-Jan-2015.)
⊢ (A ∈ 0c ↔ A = ∅)
Theorem	nulel0c 4423	The empty set is a member of cardinal zero. (Contributed by SF, 13-Feb-2015.)
⊢ ∅ ∈ 0c
Theorem	0fin 4424	The empty set is finite. (Contributed by SF, 19-Jan-2015.)
⊢ ∅ ∈ Fin
Theorem	nnsucelrlem1 4425*	Lemma for nnsucelr 4429. Establish stratification for the inductive hypothesis. (Contributed by SF, 15-Jan-2015.)
⊢ {m ∣ ∀a∀x((¬ x ∈ a ∧ (a ∪ {x}) ∈ (m +c 1c)) → a ∈ m)} ∈ V
Theorem	nnsucelrlem2 4426	Lemma for nnsucelr 4429. 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)
Theorem	nnsucelrlem3 4427	Lemma for nnsucelr 4429. Rearrange union and difference for a particular group of classes. (Contributed by SF, 15-Jan-2015.)
⊢ X ∈ V    ⇒   ⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → B = ((A ∖ {Y}) ∪ {X}))
Theorem	nnsucelrlem4 4428	Lemma for nnsucelr 4429. Remove and re-adjoin an element to a set. (Contributed by SF, 15-Jan-2015.)
⊢ (A ∈ B → ((B ∖ {A}) ∪ {A}) = B)
Theorem	nnsucelr 4429	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)
Theorem	nndisjeq 4430	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 ) → ((M ∩ N) = ∅ ∨ M = N))
Theorem	nnceleq 4431	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)
Theorem	snfi 4432	A singleton is finite. (Contributed by SF, 23-Feb-2015.)
⊢ {A} ∈ Fin
2.2.11  Deriving infinity
Syntax	clefin 4433	Extend class notation to include the less than or equal to relationship for finite cardinals.
class ≤fin
Syntax	cltfin 4434	Extend class notation to include the less than relationship for finite cardinals.
class <fin
Syntax	cncfin 4435	Extend class notation to include the finite cardinal function.
class Ncfin A
Syntax	ctfin 4436	Extend class notation to include the finite T operation.
class Tfin A
Syntax	cevenfin 4437	Extend class notation to include the (temporary) set of all even numbers.
class Evenfin
Syntax	coddfin 4438	Extend class notation to include the (temporary) set of all odd numbers.
class Oddfin
Syntax	wsfin 4439	Extend wff notation to include the finite S relationship.
wff Sfin (A, B)
Syntax	cspfin 4440	Extend class notation to include the finite Sp set.
class Spfin
Definition	df-lefin 4441*	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 ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃w ∈ Nn z = (y +c w))}
Definition	df-ltfin 4442*	Define the less than relationship for finite cardinals. Definition from [Rosser] p. 527. (Contributed by SF, 12-Jan-2015.)
⊢ <fin = {x ∣ ∃m∃n(x = ⟪m, n⟫ ∧ (m ≠ ∅ ∧ ∃p ∈ Nn n = ((m +c p) +c 1c)))}
Definition	df-ncfin 4443*	Define the finite cardinal function. Definition from [Rosser] p. 527. (Contributed by SF, 12-Jan-2015.)
⊢ Ncfin A = (℩x(x ∈ Nn ∧ A ∈ x))
Definition	df-tfin 4444*	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)))
Definition	df-evenfin 4445*	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 ≠ ∅)}
Definition	df-oddfin 4446*	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 ≠ ∅)}
Definition	df-sfin 4447*	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)))
Definition	df-spfin 4448*	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))}
Theorem	opklefing 4449*	Kuratowski ordered pair membership in finite less than or equal to. (Contributed by SF, 18-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ ≤fin ↔ ∃x ∈ Nn B = (A +c x)))
Theorem	opkltfing 4450*	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))))
Theorem	lefinaddc 4451	Cardinal sum always yields a larger set. (Contributed by SF, 27-Jan-2015.)
⊢ ((A ∈ V ∧ N ∈ Nn ) → ⟪A, (A +c N)⟫ ∈ ≤fin )
Theorem	prepeano4 4452	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)
Theorem	addcnul1 4453	Cardinal addition with the empty set. Theorem X.1.20, corollary 1 of [Rosser] p. 526. (Contributed by SF, 18-Jan-2015.)
⊢ (A +c ∅) = ∅
Theorem	addcnnul 4454	If cardinal addition is nonempty, then both addends are nonempty. Theorem X.1.20 of [Rosser] p. 526. (Contributed by SF, 18-Jan-2015.)
⊢ ((A +c B) ≠ ∅ → (A ≠ ∅ ∧ B ≠ ∅))
Theorem	preaddccan2lem1 4455*	Lemma for preaddccan2 4456. 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)
Theorem	preaddccan2 4456	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))
Theorem	nulge 4457	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 )
Theorem	ltfinirr 4458	Irreflexive law for finite less than. (Contributed by SF, 29-Jan-2015.)
⊢ (A ∈ Nn → ¬ ⟪A, A⟫ ∈ <fin )
Theorem	leltfintr 4459	Transitivity law for finite less than and less than or equal. (Contributed by SF, 2-Feb-2015.)
⊢ ((A ∈ Nn ∧ B ∈ Nn ∧ C ∈ Nn ) → ((⟪A, B⟫ ∈ ≤fin ∧ ⟪B, C⟫ ∈ <fin ) → ⟪A, C⟫ ∈ <fin ))
Theorem	ltfintr 4460	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 ))
Theorem	ltfinasym 4461	Asymmetry law for finite less than. (Contributed by SF, 29-Jan-2015.)
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (⟪A, B⟫ ∈ <fin → ¬ ⟪B, A⟫ ∈ <fin ))
Theorem	0cminle 4462	Cardinal zero is a minimal element for finite less than or equal. (Contributed by SF, 29-Jan-2015.)
⊢ (A ∈ Nn → ⟪0c, A⟫ ∈ ≤fin )
Theorem	ltfinp1 4463	One plus a finite cardinal is strictly greater. (Contributed by SF, 29-Jan-2015.)
⊢ ((A ∈ V ∧ A ≠ ∅) → ⟪A, (A +c 1c)⟫ ∈ <fin )
Theorem	lefinlteq 4464	Transfer from less than or equal to less than. (Contributed by SF, 29-Jan-2015.)
⊢ ((A ∈ V ∧ B ∈ W ∧ A ≠ ∅) → (⟪A, B⟫ ∈ ≤fin ↔ (⟪A, B⟫ ∈ <fin ∨ A = B)))
Theorem	ltfinex 4465	Finite less than is stratified. (Contributed by SF, 29-Jan-2015.)
⊢ <fin ∈ V
Theorem	ltfintrilem1 4466*	Lemma for ltfintri 4467. Establish stratification for induction. (Contributed by SF, 29-Jan-2015.)
⊢ {m ∣ (n ∈ Nn → (m ≠ ∅ → (⟪m, n⟫ ∈ <fin ∨ m = n ∨ ⟪n, m⟫ ∈ <fin )))} ∈ V
Theorem	ltfintri 4467	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 ))
Theorem	lefinrflx 4468	Less than or equal to is reflexive. (Contributed by SF, 2-Feb-2015.)
⊢ (A ∈ V → ⟪A, A⟫ ∈ ≤fin )
Theorem	ltlefin 4469	Less than implies less than or equal. (Contributed by SF, 2-Feb-2015.)
⊢ ((A ∈ V ∧ B ∈ W) → (⟪A, B⟫ ∈ <fin → ⟪A, B⟫ ∈ ≤fin ))
Theorem	lenltfin 4470	Less than or equal is the same as negated less than. (Contributed by SF, 2-Feb-2015.)
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (⟪A, B⟫ ∈ ≤fin ↔ ¬ ⟪B, A⟫ ∈ <fin ))
Theorem	ssfin 4471	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 )
Theorem	vfinnc 4472*	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)
Theorem	ncfinex 4473	The finite cardinality of a set exists. (Contributed by SF, 27-Jan-2015.)
⊢ Ncfin A ∈ V
Theorem	ncfineq 4474	Equality theorem for finite cardinality. (Contributed by SF, 20-Jan-2015.)
⊢ (A = B → Ncfin A = Ncfin B)
Theorem	ncfinprop 4475	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))
Theorem	ncfindi 4476	Distribution law for finite cardinality. (Contributed by SF, 30-Jan-2015.)
⊢ (((V ∈ Fin ∧ A ∈ V) ∧ B ∈ W ∧ (A ∩ B) = ∅) → Ncfin (A ∪ B) = ( Ncfin A +c Ncfin B))
Theorem	ncfinsn 4477	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)
Theorem	ncfineleq 4478	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 B ↔ Ncfin A = Ncfin B))
Theorem	eqpwrelk 4479	Represent equality to power class via a Kuratowski relationship. (Contributed by SF, 26-Jan-2015.)
⊢ A ∈ V    &   ⊢ B ∈ V    ⇒   ⊢ (⟪{A}, B⟫ ∈ ∼ (( Ins2k Sk ⊕ Ins3k SIk Sk ) “k ℘1℘11c) ↔ B = ℘A)
Theorem	eqpw1relk 4480	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 Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ↔ A = ℘1B)
Theorem	ncfinraiselem2 4481*	Lemma for ncfinraise 4482. Show stratification for induction. (Contributed by SF, 22-Jan-2015.)
⊢ {m ∣ ∀a ∈ m ∀b ∈ m ∃n ∈ Nn (℘1a ∈ n ∧ ℘1b ∈ n)} ∈ V
Theorem	ncfinraise 4482*	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))
Theorem	ncfinlowerlem1 4483*	Lemma for ncfinlower 4484. Set up stratification for induction. (Contributed by SF, 22-Jan-2015.)
⊢ {m ∣ ∀a∀b((℘1a ∈ m ∧ ℘1b ∈ m) → ∃n ∈ Nn (a ∈ n ∧ b ∈ n))} ∈ V
Theorem	ncfinlower 4484*	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))
Theorem	nnpw1ex 4485*	For any nonempty 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)
Theorem	tfinex 4486	The finite T operator is always a set. (Contributed by SF, 26-Jan-2015.)
⊢ Tfin A ∈ V
Theorem	eqtfinrelk 4487	Equality to a T raising expressed via a Kuratowski relationship. (Contributed by SF, 29-Jan-2015.)
⊢ M ∈ V    &   ⊢ X ∈ V    ⇒   ⊢ (⟪{M}, X⟫ ∈ (({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ↔ X = Tfin M)
Theorem	tfinrelkex 4488	The expression at the core of eqtfinrelk 4487 exists. (Contributed by SF, 30-Jan-2015.)
⊢ (({{∅}} ×k {∅}) ∪ ( ∼ (( Ins2k Sk ⊕ Ins3k (( Ins3k ◡k Sk ∖ Ins2k (( Ins2k (( Nn ×k V) ∩ (( Ins2k SIk Sk ∩ Ins3k (( Ins3k SIk ((℘1c ×k V) ∖ (( Ins3k Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ∩ Ins2k Sk ) “k ℘1℘11c)) “k ℘1℘1℘11c)) ⊕ Ins3k Ik ) “k ℘11c)) “k ℘11c)) “k ℘1℘11c) ∖ ({{∅}} ×k V))) ∈ V
Theorem	tfineq 4489	Equality theorem for the finite T operator. (Contributed by SF, 24-Jan-2015.)
⊢ (A = B → Tfin A = Tfin B)
Theorem	tfinprop 4490*	Properties of the finite T operator for a nonempty 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))
Theorem	tfinnnul 4491	If M is a nonempty natural, then Tfin M is also nonempty. Corollary 1 of Theorem X.1.28 of [Rosser] p. 528. (Contributed by SF, 23-Jan-2015.)
⊢ ((M ∈ Nn ∧ M ≠ ∅) → Tfin M ≠ ∅)
Theorem	tfinnul 4492	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 ∅ = ∅
Theorem	tfincl 4493	Closure law for finite T operation. (Contributed by SF, 2-Feb-2015.)
⊢ (N ∈ Nn → Tfin N ∈ Nn )
Theorem	tfin11 4494	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)
Theorem	tfinpw1 4495	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)
Theorem	ncfintfin 4496	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)
Theorem	tfindi 4497	The finite T operation distributes over nonempty 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))
Theorem	tfin0c 4498	The finite T operator is fixed at 0c. (Contributed by SF, 29-Jan-2015.)
⊢ Tfin 0c = 0c
Theorem	tfinsuc 4499	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))
Theorem	tfin1c 4500	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