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