Theorem List for Intuitionistic Logic Explorer - 6401-6500 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | 1oex 6401 |
Ordinal 1 is a set. (Contributed by BJ, 4-Jul-2022.)
|
⊢ 1o ∈ V |
|
Theorem | 2on 6402 |
Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004.) (Proof
shortened by Andrew Salmon, 12-Aug-2011.)
|
⊢ 2o ∈ On |
|
Theorem | 2on0 6403 |
Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011.)
|
⊢ 2o ≠ ∅ |
|
Theorem | 3on 6404 |
Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ 3o ∈ On |
|
Theorem | 4on 6405 |
Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ 4o ∈ On |
|
Theorem | df1o2 6406 |
Expanded value of the ordinal number 1. (Contributed by NM,
4-Nov-2002.)
|
⊢ 1o = {∅} |
|
Theorem | df2o3 6407 |
Expanded value of the ordinal number 2. (Contributed by Mario Carneiro,
14-Aug-2015.)
|
⊢ 2o = {∅,
1o} |
|
Theorem | df2o2 6408 |
Expanded value of the ordinal number 2. (Contributed by NM,
29-Jan-2004.)
|
⊢ 2o = {∅,
{∅}} |
|
Theorem | 1n0 6409 |
Ordinal one is not equal to ordinal zero. (Contributed by NM,
26-Dec-2004.)
|
⊢ 1o ≠ ∅ |
|
Theorem | xp01disj 6410 |
Cartesian products with the singletons of ordinals 0 and 1 are disjoint.
(Contributed by NM, 2-Jun-2007.)
|
⊢ ((𝐴 × {∅}) ∩ (𝐶 × {1o})) =
∅ |
|
Theorem | xp01disjl 6411 |
Cartesian products with the singletons of ordinals 0 and 1 are disjoint.
(Contributed by Jim Kingdon, 11-Jul-2023.)
|
⊢ (({∅} × 𝐴) ∩ ({1o} × 𝐶)) = ∅ |
|
Theorem | ordgt0ge1 6412 |
Two ways to express that an ordinal class is positive. (Contributed by
NM, 21-Dec-2004.)
|
⊢ (Ord 𝐴 → (∅ ∈ 𝐴 ↔ 1o ⊆ 𝐴)) |
|
Theorem | ordge1n0im 6413 |
An ordinal greater than or equal to 1 is nonzero. (Contributed by Jim
Kingdon, 26-Jun-2019.)
|
⊢ (Ord 𝐴 → (1o ⊆ 𝐴 → 𝐴 ≠ ∅)) |
|
Theorem | el1o 6414 |
Membership in ordinal one. (Contributed by NM, 5-Jan-2005.)
|
⊢ (𝐴 ∈ 1o ↔ 𝐴 = ∅) |
|
Theorem | dif1o 6415 |
Two ways to say that 𝐴 is a nonzero number of the set 𝐵.
(Contributed by Mario Carneiro, 21-May-2015.)
|
⊢ (𝐴 ∈ (𝐵 ∖ 1o) ↔ (𝐴 ∈ 𝐵 ∧ 𝐴 ≠ ∅)) |
|
Theorem | 2oconcl 6416 |
Closure of the pair swapping function on 2o.
(Contributed by Mario
Carneiro, 27-Sep-2015.)
|
⊢ (𝐴 ∈ 2o → (1o
∖ 𝐴) ∈
2o) |
|
Theorem | 0lt1o 6417 |
Ordinal zero is less than ordinal one. (Contributed by NM,
5-Jan-2005.)
|
⊢ ∅ ∈
1o |
|
Theorem | 0lt2o 6418 |
Ordinal zero is less than ordinal two. (Contributed by Jim Kingdon,
31-Jul-2022.)
|
⊢ ∅ ∈
2o |
|
Theorem | 1lt2o 6419 |
Ordinal one is less than ordinal two. (Contributed by Jim Kingdon,
31-Jul-2022.)
|
⊢ 1o ∈
2o |
|
Theorem | el2oss1o 6420 |
Being an element of ordinal two implies being a subset of ordinal one.
The converse is equivalent to excluded middle by ss1oel2o 13988.
(Contributed by Jim Kingdon, 8-Aug-2022.)
|
⊢ (𝐴 ∈ 2o → 𝐴 ⊆
1o) |
|
Theorem | oafnex 6421 |
The characteristic function for ordinal addition is defined everywhere.
(Contributed by Jim Kingdon, 27-Jul-2019.)
|
⊢ (𝑥 ∈ V ↦ suc 𝑥) Fn V |
|
Theorem | sucinc 6422* |
Successor is increasing. (Contributed by Jim Kingdon, 25-Jun-2019.)
|
⊢ 𝐹 = (𝑧 ∈ V ↦ suc 𝑧) ⇒ ⊢ ∀𝑥 𝑥 ⊆ (𝐹‘𝑥) |
|
Theorem | sucinc2 6423* |
Successor is increasing. (Contributed by Jim Kingdon, 14-Jul-2019.)
|
⊢ 𝐹 = (𝑧 ∈ V ↦ suc 𝑧) ⇒ ⊢ ((𝐵 ∈ On ∧ 𝐴 ∈ 𝐵) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) |
|
Theorem | fnoa 6424 |
Functionality and domain of ordinal addition. (Contributed by NM,
26-Aug-1995.) (Proof shortened by Mario Carneiro, 3-Jul-2019.)
|
⊢ +o Fn (On ×
On) |
|
Theorem | oaexg 6425 |
Ordinal addition is a set. (Contributed by Mario Carneiro,
3-Jul-2019.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 +o 𝐵) ∈ V) |
|
Theorem | omfnex 6426* |
The characteristic function for ordinal multiplication is defined
everywhere. (Contributed by Jim Kingdon, 23-Aug-2019.)
|
⊢ (𝐴 ∈ 𝑉 → (𝑥 ∈ V ↦ (𝑥 +o 𝐴)) Fn V) |
|
Theorem | fnom 6427 |
Functionality and domain of ordinal multiplication. (Contributed by NM,
26-Aug-1995.) (Revised by Mario Carneiro, 3-Jul-2019.)
|
⊢ ·o Fn (On ×
On) |
|
Theorem | omexg 6428 |
Ordinal multiplication is a set. (Contributed by Mario Carneiro,
3-Jul-2019.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ·o 𝐵) ∈ V) |
|
Theorem | fnoei 6429 |
Functionality and domain of ordinal exponentiation. (Contributed by
Mario Carneiro, 29-May-2015.) (Revised by Mario Carneiro,
3-Jul-2019.)
|
⊢ ↑o Fn (On ×
On) |
|
Theorem | oeiexg 6430 |
Ordinal exponentiation is a set. (Contributed by Mario Carneiro,
3-Jul-2019.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ↑o 𝐵) ∈ V) |
|
Theorem | oav 6431* |
Value of ordinal addition. (Contributed by NM, 3-May-1995.) (Revised
by Mario Carneiro, 8-Sep-2013.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (rec((𝑥 ∈ V ↦ suc 𝑥), 𝐴)‘𝐵)) |
|
Theorem | omv 6432* |
Value of ordinal multiplication. (Contributed by NM, 17-Sep-1995.)
(Revised by Mario Carneiro, 23-Aug-2014.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 +o 𝐴)), ∅)‘𝐵)) |
|
Theorem | oeiv 6433* |
Value of ordinal exponentiation. (Contributed by Jim Kingdon,
9-Jul-2019.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) = (rec((𝑥 ∈ V ↦ (𝑥 ·o 𝐴)), 1o)‘𝐵)) |
|
Theorem | oa0 6434 |
Addition with zero. Proposition 8.3 of [TakeutiZaring] p. 57.
(Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
⊢ (𝐴 ∈ On → (𝐴 +o ∅) = 𝐴) |
|
Theorem | om0 6435 |
Ordinal multiplication with zero. Definition 8.15 of [TakeutiZaring]
p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
⊢ (𝐴 ∈ On → (𝐴 ·o ∅) =
∅) |
|
Theorem | oei0 6436 |
Ordinal exponentiation with zero exponent. Definition 8.30 of
[TakeutiZaring] p. 67.
(Contributed by NM, 31-Dec-2004.) (Revised by
Mario Carneiro, 8-Sep-2013.)
|
⊢ (𝐴 ∈ On → (𝐴 ↑o ∅) =
1o) |
|
Theorem | oacl 6437 |
Closure law for ordinal addition. Proposition 8.2 of [TakeutiZaring]
p. 57. (Contributed by NM, 5-May-1995.) (Constructive proof by Jim
Kingdon, 26-Jul-2019.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) ∈ On) |
|
Theorem | omcl 6438 |
Closure law for ordinal multiplication. Proposition 8.16 of
[TakeutiZaring] p. 57.
(Contributed by NM, 3-Aug-2004.) (Constructive
proof by Jim Kingdon, 26-Jul-2019.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) |
|
Theorem | oeicl 6439 |
Closure law for ordinal exponentiation. (Contributed by Jim Kingdon,
26-Jul-2019.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ↑o 𝐵) ∈ On) |
|
Theorem | oav2 6440* |
Value of ordinal addition. (Contributed by Mario Carneiro and Jim
Kingdon, 12-Aug-2019.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) = (𝐴 ∪ ∪
𝑥 ∈ 𝐵 suc (𝐴 +o 𝑥))) |
|
Theorem | oasuc 6441 |
Addition with successor. Definition 8.1 of [TakeutiZaring] p. 56.
(Contributed by NM, 3-May-1995.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) |
|
Theorem | omv2 6442* |
Value of ordinal multiplication. (Contributed by Jim Kingdon,
23-Aug-2019.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) = ∪
𝑥 ∈ 𝐵 ((𝐴 ·o 𝑥) +o 𝐴)) |
|
Theorem | onasuc 6443 |
Addition with successor. Theorem 4I(A2) of [Enderton] p. 79.
(Contributed by Mario Carneiro, 16-Nov-2014.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) |
|
Theorem | oa1suc 6444 |
Addition with 1 is same as successor. Proposition 4.34(a) of [Mendelson]
p. 266. (Contributed by NM, 29-Oct-1995.) (Revised by Mario Carneiro,
16-Nov-2014.)
|
⊢ (𝐴 ∈ On → (𝐴 +o 1o) = suc 𝐴) |
|
Theorem | o1p1e2 6445 |
1 + 1 = 2 for ordinal numbers. (Contributed by NM, 18-Feb-2004.)
|
⊢ (1o +o 1o)
= 2o |
|
Theorem | oawordi 6446 |
Weak ordering property of ordinal addition. (Contributed by Jim
Kingdon, 27-Jul-2019.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵))) |
|
Theorem | oawordriexmid 6447* |
A weak ordering property of ordinal addition which implies excluded
middle. The property is proposition 8.7 of [TakeutiZaring] p. 59.
Compare with oawordi 6446. (Contributed by Jim Kingdon, 15-May-2022.)
|
⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → (𝑎 ⊆ 𝑏 → (𝑎 +o 𝑐) ⊆ (𝑏 +o 𝑐))) ⇒ ⊢ (𝜑 ∨ ¬ 𝜑) |
|
Theorem | oaword1 6448 |
An ordinal is less than or equal to its sum with another. Part of
Exercise 5 of [TakeutiZaring] p. 62.
(Contributed by NM, 6-Dec-2004.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐴 +o 𝐵)) |
|
Theorem | omsuc 6449 |
Multiplication with successor. Definition 8.15 of [TakeutiZaring]
p. 62. (Contributed by NM, 17-Sep-1995.) (Revised by Mario Carneiro,
8-Sep-2013.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) |
|
Theorem | onmsuc 6450 |
Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80.
(Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro,
14-Nov-2014.)
|
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) |
|
2.6.24 Natural number arithmetic
|
|
Theorem | nna0 6451 |
Addition with zero. Theorem 4I(A1) of [Enderton] p. 79. (Contributed by
NM, 20-Sep-1995.)
|
⊢ (𝐴 ∈ ω → (𝐴 +o ∅) = 𝐴) |
|
Theorem | nnm0 6452 |
Multiplication with zero. Theorem 4J(A1) of [Enderton] p. 80.
(Contributed by NM, 20-Sep-1995.)
|
⊢ (𝐴 ∈ ω → (𝐴 ·o ∅) =
∅) |
|
Theorem | nnasuc 6453 |
Addition with successor. Theorem 4I(A2) of [Enderton] p. 79.
(Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro,
14-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o suc 𝐵) = suc (𝐴 +o 𝐵)) |
|
Theorem | nnmsuc 6454 |
Multiplication with successor. Theorem 4J(A2) of [Enderton] p. 80.
(Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro,
14-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·o suc 𝐵) = ((𝐴 ·o 𝐵) +o 𝐴)) |
|
Theorem | nna0r 6455 |
Addition to zero. Remark in proof of Theorem 4K(2) of [Enderton] p. 81.
(Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro,
14-Nov-2014.)
|
⊢ (𝐴 ∈ ω → (∅
+o 𝐴) = 𝐴) |
|
Theorem | nnm0r 6456 |
Multiplication with zero. Exercise 16 of [Enderton] p. 82.
(Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
⊢ (𝐴 ∈ ω → (∅
·o 𝐴) =
∅) |
|
Theorem | nnacl 6457 |
Closure of addition of natural numbers. Proposition 8.9 of
[TakeutiZaring] p. 59.
(Contributed by NM, 20-Sep-1995.) (Proof
shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) ∈ ω) |
|
Theorem | nnmcl 6458 |
Closure of multiplication of natural numbers. Proposition 8.17 of
[TakeutiZaring] p. 63.
(Contributed by NM, 20-Sep-1995.) (Proof
shortened by Andrew Salmon, 22-Oct-2011.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·o 𝐵) ∈ ω) |
|
Theorem | nnacli 6459 |
ω is closed under addition. Inference form of nnacl 6457.
(Contributed by Scott Fenton, 20-Apr-2012.)
|
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈
ω ⇒ ⊢ (𝐴 +o 𝐵) ∈ ω |
|
Theorem | nnmcli 6460 |
ω is closed under multiplication. Inference form
of nnmcl 6458.
(Contributed by Scott Fenton, 20-Apr-2012.)
|
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈
ω ⇒ ⊢ (𝐴 ·o 𝐵) ∈ ω |
|
Theorem | nnacom 6461 |
Addition of natural numbers is commutative. Theorem 4K(2) of [Enderton]
p. 81. (Contributed by NM, 6-May-1995.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +o 𝐵) = (𝐵 +o 𝐴)) |
|
Theorem | nnaass 6462 |
Addition of natural numbers is associative. Theorem 4K(1) of [Enderton]
p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶))) |
|
Theorem | nndi 6463 |
Distributive law for natural numbers (left-distributivity). Theorem
4K(3) of [Enderton] p. 81.
(Contributed by NM, 20-Sep-1995.) (Revised
by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))) |
|
Theorem | nnmass 6464 |
Multiplication of natural numbers is associative. Theorem 4K(4) of
[Enderton] p. 81. (Contributed by NM,
20-Sep-1995.) (Revised by Mario
Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ·o 𝐵) ·o 𝐶) = (𝐴 ·o (𝐵 ·o 𝐶))) |
|
Theorem | nnmsucr 6465 |
Multiplication with successor. Exercise 16 of [Enderton] p. 82.
(Contributed by NM, 21-Sep-1995.) (Proof shortened by Andrew Salmon,
22-Oct-2011.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (suc 𝐴 ·o 𝐵) = ((𝐴 ·o 𝐵) +o 𝐵)) |
|
Theorem | nnmcom 6466 |
Multiplication of natural numbers is commutative. Theorem 4K(5) of
[Enderton] p. 81. (Contributed by NM,
21-Sep-1995.) (Proof shortened
by Andrew Salmon, 22-Oct-2011.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ·o 𝐵) = (𝐵 ·o 𝐴)) |
|
Theorem | nndir 6467 |
Distributive law for natural numbers (right-distributivity). (Contributed
by Jim Kingdon, 3-Dec-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) ·o 𝐶) = ((𝐴 ·o 𝐶) +o (𝐵 ·o 𝐶))) |
|
Theorem | nnsucelsuc 6468 |
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucelsucr 4490, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucelsucexmid 4512.
(Contributed by Jim Kingdon, 25-Aug-2019.)
|
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)) |
|
Theorem | nnsucsssuc 6469 |
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucsssucr 4491, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucsssucexmid 4509.
(Contributed by Jim Kingdon, 25-Aug-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵)) |
|
Theorem | nntri3or 6470 |
Trichotomy for natural numbers. (Contributed by Jim Kingdon,
25-Aug-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |
|
Theorem | nntri2 6471 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28-Aug-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
|
Theorem | nnsucuniel 6472 |
Given an element 𝐴 of the union of a natural number
𝐵,
suc 𝐴 is an element of 𝐵 itself.
The reverse direction holds
for all ordinals (sucunielr 4492). The forward direction for all
ordinals implies excluded middle (ordsucunielexmid 4513). (Contributed
by Jim Kingdon, 13-Mar-2022.)
|
⊢ (𝐵 ∈ ω → (𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵)) |
|
Theorem | nntri1 6473 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28-Aug-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) |
|
Theorem | nntri3 6474 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-May-2020.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 = 𝐵 ↔ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴))) |
|
Theorem | nntri2or2 6475 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-Sep-2021.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) |
|
Theorem | nndceq 6476 |
Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p.
(varies). For the specific case where 𝐵 is zero, see nndceq0 4600.
(Contributed by Jim Kingdon, 31-Aug-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
DECID 𝐴 =
𝐵) |
|
Theorem | nndcel 6477 |
Set membership between two natural numbers is decidable. (Contributed by
Jim Kingdon, 6-Sep-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
DECID 𝐴
∈ 𝐵) |
|
Theorem | nnsseleq 6478 |
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16-Sep-2021.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) |
|
Theorem | nnsssuc 6479 |
A natural number is a subset of another natural number if and only if it
belongs to its successor. (Contributed by Jim Kingdon, 22-Jul-2023.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ 𝐴 ∈ suc 𝐵)) |
|
Theorem | nntr2 6480 |
Transitive law for natural numbers. (Contributed by Jim Kingdon,
22-Jul-2023.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
|
Theorem | dcdifsnid 6481* |
If we remove a single element from a set with decidable equality then
put it back in, we end up with the original set. This strengthens
difsnss 3724 from subset to equality but the proof relies
on equality being
decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
|
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
|
Theorem | fnsnsplitdc 6482* |
Split a function into a single point and all the rest. (Contributed by
Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 29-Jan-2023.)
|
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐹 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐹 = ((𝐹 ↾ (𝐴 ∖ {𝑋})) ∪ {〈𝑋, (𝐹‘𝑋)〉})) |
|
Theorem | funresdfunsndc 6483* |
Restricting a function to a domain without one element of the domain of
the function, and adding a pair of this element and the function value
of the element results in the function itself, where equality is
decidable. (Contributed by AV, 2-Dec-2018.) (Revised by Jim Kingdon,
30-Jan-2023.)
|
⊢ ((∀𝑥 ∈ dom 𝐹∀𝑦 ∈ dom 𝐹DECID 𝑥 = 𝑦 ∧ Fun 𝐹 ∧ 𝑋 ∈ dom 𝐹) → ((𝐹 ↾ (V ∖ {𝑋})) ∪ {〈𝑋, (𝐹‘𝑋)〉}) = 𝐹) |
|
Theorem | nndifsnid 6484 |
If we remove a single element from a natural number then put it back in,
we end up with the original natural number. This strengthens difsnss 3724
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
|
Theorem | nnaordi 6485 |
Ordering property of addition. Proposition 8.4 of [TakeutiZaring]
p. 58, limited to natural numbers. (Contributed by NM, 3-Feb-1996.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 → (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) |
|
Theorem | nnaord 6486 |
Ordering property of addition. Proposition 8.4 of [TakeutiZaring] p. 58,
limited to natural numbers, and its converse. (Contributed by NM,
7-Mar-1996.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 ↔ (𝐶 +o 𝐴) ∈ (𝐶 +o 𝐵))) |
|
Theorem | nnaordr 6487 |
Ordering property of addition of natural numbers. (Contributed by NM,
9-Nov-2002.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 ↔ (𝐴 +o 𝐶) ∈ (𝐵 +o 𝐶))) |
|
Theorem | nnaword 6488 |
Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵))) |
|
Theorem | nnacan 6489 |
Cancellation law for addition of natural numbers. (Contributed by NM,
27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) = (𝐴 +o 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | nnaword1 6490 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐴 ⊆ (𝐴 +o 𝐵)) |
|
Theorem | nnaword2 6491 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐴 ⊆ (𝐵 +o 𝐴)) |
|
Theorem | nnawordi 6492 |
Adding to both sides of an inequality in ω.
(Contributed by Scott
Fenton, 16-Apr-2012.) (Revised by Mario Carneiro, 12-May-2012.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ⊆ 𝐵 → (𝐴 +o 𝐶) ⊆ (𝐵 +o 𝐶))) |
|
Theorem | nnmordi 6493 |
Ordering property of multiplication. Half of Proposition 8.19 of
[TakeutiZaring] p. 63, limited to
natural numbers. (Contributed by NM,
18-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ (((𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐶) → (𝐴 ∈ 𝐵 → (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) |
|
Theorem | nnmord 6494 |
Ordering property of multiplication. Proposition 8.19 of [TakeutiZaring]
p. 63, limited to natural numbers. (Contributed by NM, 22-Jan-1996.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶) ↔ (𝐶 ·o 𝐴) ∈ (𝐶 ·o 𝐵))) |
|
Theorem | nnmword 6495 |
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17-Nov-2014.)
|
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ·o 𝐴) ⊆ (𝐶 ·o 𝐵))) |
|
Theorem | nnmcan 6496 |
Cancellation law for multiplication of natural numbers. (Contributed by
NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | 1onn 6497 |
One is a natural number. (Contributed by NM, 29-Oct-1995.)
|
⊢ 1o ∈
ω |
|
Theorem | 2onn 6498 |
The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|
⊢ 2o ∈
ω |
|
Theorem | 3onn 6499 |
The ordinal 3 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ 3o ∈
ω |
|
Theorem | 4onn 6500 |
The ordinal 4 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ 4o ∈
ω |