Theorem List for New Foundations Explorer - 6201-6300 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | ncpw1pwneg 6201 |
The cardinality of a unit power class is not equal to the cardinality of
the power class. Theorem XI.2.4 of [Rosser] p. 372. (Contributed by
SF, 10-Mar-2015.)
|
⊢ (A ∈ V →
Nc ℘1A ≠ Nc ℘A) |
|
Theorem | ltcpw1pwg 6202 |
The cardinality of a unit power class is strictly less than the
cardinality of the power class. Theorem XI.2.17 of [Rosser] p. 376.
(Contributed by SF, 10-Mar-2015.)
|
⊢ (A ∈ V →
Nc ℘1A <c Nc
℘A) |
|
Theorem | sbthlem1 6203 |
Lemma for sbth 6206. Set up similarity with a range. Theorem
XI.1.14 of
[Rosser] p. 350. (Contributed by SF,
11-Mar-2015.)
|
⊢ R ∈ V
& ⊢ X ∈ V
& ⊢ G = Clos1 ((X ∖ ran R),
R)
& ⊢ A =
(X ∩ G)
& ⊢ B =
(X ∖
G)
& ⊢ C = (ran
R ∩ G)
& ⊢ D = (ran
R ∖
G) ⇒ ⊢ (((Fun R
∧ Fun ◡R)
∧ (X
⊆ dom R
∧ ran R
⊆ X))
→ ran R ≈ X) |
|
Theorem | sbthlem2 6204 |
Lemma for sbth 6206. Eliminate hypotheses from sbthlem1 6203. Theorem
XI.1.14 of [Rosser] p. 350. (Contributed
by SF, 10-Mar-2015.)
|
⊢ R ∈ V ⇒ ⊢ (((Fun R
∧ Fun ◡R)
∧ (B
∈ V
∧ B ⊆ dom R ∧ ran R ⊆ B)) →
ran R ≈ B) |
|
Theorem | sbthlem3 6205 |
Lemma for sbth 6206. If A is equinumerous with a subset of B and
vice-versa, then A is
equinumerous with B. Theorem
XI.1.15 of
[Rosser] p. 353. (Contributed by SF,
10-Mar-2015.)
|
⊢ (((A
≈ C ∧ C ⊆ B) ∧ (B ≈
D ∧
D ⊆
A)) → A ≈ B) |
|
Theorem | sbth 6206 |
The Schroder-Bernstein Theorem. This theorem gives the antisymmetry law
for cardinal less than or equal. Translated out, it means that, if
A is no larger than
B and B is no larger than A, then
Nc A = Nc B. Theorem XI.2.20 of [Rosser] p. 376. (Contributed by
SF, 11-Mar-2015.)
|
⊢ ((A ∈ NC ∧ B ∈ NC ) →
((A ≤c B ∧ B ≤c A) → A =
B)) |
|
Theorem | ltlenlec 6207 |
Cardinal less than is equivalent to one-way cardinal less than or equal.
Theorem XI.2.21 of [Rosser] p. 377.
(Contributed by SF, 11-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ NC ) →
(M <c N ↔ (M
≤c N ∧ ¬ N
≤c M))) |
|
Theorem | addlec 6208 |
For non-empty sets, cardinal sum always increases cardinal less than or
equal. Theorem XI.2.19 of [Rosser] p.
376. (Contributed by SF,
11-Mar-2015.)
|
⊢ ((M ∈ V ∧ N ∈ W ∧ (M
+c N) ≠ ∅) → M
≤c (M +c
N)) |
|
Theorem | addlecncs 6209 |
For cardinals, cardinal sum always increases cardinal less than or
equal. Corollary of theorem XI.2.19 of [Rosser] p. 376. (Contributed
by SF, 11-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ NC ) →
M ≤c (M +c N)) |
|
Theorem | dflec2 6210* |
Cardinal less than or equal in terms of cardinal addition. Theorem
XI.2.22 of [Rosser] p. 377. (Contributed
by SF, 11-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ NC ) →
(M ≤c N ↔ ∃p ∈ NC N = (M
+c p))) |
|
Theorem | lectr 6211 |
Cardinal less than or equal is transitive. (Contributed by SF,
12-Mar-2015.)
|
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) →
((A ≤c B ∧ B ≤c C) → A
≤c C)) |
|
Theorem | leltctr 6212 |
Transitivity law for cardinal less than or equal and less than.
(Contributed by SF, 16-Mar-2015.)
|
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) →
((A ≤c B ∧ B <c C) → A
<c C)) |
|
Theorem | lecponc 6213 |
Cardinal less than or equal partially orders the cardinals.
(Contributed by SF, 12-Mar-2015.)
|
⊢ ≤c Po NC |
|
Theorem | leaddc1 6214 |
Addition law for cardinal less than. Theorem XI.2.23 of [Rosser]
p. 377. (Contributed by SF, 12-Mar-2015.)
|
⊢ (((M ∈ NC ∧ N ∈ NC ∧ P ∈ NC ) ∧ M
≤c N) → (M +c P) ≤c (N +c P)) |
|
Theorem | leaddc2 6215 |
Addition law for cardinal less than. Theorem XI.2.23 of [Rosser] p. 377.
(Contributed by SF, 12-Mar-2015.)
|
⊢ (((M ∈ NC ∧ N ∈ NC ∧ P ∈ NC ) ∧ N
≤c P) → (M +c N) ≤c (M +c P)) |
|
Theorem | nc0le1 6216 |
Any cardinal is either zero or no greater than one. Theorem XI.2.24 of
[Rosser] p. 377. (Contributed by SF,
12-Mar-2015.)
|
⊢ (N ∈ NC → (N = 0c
∨ 1c ≤c N)) |
|
Theorem | nc0suc 6217* |
Any cardinal is either zero or the successor of a cardinal. Corollary
of theorem XI.2.24 of [Rosser] p. 377.
(Contributed by SF,
12-Mar-2015.)
|
⊢ (N ∈ NC → (N = 0c
∨ ∃m ∈ NC N = (m +c
1c))) |
|
Theorem | leconnnc 6218 |
Cardinal less than or equal is total over the naturals. (Contributed by
SF, 12-Mar-2015.)
|
⊢ ((A ∈ Nn ∧ B ∈ Nn ) →
(A ≤c B ∨ B ≤c A)) |
|
Theorem | addceq0 6219 |
The sum of two cardinals is zero iff both addends are zero.
(Contributed by SF, 12-Mar-2015.)
|
⊢ ((A ∈ NC ∧ B ∈ NC ) →
((A +c B) = 0c ↔ (A = 0c ∧ B =
0c))) |
|
Theorem | ce2lt 6220 |
Ordering law for cardinal exponentiation to two. Theorem XI.2.71 of
[Rosser] p. 390. (Contributed by SF,
13-Mar-2015.)
|
⊢ ((M ∈ NC ∧ (M
↑c 0c) ∈ NC ) →
M <c (2c
↑c M)) |
|
Theorem | dflec3 6221* |
Another potential definition of cardinal inequality. (Contributed by
SF, 23-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ NC ) →
(M ≤c N ↔ ∃a ∈ M ∃b ∈ N ∃f f:a–1-1→b)) |
|
Theorem | nclenc 6222* |
Comparison rule for cardinalities. (Contributed by SF, 24-Mar-2015.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ ( Nc A ≤c Nc
B ↔ ∃f f:A–1-1→B) |
|
Theorem | lenc 6223* |
Less than or equal condition for the cardinality of a number.
(Contributed by SF, 18-Mar-2015.)
|
⊢ A ∈ V ⇒ ⊢ (M ∈ NC → (M ≤c Nc
A ↔ ∃x ∈ M x ⊆ A)) |
|
Theorem | tcnc 6224 |
Compute the T-raising of a cardinality. (Contributed by SF,
4-Mar-2015.)
|
⊢ A ∈ V ⇒ ⊢ Tc
Nc A = Nc ℘1A |
|
Theorem | tcncv 6225 |
Compute the T-raising of the cardinality of the universe. Part of Theorem
5.2 of [Specker] p. 973. (Contributed by
SF, 4-Mar-2015.)
|
⊢ Tc
Nc V = Nc
1c |
|
Theorem | tcnc1c 6226 |
Compute the T-raising of the cardinality of one. Part of Theorem 5.2 of
[Specker] p. 973. (Contributed by SF,
4-Mar-2015.)
|
⊢ Tc
Nc 1c = Nc ℘11c |
|
Theorem | tc11 6227 |
Cardinal T is one-to-one. Based on theorem 2.4 of [Specker] p. 972.
(Contributed by SF, 10-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ NC ) → ( Tc M =
Tc N ↔ M =
N)) |
|
Theorem | taddc 6228* |
T raising rule for cardinal sum. (Contributed by SF, 11-Mar-2015.)
|
⊢ (((A ∈ NC ∧ B ∈ NC ∧ X ∈ NC ) ∧ Tc
A = ( Tc B
+c X)) → ∃c ∈ NC X = Tc
c) |
|
Theorem | tlecg 6229 |
T-raising perserves order for cardinals. Theorem 5.5 of [Specker]
p. 973. (Contributed by SF, 11-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ NC ) →
(M ≤c N ↔ Tc
M ≤c Tc N)) |
|
Theorem | letc 6230* |
If a cardinal is less than or equal to a T-raising, then it is also a
T-raising. Theorem 5.6 of [Specker] p.
973. (Contributed by SF,
11-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ NC ∧ M
≤c Tc N) → ∃p ∈ NC M = Tc
p) |
|
Theorem | ce0t 6231* |
If (M ↑c
0c) is a cardinal, then M is a T-raising of some
cardinal. (Contributed by SF, 17-Mar-2015.)
|
⊢ ((M ∈ NC ∧ (M
↑c 0c) ∈ NC ) → ∃n ∈ NC M = Tc
n) |
|
Theorem | ce2le 6232 |
Partial ordering law for base two cardinal exponentiation. Theorem 4.8
of [Specker] p. 973. (Contributed by
SF, 16-Mar-2015.)
|
⊢ (((M ∈ NC ∧ N ∈ NC ∧ (N
↑c 0c) ∈ NC ) ∧ M
≤c N) →
(2c ↑c M) ≤c (2c
↑c N)) |
|
Theorem | cet 6233 |
The exponent of a T-raising to a T-raising is always a cardinal.
(Contributed by SF, 13-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ NC ) → ( Tc M
↑c Tc N) ∈ NC ) |
|
Theorem | ce2t 6234 |
The exponent of two to a T-raising is always a cardinal. Theorem 5.8 of
[Specker] p. 973. (Contributed by SF,
13-Mar-2015.)
|
⊢ (M ∈ NC →
(2c ↑c Tc M)
∈ NC
) |
|
Theorem | tce2 6235 |
Distributive law for T-raising and cardinal exponentiation to two.
(Contributed by SF, 13-Mar-2015.)
|
⊢ ((M ∈ NC ∧ (M
↑c 0c) ∈ NC ) → Tc (2c
↑c M) =
(2c ↑c Tc M)) |
|
Theorem | te0c 6236 |
A T-raising raised to zero is always a cardinal. (Contributed by SF,
16-Mar-2015.)
|
⊢ (M ∈ NC → ( Tc M
↑c 0c) ∈ NC
) |
|
Theorem | ce0tb 6237* |
(M ↑c
0c) is a cardinal iff M is a T-raising of some
cardinal. (Contributed by SF, 17-Mar-2015.)
|
⊢ (M ∈ NC →
((M ↑c
0c) ∈ NC ↔ ∃n ∈ NC M = Tc n)) |
|
Theorem | ce0lenc1 6238 |
Cardinal exponentiation to zero is a cardinal iff the number is less
than the size of cardinal one. (Contributed by SF, 18-Mar-2015.)
|
⊢ (M ∈ NC →
((M ↑c
0c) ∈ NC ↔ M
≤c Nc
1c)) |
|
Theorem | tlenc1c 6239 |
A T-raising is less than or equal to the cardinality of cardinal one.
(Contributed by SF, 16-Mar-2015.)
|
⊢ (M ∈ NC → Tc M
≤c Nc
1c) |
|
Theorem | 1ne0c 6240 |
Cardinal one is not zero. (Contributed by SF, 4-Mar-2015.)
|
⊢ 1c ≠
0c |
|
Theorem | 2ne0c 6241 |
Cardinal two is not zero. (Contributed by SF, 4-Mar-2015.)
|
⊢ 2c ≠
0c |
|
Theorem | finnc 6242 |
A set is finite iff its cardinality is a natural. (Contributed by SF,
18-Mar-2015.)
|
⊢ (A ∈ Fin ↔ Nc A ∈ Nn
) |
|
Theorem | tcfnex 6243 |
The stratified T raising function is a set. (Contributed by SF,
18-Mar-2015.)
|
⊢ TcFn ∈
V |
|
Theorem | fntcfn 6244 |
Functionhood statement for the stratified T-raising function.
(Contributed by SF, 18-Mar-2015.)
|
⊢ TcFn Fn 1c |
|
Theorem | brtcfn 6245 |
Binary relationship form of the stratified T-raising function.
(Contributed by SF, 18-Mar-2015.)
|
⊢ A ∈ V ⇒ ⊢ ({A}TcFnB ↔
B = Tc A) |
|
Theorem | ncfin 6246 |
The cardinality of a set is a natural iff the set is finite.
(Contributed by SF, 19-Mar-2015.)
|
⊢ A ∈ V ⇒ ⊢ ( Nc A ∈ Nn ↔ A ∈ Fin
) |
|
Theorem | nclennlem1 6247* |
Lemma for nclenn 6248. Set up stratification for induction.
(Contributed
by SF, 19-Mar-2015.)
|
⊢ {x ∣ ∀n ∈ NC (n
≤c x → n ∈ Nn )} ∈
V |
|
Theorem | nclenn 6248 |
A cardinal that is less than or equal to a natural is a natural.
Theorem XI.3.3 of [Rosser] p. 391.
(Contributed by SF, 19-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ Nn ∧ M
≤c N) → M ∈ Nn ) |
|
Theorem | addcdi 6249 |
Distributivity law for cardinal addition and multiplication. Theorem
XI.2.31 of [Rosser] p. 379. (Contributed
by Scott Fenton,
31-Jul-2019.)
|
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) →
(A ·c (B +c C)) = ((A
·c B)
+c (A
·c C))) |
|
Theorem | addcdir 6250 |
Distributivity law for cardinal addition and multiplication. Theorem
XI.2.30 of [Rosser] p. 379. (Contributed
by Scott Fenton,
31-Jul-2019.)
|
⊢ ((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) →
((A +c B) ·c C) = ((A
·c C)
+c (B
·c C))) |
|
Theorem | muc0or 6251 |
The cardinal product of two cardinal numbers is zero iff one of the
numbers is zero. Biconditional form of theorem XI.2.34 of [Rosser]
p. 380. (Contributed by Scott Fenton, 31-Jul-2019.)
|
⊢ ((A ∈ NC ∧ B ∈ NC ) →
((A ·c B) = 0c ↔ (A = 0c
∨ B =
0c))) |
|
Theorem | lemuc1 6252 |
Multiplication law for cardinal less than. Theorem XI.2.35 of [Rosser]
p. 380. (Contributed by Scott Fenton, 31-Jul-2019.)
|
⊢ (((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) ∧ A
≤c B) → (A ·c C) ≤c (B ·c C)) |
|
Theorem | lemuc2 6253 |
Multiplication law for cardinal less than. (Contributed by Scott Fenton,
31-Jul-2019.)
|
⊢ (((A ∈ NC ∧ B ∈ NC ∧ C ∈ NC ) ∧ B
≤c C) → (A ·c B) ≤c (A ·c C)) |
|
Theorem | ncslemuc 6254 |
A cardinal is less than or equal to its product with another. Theorem
XI.2.36 of [Rosser] p. 381. (Contributed
by Scott Fenton,
31-Jul-2019.)
|
⊢ ((M ∈ NC ∧ N ∈ NC ∧ N ≠
0c) → M
≤c (M
·c N)) |
|
Theorem | ncvsq 6255 |
The product of the cardinality of V squared is just the
cardinality
of V. Theorem XI.2.37 of [Rosser] p. 381. (Contributed by Scott
Fenton, 31-Jul-2019.)
|
⊢ ( Nc V
·c Nc V) = Nc V |
|
Theorem | vvsqenvv 6256 |
There are exactly as many ordered pairs as there are sets. Corollary to
theorem XI.2.37 of [Rosser] p. 381.
(Contributed by Scott Fenton,
31-Jul-2019.)
|
⊢ (V × V) ≈ V |
|
Theorem | 0lt1c 6257 |
Cardinal one is strictly greater than cardinal zero. (Contributed by
Scott Fenton, 1-Aug-2019.)
|
⊢ 0c <c
1c |
|
Theorem | csucex 6258 |
The function mapping x to its
cardinal successor exists.
(Contributed by Scott Fenton, 30-Jul-2019.)
|
⊢ (x ∈ V ↦ (x +c 1c)) ∈ V |
|
Theorem | brcsuc 6259* |
Binary relationship form of the successor mapping function.
(Contributed by Scott Fenton, 2-Aug-2019.)
|
⊢ A ∈ V
& ⊢ B ∈ V ⇒ ⊢ (A(x ∈ V ↦ (x
+c 1c))B ↔ B =
(A +c
1c)) |
|
Theorem | nnltp1clem1 6260 |
Lemma for nnltp1c 6261. Set up stratification. (Contributed by SF,
25-Mar-2015.)
|
⊢ {x ∣ x
<c (x +c
1c)} ∈ V |
|
Theorem | nnltp1c 6261 |
Any natural is less than one plus itself. (Contributed by SF,
25-Mar-2015.)
|
⊢ (N ∈ Nn → N <c (N +c
1c)) |
|
Theorem | addccan2nclem1 6262* |
Lemma for addccan2nc 6264. Stratification helper theorem.
(Contributed
by Scott Fenton, 2-Aug-2019.)
|
⊢ (x( AddC ∘ ◡(1st ↾ (V × {n})))y ↔
y = (x
+c n)) |
|
Theorem | addccan2nclem2 6263* |
Lemma for addccan2nc 6264. Establish stratification for induction.
(Contributed by Scott Fenton, 2-Aug-2019.)
|
⊢ ((N ∈ V ∧ P ∈ W) →
{x ∣
((x +c N) = (x
+c P) → N = P)} ∈ V) |
|
Theorem | addccan2nc 6264 |
Cancellation law for addition over the cardinal numbers. Biconditional
form of theorem XI.3.2 of [Rosser] p.
391. (Contributed by Scott
Fenton, 2-Aug-2019.)
|
⊢ ((M ∈ Nn ∧ N ∈ NC ∧ P ∈ NC ) →
((M +c N) = (M
+c P) ↔ N = P)) |
|
Theorem | lecadd2 6265 |
Cardinal addition preserves cardinal less than. Biconditional form of
corollary 4 of theorem XI.3.2 of [Rosser]
p. 391. (Contributed by Scott
Fenton, 2-Aug-2019.)
|
⊢ ((M ∈ Nn ∧ N ∈ NC ∧ P ∈ NC ) →
((M +c N) ≤c (M +c P) ↔ N
≤c P)) |
|
Theorem | ncslesuc 6266 |
Relationship between successor and cardinal less than or equal.
(Contributed by Scott Fenton, 3-Aug-2019.)
|
⊢ ((M ∈ NC ∧ N ∈ NC ) →
(M ≤c (N +c 1c) ↔
(M ≤c N ∨ M = (N
+c 1c)))) |
|
Theorem | nmembers1lem1 6267* |
Lemma for nmembers1 6270. Set up stratification. (Contributed by SF,
25-Mar-2015.)
|
⊢ {x ∣ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c x)} ∈ Tc Tc x}
∈ V |
|
Theorem | nmembers1lem2 6268 |
Lemma for nmembers1 6270. The set of all elements between one and
zero is
empty. (Contributed by Scott Fenton, 1-Aug-2019.)
|
⊢ {m ∈ Nn ∣ (1c ≤c m ∧ m ≤c 0c)} ∈ 0c |
|
Theorem | nmembers1lem3 6269* |
Lemma for nmembers1 6270. If the interval from one to a natural is in
a
given natural, extending it by one puts it in the next natural.
(Contributed by Scott Fenton, 3-Aug-2019.)
|
⊢ ((A ∈ Nn ∧ B ∈ Nn ) →
({m ∈
Nn ∣
(1c ≤c m
∧ m
≤c A)} ∈ B →
{m ∈
Nn ∣
(1c ≤c m
∧ m
≤c (A +c
1c))} ∈ (B +c
1c))) |
|
Theorem | nmembers1 6270* |
Count the number of elements in a natural interval. From
nmembers1lem2 6268 and nmembers1lem3 6269, we would expect to arrive at
{m ∈ Nn ∣ (1c ≤c m ∧ m ≤c N)} ∈ N, but this proposition is
not stratifiable. Instead, we arrive at the weaker conclusion below.
We can arrive at the earlier proposition once we add the Axiom of
Counting, which we will do later. (Contributed by Scott Fenton,
3-Aug-2019.)
|
⊢ (N ∈ Nn → {m ∈ Nn ∣
(1c ≤c m
∧ m
≤c N)} ∈ Tc Tc N) |
|
2.4.6 Specker's disproof of the axiom of
choice
|
|
Syntax | cspac 6271 |
Extend the definition of a class to include the special set generator for
the axiom of choice.
|
class
Spac |
|
Definition | df-spac 6272* |
Define the special class generator for the disproof of the axiom of
choice. Definition 6.1 of [Specker] p.
973. (Contributed by SF,
3-Mar-2015.)
|
⊢ Spac =
(m ∈
NC ↦ Clos1 ({m}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y =
(2c ↑c x))})) |
|
Theorem | nncdiv3lem1 6273 |
Lemma for nncdiv3 6275. Set up a helper for stratification.
(Contributed
by SF, 3-Mar-2015.)
|
⊢ (〈n, b〉 ∈ ran ( Ins3 ◡((ran
(◡1st ⊗
(1st ∩ 2nd )) ⊗ 2nd ) “
AddC ) ∩ (((1st ∘ 1st ) ⊗ ((2nd
∘ 1st ) ⊗ 2nd
)) “ AddC )) ↔ b = ((n
+c n)
+c n)) |
|
Theorem | nncdiv3lem2 6274* |
Lemma for nncdiv3 6275. Set up stratification for induction.
(Contributed by SF, 2-Mar-2015.)
|
⊢ {a ∣ ∃n ∈ Nn (a = ((n +c n) +c n) ∨ a = (((n
+c n)
+c n)
+c 1c) ∨
a = (((n +c n) +c n) +c 2c))}
∈ V |
|
Theorem | nncdiv3 6275* |
Divisibility by three rule for finite cardinals. Part of Theorem 3.4 of
[Specker] p. 973. (Contributed by SF,
2-Mar-2015.)
|
⊢ (A ∈ Nn → ∃n ∈ Nn (A = ((n
+c n)
+c n) ∨ A =
(((n +c n) +c n) +c 1c) ∨ A =
(((n +c n) +c n) +c
2c))) |
|
Theorem | nnc3n3p1 6276 |
Three times a natural is not one more than three times a natural.
Another part of Theorem 3.4 of [Specker]
p. 973. (Contributed by SF,
13-Mar-2015.)
|
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬
((A +c A) +c A) = (((B
+c B)
+c B)
+c 1c)) |
|
Theorem | nnc3n3p2 6277 |
Three times a natural is not two more than three times a natural.
Another part of Theorem 3.4 of [Specker]
p. 973. (Contributed by SF,
12-Mar-2015.)
|
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬
((A +c A) +c A) = (((B
+c B)
+c B)
+c 2c)) |
|
Theorem | nnc3p1n3p2 6278 |
One more than three times a natural is not two more than three times a
natural. Final part of Theorem 3.4 of [Specker] p. 973. (Contributed
by SF, 12-Mar-2015.)
|
⊢ ((A ∈ Nn ∧ B ∈ Nn ) → ¬
(((A +c A) +c A) +c 1c) =
(((B +c B) +c B) +c
2c)) |
|
Theorem | spacvallem1 6279* |
Lemma for spacval 6280. Set up stratification for the recursive
relationship. (Contributed by SF, 6-Mar-2015.)
|
⊢ {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))} ∈
V |
|
Theorem | spacval 6280* |
The value of the special set generator. (Contributed by SF,
4-Mar-2015.)
|
⊢ (N ∈ NC → ( Spac ‘N) = Clos1 ({N}, {〈x, y〉 ∣ (x ∈ NC ∧ y ∈ NC ∧ y = (2c ↑c
x))})) |
|
Theorem | fnspac 6281 |
The special set generator is a function over the cardinals.
(Contributed by SF, 18-Mar-2015.)
|
⊢ Spac
Fn NC |
|
Theorem | spacssnc 6282 |
The special set generator generates a set of cardinals. (Contributed by
SF, 13-Mar-2015.)
|
⊢ (N ∈ NC → ( Spac ‘N) ⊆ NC ) |
|
Theorem | spacid 6283 |
The initial value of the special set generator is an element.
(Contributed by SF, 13-Mar-2015.)
|
⊢ (M ∈ NC → M ∈ ( Spac ‘M)) |
|
Theorem | spaccl 6284 |
Closure law for the special set generator. (Contributed by SF,
13-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ ( Spac
‘M) ∧ (N
↑c 0c) ∈ NC ) →
(2c ↑c N) ∈ ( Spac ‘M)) |
|
Theorem | spacind 6285* |
Inductive law for the special set generator. (Contributed by SF,
13-Mar-2015.)
|
⊢ (((M ∈ NC ∧ S ∈ V) ∧ (M ∈ S ∧ ∀x ∈ ( Spac ‘M)((x ∈ S ∧ (x
↑c 0c) ∈ NC ) →
(2c ↑c x) ∈ S))) → ( Spac ‘M) ⊆ S) |
|
Theorem | spacis 6286* |
Induction scheme for the special set generator. (Contributed by SF,
13-Mar-2015.)
|
⊢ {x ∣ φ}
∈ V
& ⊢ (x =
M → (φ ↔ ψ))
& ⊢ (x =
y → (φ ↔ χ))
& ⊢ (x =
(2c ↑c y) → (φ ↔ θ))
& ⊢ (x =
N → (φ ↔ τ))
& ⊢ (M ∈ NC → ψ)
& ⊢ (((M ∈ NC ∧ y ∈ ( Spac
‘M)) ∧ ((y
↑c 0c) ∈ NC ∧ χ))
→ θ)
⇒ ⊢ ((M ∈ NC ∧ N ∈ ( Spac ‘M)) → τ) |
|
Theorem | nchoicelem1 6287 |
Lemma for nchoice 6306. A finite cardinal is not one more than its
T-raising. (Contributed by SF, 3-Mar-2015.)
|
⊢ (A ∈ Nn → ¬
A = ( Tc A
+c 1c)) |
|
Theorem | nchoicelem2 6288 |
Lemma for nchoice 6306. A finite cardinal is not two more than its
T-raising. (Contributed by SF, 12-Mar-2015.)
|
⊢ (A ∈ Nn → ¬
A = ( Tc A
+c 2c)) |
|
Theorem | nchoicelem3 6289 |
Lemma for nchoice 6306. Compute the value of Spac when the argument
is not exponentiable. Theorem 6.2 of [Specker] p. 973. (Contributed by
SF, 13-Mar-2015.)
|
⊢ ((M ∈ NC ∧ ¬ (M
↑c 0c) ∈ NC ) → ( Spac ‘M) = {M}) |
|
Theorem | nchoicelem4 6290 |
Lemma for nchoice 6306. The initial value of Spac is a minimum
value. Theorem 6.4 of [Specker] p. 973.
(Contributed by SF,
13-Mar-2015.)
|
⊢ ((M ∈ NC ∧ N ∈ ( Spac
‘M)) → M ≤c N) |
|
Theorem | nchoicelem5 6291 |
Lemma for nchoice 6306. A cardinal is not a member of the special
set of
itself raised to two. Theorem 6.5 of [Specker] p. 973. (Contributed by
SF, 13-Mar-2015.)
|
⊢ ((M ∈ NC ∧ (M
↑c 0c) ∈ NC ) → ¬
M ∈ (
Spac ‘(2c
↑c M))) |
|
Theorem | nchoicelem6 6292 |
Lemma for nchoice 6306. Split the special set generator into base
and
inductive values. Theorem 6.6 of [Specker] p. 973. (Contributed by SF,
13-Mar-2015.)
|
⊢ ((M ∈ NC ∧ (M
↑c 0c) ∈ NC ) → ( Spac ‘M) = ({M} ∪
( Spac ‘(2c
↑c M)))) |
|
Theorem | nchoicelem7 6293 |
Lemma for nchoice 6306. Calculate the cardinality of a special set
generator. Theorem 6.7 of [Specker] p.
974. (Contributed by SF,
13-Mar-2015.)
|
⊢ ((M ∈ NC ∧ (M
↑c 0c) ∈ NC ) → Nc ( Spac
‘M) = ( Nc ( Spac
‘(2c ↑c M)) +c
1c)) |
|
Theorem | nchoicelem8 6294 |
Lemma for nchoice 6306. An anti-closure condition for cardinal
exponentiation to zero. Theorem 4.5 of [Specker] p. 973. (Contributed
by SF, 18-Mar-2015.)
|
⊢ (( ≤c We NC ∧ M ∈ NC ) → (¬
(M ↑c
0c) ∈ NC ↔ Nc
1c <c M)) |
|
Theorem | nchoicelem9 6295 |
Lemma for nchoice 6306. Calculate the cardinality of the special
set
generator when near the end of raisability. Theorem 6.8 of [Specker]
p. 974. (Contributed by SF, 18-Mar-2015.)
|
⊢ (( ≤c We NC ∧ M ∈ NC ∧ ¬ (M
↑c 0c) ∈ NC ) → ( Nc ( Spac
‘ Tc M) = 2c
∨ Nc ( Spac ‘ Tc M) =
3c)) |
|
Theorem | nchoicelem10 6296 |
Lemma for nchoice 6306. Stratification helper lemma. (Contributed
by SF,
18-Mar-2015.)
|
⊢ S ∈ V
& ⊢ X ∈ V ⇒ ⊢ (〈c, X〉 ∈ ∼ ((
Ins3 S ⊕
Ins2 ∼ ran (◡ ∼ S
⊗ (◡ S
↾ Fix
( S ∘
ImageS)))) “ 1c)
↔ c = Clos1
(X, S)) |
|
Theorem | nchoicelem11 6297* |
Lemma for nchoice 6306. Set up stratification for nchoicelem12 6298.
(Contributed by SF, 18-Mar-2015.)
|
⊢ {t ∣ ∀m ∈ NC (t = Nc ( Spac
‘ Tc m) → Nc ( Spac ‘m) ∈ Nn )} ∈
V |
|
Theorem | nchoicelem12 6298 |
Lemma for nchoice 6306. If the T-raising of a cardinal yields a
finite
special set, then so does the initial set. Theorem 7.1 of [Specker]
p. 974. (Contributed by SF, 18-Mar-2015.)
|
⊢ ((M ∈ NC ∧ ( Spac
‘ Tc M) ∈ Fin ) → ( Spac ‘M) ∈ Fin ) |
|
Theorem | nchoicelem13 6299 |
Lemma for nchoice 6306. The cardinality of a special set is at
least
one. (Contributed by SF, 18-Mar-2015.)
|
⊢ (M ∈ NC →
1c ≤c Nc ( Spac ‘M)) |
|
Theorem | nchoicelem14 6300 |
Lemma for nchoice 6306. When the special set generator yields a
singleton, then the cardinal is not raisable. (Contributed by SF,
19-Mar-2015.)
|
⊢ ((M ∈ NC ∧ Nc ( Spac ‘M) = 1c) → ¬ (M ↑c 0c)
∈ NC
) |