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	0cnsuc 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
Theorem	peano1 4402	Cardinal zero is a finite cardinal. Theorem X.1.4 of [Rosser] p. 276. (Contributed by SF, 14-Jan-2015.)
⊢ 0c ∈ Nn
Theorem	peano2 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 )
Theorem	peano3 4404	The successor of a finite cardinal is not zero. (Contributed by SF, 14-Jan-2015.)
⊢ (A ∈ Nn → (A +c 1c) ≠ 0c)
Theorem	addcid1 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
Theorem	addccom 4406	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 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
Theorem	1cnnc 4408	Cardinal one is a finite cardinal. Theorem X.1.12 of [Rosser] p. 277. (Contributed by SF, 16-Jan-2015.)
⊢ 1c ∈ Nn
Theorem	peano5 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)
Theorem	findsd 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 ∧ η) → τ)
Theorem	finds 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 → τ)
Theorem	nnc0suc 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)))
Theorem	elsuc 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}))
Theorem	elsuci 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))
Theorem	addcass 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))
Theorem	addc32 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)
Theorem	addc4 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))
Theorem	addc6 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))
Theorem	nncaddccl 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 )
Theorem	elfin 4420*	Membership in the set of finite sets. (Contributed by SF, 19-Jan-2015.)
⊢ (A ∈ Fin ↔ ∃x ∈ Nn A ∈ x)
Theorem	el0c 4421	Membership in cardinal zero. (Contributed by SF, 22-Jan-2015.)
⊢ (A ∈ 0c ↔ A = ∅)
Theorem	nulel0c 4422	The empty set is a member of cardinal zero. (Contributed by SF, 13-Feb-2015.)
⊢ ∅ ∈ 0c
Theorem	0fin 4423	The empty set is finite. (Contributed by SF, 19-Jan-2015.)
⊢ ∅ ∈ Fin
Theorem	nnsucelrlem1 4424*	Lemma for nnsucelr 4428. 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 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)
Theorem	nnsucelrlem3 4426	Lemma for nnsucelr 4428. 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 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)
Theorem	nnsucelr 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)
Theorem	nndisjeq 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 ) → ((M ∩ N) = ∅ ∨ M = N))
Theorem	nnceleq 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)
Theorem	snfi 4431	A singleton is finite. (Contributed by SF, 23-Feb-2015.)
⊢ {A} ∈ Fin
2.2.11  Deriving infinity
Syntax	clefin 4432	Extend class notation to include the less than or equal to relationship for finite cardinals.
class ≤fin
Syntax	cltfin 4433	Extend class notation to include the less than relationship for finite cardinals.
class <fin
Syntax	cncfin 4434	Extend class notation to include the finite cardinal function.
class Ncfin A
Syntax	ctfin 4435	Extend class notation to include the finite T operation.
class Tfin A
Syntax	cevenfin 4436	Extend class notation to include the (temporary) set of all even numbers.
class Evenfin
Syntax	coddfin 4437	Extend class notation to include the (temporary) set of all odd numbers.
class Oddfin
Syntax	wsfin 4438	Extend wff notation to include the finite S relationship.
wff Sfin (A, B)
Syntax	cspfin 4439	Extend class notation to include the finite Sp set.
class Spfin
Definition	df-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 ∣ ∃y∃z(x = ⟪y, z⟫ ∧ ∃w ∈ Nn z = (y +c w))}
Definition	df-ltfin 4441*	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 4442*	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 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)))
Definition	df-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 ≠ ∅)}
Definition	df-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 ≠ ∅)}
Definition	df-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)))
Definition	df-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))}
Theorem	opklefing 4448*	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 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))))
Theorem	lefinaddc 4450	Cardinal sum always yields a larger set. (Contributed by SF, 27-Jan-2015.)
⊢ ((A ∈ V ∧ N ∈ Nn ) → ⟪A, (A +c N)⟫ ∈ ≤fin )
Theorem	prepeano4 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)
Theorem	addcnul1 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 ∅) = ∅
Theorem	addcnnul 4453	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 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)
Theorem	preaddccan2 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))
Theorem	nulge 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 )
Theorem	ltfinirr 4457	Irreflexive law for finite less than. (Contributed by SF, 29-Jan-2015.)
⊢ (A ∈ Nn → ¬ ⟪A, A⟫ ∈ <fin )
Theorem	leltfintr 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, B⟫ ∈ ≤fin ∧ ⟪B, C⟫ ∈ <fin ) → ⟪A, C⟫ ∈ <fin ))
Theorem	ltfintr 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 ))
Theorem	ltfinasym 4460	Asymmetry law for finite less than. (Contributed by SF, 29-Jan-2015.)
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → (⟪A, B⟫ ∈ <fin → ¬ ⟪B, A⟫ ∈ <fin ))
Theorem	0cminle 4461	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 4462	One plus a finite cardinal is strictly greater. (Contributed by SF, 29-Jan-2015.)
⊢ ((A ∈ V ∧ A ≠ ∅) → ⟪A, (A +c 1c)⟫ ∈ <fin )
Theorem	lefinlteq 4463	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 4464	Finite less than is stratified. (Contributed by SF, 29-Jan-2015.)
⊢ <fin ∈ V
Theorem	ltfintrilem1 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
Theorem	ltfintri 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 ))
Theorem	lefinrflx 4467	Less than or equal to is reflexive. (Contributed by SF, 2-Feb-2015.)
⊢ (A ∈ V → ⟪A, A⟫ ∈ ≤fin )
Theorem	ltlefin 4468	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 4469	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 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 )
Theorem	vfinnc 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)
Theorem	ncfinex 4472	The finite cardinality of a set exists. (Contributed by SF, 27-Jan-2015.)
⊢ Ncfin A ∈ V
Theorem	ncfineq 4473	Equality theorem for finite cardinality. (Contributed by SF, 20-Jan-2015.)
⊢ (A = B → Ncfin A = Ncfin B)
Theorem	ncfinprop 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))
Theorem	ncfindi 4475	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 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)
Theorem	ncfineleq 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 B ↔ Ncfin A = Ncfin B))
Theorem	eqpwrelk 4478	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 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 Sk ⊕ Ins2k SIk Sk ) “k ℘1℘1℘11c)) ↔ A = ℘1B)
Theorem	ncfinraiselem2 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
Theorem	ncfinraise 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))
Theorem	ncfinlowerlem1 4482*	Lemma for ncfinlower 4483. 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 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))
Theorem	nnpw1ex 4484*	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 4485	The finite T operator is always a set. (Contributed by SF, 26-Jan-2015.)
⊢ Tfin A ∈ V
Theorem	eqtfinrelk 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 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 4487	The expression at the core of eqtfinrelk 4486 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 4488	Equality theorem for the finite T operator. (Contributed by SF, 24-Jan-2015.)
⊢ (A = B → Tfin A = Tfin B)
Theorem	tfinprop 4489*	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 4490	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 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 ∅ = ∅
Theorem	tfincl 4492	Closure law for finite T operation. (Contributed by SF, 2-Feb-2015.)
⊢ (N ∈ Nn → Tfin N ∈ Nn )
Theorem	tfin11 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)
Theorem	tfinpw1 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)
Theorem	ncfintfin 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)
Theorem	tfindi 4496	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 4497	The finite T operator is fixed at 0c. (Contributed by SF, 29-Jan-2015.)
⊢ Tfin 0c = 0c
Theorem	tfinsuc 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))
Theorem	tfin1c 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
Theorem	tfinltfinlem1 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 ))