Statement List for Metamath Proof Explorer - 3401-3500 - Page 35 of 58
| Type | Label | Description |
|---|
| Statement |
|---|
| |
| Theorem | limensuci 3401 |
A limit ordinal is equinumerous to its successor.
|
| ⊢
Lim A
⇒ ⊢ (A ∈ B
→ A ≈ suc A) |
| |
| Theorem | limensuc 3402 |
A limit ordinal is equinumerous to its successor.
|
| ⊢
((A ∈ B ∧ Lim A)
→ A ≈ suc A) |
| |
| Theorem | phplem1 3403 |
Lemma for Pigeonhole Principle. This just says that if we remove an
element of a set then put it back in, we end up with the original set.
|
| ⊢
(B ∈ A → ({B}
∪ (A ∖ {B})) = A) |
| |
| Theorem | phplem2 3404 |
Lemma for Pigeonhole Principle. If we join a natural number to itself
minus an element, we end up with its successor minus the same element.
|
| ⊢
((A ∈ ω ∧ B ∈ A)
→ ({A} ∪ (A ∖ {B}))
= (suc A ∖ {B})) |
| |
| Theorem | phplem3 3405 |
Lemma for Pigeonhole Principle. A natural number is equinumerous to its
successor minus one of its elements.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ ((A ∈ ω ∧ B ∈ A)
→ A ≈ (suc A ∖ {B})) |
| |
| Theorem | phplem4 3406 |
Lemma for Pigeonhole Principle. A natural number is equinumerous
to its successor minus any element of the successor.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ ((A ∈ ω ∧ B ∈ suc A)
→ A ≈ (suc A ∖ {B})) |
| |
| Theorem | phplem5 3407 |
Lemma for Pigeonhole Principle. Equinumerosity of successors implies
equinumerosity of the original natural numbers.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
⇒ ⊢ ((A ∈ ω ∧ B ∈ ω) → (suc A ≈ suc B
→ A ≈ B)) |
| |
| Theorem | nneneq 3408 |
Two equinumerous natural numbers are equal. Proposition 10.20 of
[TakeutiZaring] p. 90 and its
converse. Also compare Corollary 6E of
[Enderton] p. 136.
|
| ⊢
((A ∈ ω ∧ B ∈ ω) → (A ≈ B
↔ A = B)) |
| |
| Theorem | php 3409 |
Pigeonhole Principle. A natural number is not equinumerous to a
proper subset of itself. Theorem (Pigeonhole Principle) of [Enderton]
p. 134. The theorem is so-called because you can't put n + 1
pigeons into n holes (if each hole holds only one pigeon).
The proof consists of lemmas phplem1 3403 through phplem5 3407, nneneq 3408,
and this final piece of the proof.
|
| ⊢
((A ∈ ω ∧ B ⊂ A)
→ ¬ A ≈ B) |
| |
| Theorem | php2 3410 |
Corollary of Pigeonhole Principle.
|
| ⊢
((A ∈ ω ∧ B ⊂ A)
→ B ≺ A) |
| |
| Theorem | php3 3411 |
Corollary of Pigeonhole Principle. If A
is finite and B
is a proper subset of A, the
B is strictly less numerous
than A. Stronger version of
Corollary 6C of [Enderton] p. 135.
(The expression ∃x ∈
ωA ≈ x is the definition
of "finite", and "infinite" is defined as "not
finite".)
|
| ⊢
((∃x ∈ ω A ≈ x
∧ B ⊂ A) → B
≺ A) |
| |
| Theorem | php4 3412 |
Corollary of the Pigeonhole Principle php 3409: a natural number is
strictly dominated by its successor.
|
| ⊢
(A ∈ ω → A ≺ suc A) |
| |
| Theorem | php5 3413 |
Corollary of the Pigeonhole Principle php 3409: a natural number is not
equinumerous to its successor. Corollary 10.21(1) of [TakeutiZaring]
p. 90.
|
| ⊢
(A ∈ ω → ¬
A ≈ suc A) |
| |
| Theorem | onomeneq 3414 |
An ordinal number equinumerous to a natural number is equal to it.
Proposition 10.22 of [TakeutiZaring] p. 90 and its converse.
|
| ⊢
((A ∈ On ∧ B ∈ ω) → (A ≈ B
↔ A = B)) |
| |
| Theorem | onfin 3415 |
An ordinal number is finite iff it is a natural number. Proposition
10.32 of [TakeutiZaring] p. 92.
|
| ⊢
(A ∈ On →
(∃x ∈ ω A ≈ x
↔ A ∈ ω)) |
| |
| Theorem | nndomo 3416 |
Cardinal ordering agrees with natural number ordering. Example 3 of
[Enderton] p. 146.
|
| ⊢
((A ∈ ω ∧ B ∈ ω) → (A ≼ B
↔ A ⊆ B)) |
| |
| Theorem | nnsdomo 3417 |
Cardinal ordering agrees with natural number ordering.
|
| ⊢
((A ∈ ω ∧ B ∈ ω) → (A ≺ B
↔ A ⊂ B)) |
| |
| Theorem | omsucdom 3418 |
Strict dominance of natural numbers is the same as dominance over the
successor of the smaller.
|
| ⊢
((A ∈ ω ∧ B ∈ ω) → (A ≺ B
↔ suc A ≼ B)) |
| |
| Theorem | sucdomi 3419 |
Dominance of a set over a successor of a natural number implies strict
dominance over the number. For the converse, see sucdom 3648.
|
| ⊢
((A ∈ ω ∧ B ∈ C)
→ (suc A ≼ B → A
≺ B)) |
| |
| Theorem | 0sdom1dom 3420 |
Strict dominance over zero is the same as dominance over one.
|
| ⊢
A ∈ V
⇒ ⊢ (∅ ≺
A ↔ 1o ≼
A) |
| |
| Theorem | finsucdom 3421 |
Strict dominance of a finite set over a natural number is the same as
dominance over its successor.
|
| ⊢
((A ∈ ω ∧
∃x ∈ ω B ≈ x)
→ (A ≺ B ↔ suc A
≼ B)) |
| |
| Theorem | pssinf 3422 |
A set equinumerous to a proper subset of itself is infinite. Corollary
6D(a) of [Enderton] p. 136.
|
| ⊢
((A ⊂ B ∧ A
≈ B) → ¬ ∃x ∈ ω B ≈ x) |
| |
| Theorem | ominf 3423 |
The set of natural numbers is infinite. Corollary 6D(b) of [Enderton]
p. 136.
|
| ⊢
¬ ∃x ∈ ω ω
≈ x |
| |
| Theorem | omsdomnn 3424 |
Omega strictly dominates a natural number. Example 3 of [Enderton]
p. 146. Here we use A ≼
ω ∧ ¬ ω ≈ A
instead of A ≺ ω
because, due to a peculiarity ultimately caused our ordered pair
definition, we would need the axiom of infinity (which we have avoided
up to now) in order to prove the latter.
|
| ⊢
(A ∈ ω → (A ≼ ω ∧ ¬ ω ≈
A)) |
| |
| Theorem | isfinite1 3425 |
Omega strictly dominates a finite set. See comment in omsdomnn 3424.
|
| ⊢
(∃x ∈ ω A ≈ x
→ (A ≼ ω ∧ ¬
ω ≈ A)) |
| |
| Theorem | infsdomnn 3426 |
An infinite set strictly dominates a natural number.
|
| ⊢
A ∈ V
⇒ ⊢ ((ω
≼ A ∧ B ∈ ω) → B ≺ A) |
| |
| Theorem | infn0 3427 |
An infinite set is not empty.
|
| ⊢
A ∈ V
⇒ ⊢ (ω ≼
A → ¬ A = ∅) |
| |
| Theorem | pssnn 3428 |
A proper subset of a natural number is equinumerous to some smaller
number. Lemma 6F of [Enderton] p.
137.
|
| ⊢
((A ∈ ω ∧ B ⊂ A)
→ ∃x ∈ A B ≈
x) |
| |
| Theorem | ssnn 3429 |
A subset of a natural number is finite.
|
| ⊢
((A ∈ ω ∧ B ⊆ A)
→ ∃x ∈ ω B ≈ x) |
| |
| Theorem | ssfi 3430 |
A subset of a finite set is finite. Corollary 6G of [Enderton]
p. 138.
|
| ⊢
((∃x ∈ ω A ≈ x
∧ B ⊆ A) → ∃x ∈ ω B ≈ x) |
| |
| Theorem | unblem1 3431 |
Lemma for unbnn 3435. After removing the successor of an element
from an
unbounded set of natural numbers, the intersection of the result belongs
to the original unbounded set.
|
| ⊢
(((B ⊆ ω ∧
∀x ∈ ω ∃y ∈ B
x ∈ y) ∧ A
∈ B) → ∩(B ∖ suc
A) ∈ B) |
| |
| Theorem | unblem2 3432 |
Lemma for unbnn 3435. The value of the function F belongs to
the unbounded set of natural numbers A.
|
| ⊢
(w ∈ F → ∀x w ∈
F)
& ⊢ F = (rec({⟨x, y⟩∣y
= ∩(A ∖
suc x)}, ∩A) ↾
ω) ⇒ ⊢ ((A ⊆
ω ∧ ∀w ∈ ω
∃v ∈ A w ∈
v) → (z ∈ ω → (F ‘z)
∈ A)) |
| |
| Theorem | unblem3 3433 |
Lemma for unbnn 3435. The value of the function F is less than
its value at a successor.
|
| ⊢
(w ∈ F → ∀x w ∈
F)
& ⊢ F = (rec({⟨x, y⟩∣y
= ∩(A ∖
suc x)}, ∩A) ↾
ω) ⇒ ⊢ ((A ⊆
ω ∧ ∀w ∈ ω
∃v ∈ A w ∈
v) → (z ∈ ω → (F ‘z)
∈ (F ‘suc z))) |
| |
| Theorem | unblem4 3434 |
Lemma for unbnn 3435. The function F maps the set of natural
numbers one-to-one to set of unbounded natural numbers A.
|
| ⊢
(w ∈ F → ∀x w ∈
F)
& ⊢ F = (rec({⟨x, y⟩∣y
= ∩(A ∖
suc x)}, ∩A) ↾
ω) ⇒ ⊢ ((A ⊆
ω ∧ ∀w ∈ ω
∃v ∈ A w ∈
v) → F:ω–1-1→A) |
| |
| Theorem | unbnn 3435 |
Any unbounded subset of natural numbers is equinumerous to the set of
all natural numbers. Part of the proof of Theorem 42 of [Suppes]
p. 151.
|
| ⊢
A ∈ V
⇒ ⊢ ((A ⊆ ω ∧ ∀x ∈ ω ∃y ∈ A
x ∈ y) → A
≈ ω) |
| |
| Theorem | unbnn2 3436 |
Version of unbnn 3435 that does not require a strict upper bound.
|
| ⊢
A ∈ V
⇒ ⊢ ((A ⊆ ω ∧ ∀x ∈ ω ∃y ∈ A
x ⊆ y) → A
≈ ω) |
| |
| Theorem | isfinite2 3437 |
Any set strictly dominated by the class of natural numbers is finite.
Sufficiency part of Theorem 42 of [Suppes] p. 151. This theorem does
not require the Axiom of Infinity.
|
| ⊢
(A ≺ ω →
∃x ∈ ω A ≈ x) |
| |
| Theorem | unfilem1 3438 |
Lemma for proving that the union of two finite sets is finite.
|
| ⊢
A ∈ ω
& ⊢ B ∈ ω
& ⊢ F = {⟨x,
y⟩∣(x ∈ B
∧ y = (A +o x))}
⇒ ⊢ ran F = ((A
+o B) ∖ A) |
| |
| Theorem | unfilem2 3439 |
Lemma for proving that the union of two finite sets is finite.
|
| ⊢
A ∈ ω
& ⊢ B ∈ ω
& ⊢ F = {⟨x,
y⟩∣(x ∈ B
∧ y = (A +o x))}
⇒ ⊢ F:B–1-1-onto→((A
+o B) ∖ A) |
| |
| Theorem | unfilem3 3440 |
Lemma for proving that the union of two finite sets is finite.
|
| ⊢
((A ∈ ω ∧ B ∈ ω) → B ≈ ((A
+o B) ∖ A)) |
| |
| Theorem | unfi 3441 |
The union of two finite sets is finite. Part of Corollary 6K of
[Enderton] p. 144.
|
| ⊢
((∃x ∈ ω A ≈ x
∧ ∃x ∈ ω B ≈ x)
→ ∃x ∈ ω (A ∪ B)
≈ x) |
| |
| Theorem | unfi2 3442 |
The union of two finite sets is finite. Part of Corollary 6K of
[Enderton] p. 144.
|
| ⊢
((A ≺ ω ∧ B ≺ ω) → (A ∪ B)
≺ ω) |
| |
| Theorem | infcntss 3443 |
Every infinite set has a denumerable subset. Similar to Exercise 8 of
[TakeutiZaring] p. 91. (However,
we need neither AC nor the Axiom of
Infinity because of the way we express "infinite" in the
antecedent.)
|
| ⊢
A ∈ V
⇒ ⊢ (ω ≼
A → ∃x(x ⊆
A ∧ x ≈ ω)) |
| |
| Theorem | prfi 3444 |
An unordered pair is finite.
|
| ⊢
∃x ∈ ω {A, B} ≈
x |
| |
| Theorem | fiint 3445 |
Equivalent ways of stating the finite intersection property. We show
two ways of saying, "the intersection of elements in every finite
non-empty subcollection of A is in
A". This theorem is
applicable to a topology, which (among other axioms) is closed under
finite intersections. Some texts use the left-hand version of this
axiom and others the right-hand version, but as our proof here shows,
their "intuitively obvious" equivalence can be non-trivial to
establish
formally.
|
| ⊢
(∀x ∈ A ∀y
∈ A (x ∩ y)
∈ A ↔ ∀x(((x ⊆
A ∧ ¬ x = ∅) ∧ ∃y ∈ ω x ≈ y)
→ ∩x
∈ A)) |
| |
| Theorem | zfregcl 3446 |
The Axiom of Regularity with class variables.
|
| ⊢
A ∈ V
⇒ ⊢ (∃x x ∈
A → ∃x ∈ A
∀y ∈ x ¬ y
∈ A) |
| |
| Theorem | zfreg 3447 |
The Axiom of Regularity using abbreviations. Axiom 6 of [TakeutiZaring]
p. 21. This is called the 'weak form'; there is also a
'strong form', not requiring that A
be a set, that can be proved
with more difficulty (see zfregs 3491).
|
| ⊢
A ∈ V
⇒ ⊢ (¬ A = ∅ → ∃x ∈ A
(x ∩ A) = ∅) |
| |
| Theorem | zfreg2 3448 |
The Axiom of Regularity using abbreviations. This form with the
intersection arguments commuted (compared to zfreg 3447) is formally
more convenient for us in some cases. Axiom Reg of [BellMachover]
p. 480.
|
| ⊢
A ∈ V
⇒ ⊢ (¬ A = ∅ → ∃x ∈ A
(A ∩ x) = ∅) |
| |
| Theorem | eirrv 3449 |
The membership relation is irreflexive: no set is a member of itself.
Theorem 105 of [Suppes] p. 54. (This is
trivial to prove from zfregfr 3452
and efrirr 2180, but this proof is direct from the Axiom of
Regularity.)
|
| ⊢
¬ x ∈ x |
| |
| Theorem | eirr 3450 |
No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22.
|
| ⊢
¬ A ∈ A |
| |
| Theorem | sucprcreg 3451 |
A class is equal to its successor iff it is a proper class (assuming the
Axiom of Regularity).
|
| ⊢
(¬ A ∈ V ↔ suc
A = A) |
| |
| Theorem | zfregfr 3452 |
The epsilon relation is founded on any class.
|
| ⊢
E Fr A |
| |
| Theorem | en2lp 3453 |
No class has 2-cycle membership loops. Theorem 7X(b) of [Enderton]
p. 206.
|
| ⊢
¬ (A ∈ B ∧ B
∈ A) |
| |
| Theorem | preleq 3454 |
Equality of two unordered pairs when one member of each pair contains
the other member.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
⇒ ⊢ (((A ∈ B
∧ C ∈ D) ∧ {A,
B} = {C, D}) →
(A = C
∧ B = D)) |
| |
| Theorem | opthreg 3455 |
Theorem for alternate representation of ordered pairs, requiring
Regularity. Exercise 34 of [Enderton]
p. 207.
|
| ⊢
A ∈ V
& ⊢ B ∈ V
& ⊢ C ∈ V
& ⊢ D ∈ V
⇒ ⊢ ({A, {A, B}} = {C,
{C, D}} → (A =
C ∧ B = D)) |
| |
| Theorem | suc11reg 3456 |
The successor operation behaves like a one-to-one function (assuming the
Axiom of Regularity). Exercise 35 of [Enderton] p. 208 and its
converse.
|
| ⊢
(suc A = suc B ↔ A =
B) |
| |
| Theorem | inf0 3457 |
Our Axiom of Infinity derived from existence of omega. The proof shows
that the especially contrived class
"ran (rec({⟨w, v⟩∣v
= suc w}, y) ↾ ω)" exists,
is a subset of its union, and contains a given set y (and thus is
non-empty). Thus it provides an example demonstrating that a set
x
exists with the necessary properties demanded by ax-inf 1079.
|
| ⊢
ω ∈ V
⇒ ⊢ ∃x(y ∈
x ∧ ∀y(y ∈
x → ∃z(y ∈
z ∧ z ∈ x))) |
| |
| Theorem | inf1 3458 |
Variation of Axiom of Infinity (using axinf 1084 as a hypothesis). Axiom
of Infinity of [FreydScedrov] p.
283.
|
| ⊢
∃x(y ∈ x
∧ ∀y(y ∈ x
→ ∃z(y ∈ z
∧ z ∈ x)))
⇒ ⊢ ∃x(¬ x =
∅ ∧ ∀y(y ∈ x
→ ∃z(y ∈ z
∧ z ∈ x))) |
| |
| Theorem | inf2 3459 |
Variation of Axiom of Infinity. There exists a non-empty set that is a
subset of its union (using axinf 1084 as a hypothesis).
|
| ⊢
∃x(y ∈ x
∧ ∀y(y ∈ x
→ ∃z(y ∈ z
∧ z ∈ x)))
⇒ ⊢ ∃x(¬ x =
∅ ∧ x ⊆ ∪x) |
| |
| Theorem | inf3lema 3460 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ (A ∈
(G ‘B) ↔ (A
∈ x ∧ (A ∩ x)
⊆ B)) |
| |
| Theorem | inf3lemb 3461 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ (F
‘∅) = ∅ |
| |
| Theorem | inf3lemc 3462 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ (A ∈
ω → (F ‘suc A) = (G
‘(F ‘A))) |
| |
| Theorem | inf3lemd 3463 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ (A ∈
ω → (F ‘A) ⊆ x) |
| |
| Theorem | inf3lem1 3464 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ (A ∈
ω → (F ‘A) ⊆ (F
‘suc A)) |
| |
| Theorem | inf3lem2 3465 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ ((¬ x =
∅ ∧ x ⊆ ∪x) → (A ∈ ω → ¬ (F ‘A) =
x)) |
| |
| Theorem | inf3lem3 3466 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description. In the proof, we
invoke the Axiom of
Regularity in the form of zfreg 3447.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ ((¬ x =
∅ ∧ x ⊆ ∪x) → (A ∈ ω → ¬ (F ‘A) =
(F ‘suc A))) |
| |
| Theorem | inf3lem4 3467 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ ((¬ x =
∅ ∧ x ⊆ ∪x) → (A ∈ ω → (F ‘A)
⊂ (F ‘suc A))) |
| |
| Theorem | inf3lem5 3468 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ ((¬ x =
∅ ∧ x ⊆ ∪x) → ((A ∈ ω ∧ B ∈ A)
→ (F ‘B) ⊂ (F
‘A))) |
| |
| Theorem | inf3lem6 3469 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ ((¬ x =
∅ ∧ x ⊆ ∪x) → F:ω–1-1→℘x) |
| |
| Theorem | inf3lem7 3470 |
Lemma for our Axiom of Infinity => standard Axiom of Infinity. See
inf3 3471 for detailed description. In the proof, we
invoke the Axiom of
Replacement in the form of funrnex 2743.
|
| ⊢
G = {⟨y, z⟩∣z
= {w ∈ x∣(w
∩ x) ⊆ y}} & ⊢ F =
(rec(G, ∅) ↾
ω) & ⊢ A ∈
V & ⊢ B ∈
V ⇒ ⊢ ((¬ x =
∅ ∧ x ⊆ ∪x) → ω
∈ V) |
| |
| Theorem | inf3 3471 |
Our Axiom of Infinity ax-inf 1079 implies the standard Axiom of Infinity.
The hypothesis is a variant of our Axiom of Infinity provided by
inf2 3459, and the conclusion is the version of the
Axiom of Infinity
shown as Axiom 7 in [TakeutiZaring] p. 43. (Other standard
versions are
proved later as inf4 3473 and zfinf 3474.) The main proof is provided by
inf3lema 3460 through inf3lem7 3470, and this final piece eliminates the
auxiliary hypothesis of inf3lem7 3470. This proof is due to
Ian Sutherland, Richard Heck, and Norman Megill and was posted
on Usenet as shown below. Although the result is not new, the authors
were unable to find a published proof.
(As posted to sci.logic on 30-Oct-96, with annotations added.)
Theorem: The statement "There exists a non-empty set that is a subset
of its union" implies the Axiom of Infinity.
Proof: Let X be a nonempty set which is a subset of its union; the latter
property is equivalent to saying that for any y in X, there exists a z in X
such that y is in z.
Define by finite recursion a function F:omega-->(power X) such that
F_0 = 0 (See inf3lemb 3461.)
F_n+1 = {y<X | y^X subset F_n} (See inf3lemc 3462.)
Note: ^ means intersect, < means \in ("element of").
(Finite recursion as typically done requires the existence of omega;
to avoid this we can just use transfinite recursion restricted to omega.
F is a class-term that is not necessarily a set at this point.)
Lemma 1. F_n subset F_n+1. (See inf3lem1 3464.)
Proof: By induction: F_0 subset F_1. If y < F_n+1, then y^X subset F_n,
so if F_n subset F_n+1, then y^X subset F_n+1, so y < F_n+2.
Lemma 2. F_n =/= X. (See inf3lem2 3465.)
Proof: By induction: F_0 =/= X because X is not empty. Assume F_n =/= X.
Then there is a y in X that is not in F_n. By definition of X, there is a
z in X that contains y. Suppose F_n+1 = X. Then z is in F_n+1, and z^X
contains y, so z^X is not a subset of F_n, contrary to the definition of
F_n+1.
Lemma 3. F_n =/= F_n+1. (See inf3lem3 3466.)
Proof: Using the identity y^X subset F_n <-> y^(X-F_n) = 0, we have
F_n+1 = {y<X | y^(X-F_n) = 0}. Let q = {y<X-F_n | y^(X-F_n) = 0}.
Then q subset F_n+1. Since X-F_n is not empty by Lemma 2 and q is the
set of \in-minimal elements of X-F_n, by Foundation q is not empty, so q
and therefore F_n+1 have an element not in F_n.
Lemma 4. F_n proper_subset F_n+1. (See inf3lem4 3467.)
Proof: Lemmas 1 and 3.
Lemma 5. F_m proper_subset F_n, m < n. (See inf3lem5 3468.)
Proof: Fix m and use induction on n > m. Basis: F_m proper_subset F_m+1
by Lemma 4. Induction: Assume F_m proper_subset F_n. Then since F_n
proper_subset F_n+1, F_m proper_subset F_n+1 by transitivity of proper
subset.
By Lemma 5, F_m =/= F_n for m =/= n, so F is 1-1. (See inf3lem6 3469.)
Thus the inverse of F is a function with range omega and domain a subset
of power X, so omega exists by Replacement. (See inf3lem7 3470.)
Q.E.D.
|
|
| ⊢
∃x(¬ x = ∅ ∧ x ⊆ ∪x) ⇒ ⊢ ω ∈ V |
| |
| Theorem | inf5 3472 |
The statement "there exists a set that is the proper subset of its
union" is equivalent to the Axiom of Infinity (shown on the
right-hand
side in the form of omex 3475.) This provides us with a very short way to
express of the Axiom of Infinity using only simple defined symbols. The
proof does not depend on the Axiom of Infinity.
|
| ⊢
(∃x x ⊂ ∪x ↔ ω ∈ V) |
| |
| Theorem | inf4 3473 |
A standard version of axiom of infinity, expanded to primitives. In
English, it says: there exists a set that contains the empty set and
the successors of all of its members. See zfinf 3474 to see it converted
to abbreviations.
|
| ⊢
∃x(∃y(y ∈
x ∧ ∀z ¬ z
∈ y) ∧ ∀y(y ∈
x → ∃z(z ∈
x ∧ ∀w(w ∈
z ↔ (w ∈ y ∨
w = y))))) |
| |
| Theorem | zfinf 3474 |
A standard version of the axiom of infinity, using definitions to
abbreviate.
|
| ⊢
∃x(∅ ∈ x ∧ ∀y ∈ x suc
y ∈ x) |
| |
| Theorem | omex 3475 |
The existence of omega (the class of natural numbers). Axiom 7 of
[TakeutiZaring] p. 43. This
theorem is proved assuming the Axiom of
Infinity and in fact is equivalent to it. A finitist (someone who
doesn't believe in infinity) could, without contradiction, omit the
axiom of Infinity and instead deny it; this would lead to ω = On
(the proper class of ordinals) by omon 2384
and onprc 2240. The finitist
could still develop natural number, integer, and rational number
arithmetic but would be denied the real numbers (as well as much of the
rest of mathematics). In deference to the finitist, much of our
development is done, when possible, without invoking the Axiom of
Infinity; an example is Peano's axioms peano1 2390 through peano5 2394
(which many textbooks prove more easily assuming Infinity).
The mathematics used by computers is essentially finitist; for example,
computers cannot work directly with real numbers but only
approximations of them in the form of floating-point numbers.
|
| ⊢
ω ∈ V |
| |
| Theorem | omelon 3476 |
Omega is an ordinal number.
|
| ⊢
ω ∈ On |
| |
| Theorem | dfom3 3477 |
The class of natural numbers omega can be defined as the smallest
"inductive set," which is valid provided we assume the Axiom
of
Infinity. Definition 6.3 of [Eisenberg] p. 82.
|
| ⊢
ω = ∩{x∣(∅ ∈ x ∧ ∀y ∈ x suc
y ∈ x)} |
| |
| Theorem | elom3 3478 |
A simplification of elom 2375 assuming the Axiom of Infinity.
|
| ⊢
(A ∈ ω ↔
∀x(Lim x → A
∈ x)) |
| |
| Theorem | dfom4 3479 |
A simplification of df-om 2373 assuming the Axiom of Infinity.
|
| ⊢
ω = {x∣∀y(Lim y →
x ∈ y)} |
| |
| Theorem | isfinite 3480 |
A set is strictly dominated by the class of natural numbers iff it is
finite. Theorem 42 of [Suppes] p. 151.
This theorem provides two
equivalent ways to express "A
is finite". The Axiom of Infinity
is used for the reverse implication.
|
| ⊢
(A ≺ ω ↔
∃x ∈ ω A ≈ x) |
| |
| Theorem | nnsdom 3481 |
A natural number is strictly dominated by the set of natural numbers.
|
| ⊢
(A ∈ ω → A ≺ ω) |
| |
| Theorem | omenps 3482 |
Omega is equinumerous to a proper subset of itself. Example 13.2(4) of
[Eisenberg] p. 216.
|
| ⊢
ω ≈ (ω ∖ {∅}) |
| |
| Theorem | omensuc 3483 |
The set of natural numbers is equinumerous to its successor.
|
| ⊢
ω ≈ suc ω |
| |
| Theorem | infensuc 3484 |
Any infinite ordinal is equinumerous to its successor. Exercise 7 of
[TakeutiZaring] p. 88.
|
| ⊢
((A ∈ On ∧ ω ⊆
A) → A ≈ suc A) |
| |
| Syntax | cr1 3485 |
Extend class definition to include the cumulative hierarchy of sets
function.
|
| class
R1 |
| |
| Syntax | crnk 3486 |
Extend class definition to include rank function.
|
| class
rank |
| |
| Definition | df-r1 3487 |
Define the cumulative hierarchy of sets function, using Takeuti and
Zaring's notation (R1). Starting with the empty set,
this
function builds up layers of sets where the next layer is the power
set of the previous layer (and the union of previous layers when the
argument is a limit ordinal). Using the Axiom of Regularity, we can
show that any set whatsoever belongs to one of the layers of this
hierarchy (see tz9.13 3507). Our definition expresses Definition 9.9
of [TakeutiZaring] p. 76 in a
closed form, from which we derive the
recursive definition as theorems r10 3495, r1suc 3496, and r1lim 3497.
Theorem r1val1 3502 shows a recursive definition that works for
all values,
and theorems r1val2 3522 and r1val3 3523 show the value expressed in terms of
rank. Other notations for this function are R with the argument
as a subscript (Equation 3.1 of [BellMachover] p. 477), V with a
a subscript (Definition of [Enderton]
p. 202), M with a subscript
(Definition 15.19 of [Monk1] p. 113), and
the capital Greek letter
psi (Definition of [Mendelson] p.
281).
|
| ⊢
R1 = rec({⟨x, y⟩∣y
= ℘x}, ∅) |
| |
| Definition | df-rank 3488 |
Define the rank function. See rankval 3512, rankval2 3514, or rankval3 3525
its value. The rank is a kind of "inverse" of the cumulative
hierarchy
of sets function R1: given a set, it returns an
ordinal number
telling us the smallest layer of the hierarchy to which the set belongs.
Based on Definition 9.14 of [TakeutiZaring] p. 79. Theorem rankid 3516
illustrates the "inverse" concept. Another nice theorem
showing the
relationship is rankr1a 3521.
|
| ⊢
rank = {⟨x, y⟩∣y
= ∩{z ∈
On∣x ∈ (R1
‘suc z)}} |
| |
| Theorem | trcl 3489 |
For any set A, show the properties of its
transitive closure
C. Similar to Theorem 9.1 of [TakeutiZaring] p. 73 except that we
show an explicit expression for the transitive closure rather than just
its existence. See tz9.1 3490 for an abbreviated version showing
existence.
|
| ⊢
A ∈ V
& ⊢ F = (rec({⟨z, w⟩∣w
= (z ∪ ∪z)}, A) ↾ ω)
& ⊢ C = ∪y ∈ ω (F ‘y) ⇒ ⊢ (A ⊆
C ∧ Tr C ∧ ∀x((A ⊆
x ∧ Tr x) → C
⊆ x)) |
| |
| Theorem | tz9.1 3490 |
Every set has a transitive closure (smallest transitive extension).
Theorem 9.1 of [TakeutiZaring] p.
73. See trcl 3489 for an explicit
expression for the transitive closure.
|
| ⊢
A ∈ V
⇒ ⊢ ∃x(A ⊆
x ∧ Tr x ∧ ∀y((A ⊆
y ∧ Tr y) → x
⊆ y)) |
| |
| Theorem | zfregs 3491 |
The strong form of the Axiom of Regularity, which does not require
that A be a set. Axiom 6' of [TakeutiZaring] p. 21. The proof
makes use of a special case of Proposition 9.4 of [TakeutiZaring]
p. 75.
|
| ⊢
(¬ A = ∅ →
∃x ∈ A (x ∩
A) = ∅) |
| |
| Theorem | setind 3492 |
Set (epsilon) induction. Theorem 5.22 of [TakeutiZaring] p. 21.
|
| ⊢
(∀x(x ⊆ A
→ x ∈ A) → A =
V) |
| |
| Theorem | setind2 3493 |
Set (epsilon) induction, stated compactly. Given as a homework problem
in 1992 by George Boolos (1940-1996).
|
| ⊢
(℘A ⊆ A → A =
V) |
| |
| Theorem | r1fnon 3494 |
The cumulative hierarchy of sets function is a function on the class of
ordinal numbers.
|
| ⊢
R1 Fn On |
| |
| Theorem | r10 3495 |
Value of the cumulative hierarchy of sets function at ∅.
Part of Definition 9.9 of [TakeutiZaring] p. 76.
|
| ⊢
(R1 ‘∅) = ∅ |
| |
| Theorem | r1suc 3496 |
Value of the cumulative hierarchy of sets function at a successor
ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76.
|
| ⊢
(A ∈ On →
(R1 ‘suc A) =
℘(R1 ‘A)) |
| |
| Theorem | r1lim 3497 |
Value of the cumulative hierarchy of sets function at a limit
ordinal. Part of Definition 9.9 of [TakeutiZaring] p. 76.
|
| ⊢
((A ∈ B ∧ Lim A)
→ (R1 ‘A) =
∪x ∈
A (R1 ‘x)) |
| |
| Theorem | r1tr 3498 |
The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton]
p. 202.
|
| ⊢
Tr (R1 ‘A) |
| |
| Theorem | r1ord 3499 |
Ordering relation for the cumulative hierarchy of sets. Part of
Proposition 9.10(2) of [TakeutiZaring] p. 77.
|
| ⊢
(B ∈ On → (A ∈ B
→ (R1 ‘A)
∈ (R1 ‘B))) |
| |
| Theorem | r1ord2 3500 |
Ordering relation for the cumulative hierarchy of sets. Part of
Proposition 9.10(2) of [TakeutiZaring] p. 77.
|
| ⊢
(B ∈ On → (A ∈ B
→ (R1 ‘A)
⊆ (R1 ‘B))) |
Home
Hilbert Space Explorer
(4958-5787)