Theorem List for Intuitionistic Logic Explorer - 6501-6600 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | nnmsuc 6501 |
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 6502 |
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 6503 |
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 6504 |
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 6505 |
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 6506 |
ω is closed under addition. Inference form of nnacl 6504.
(Contributed by Scott Fenton, 20-Apr-2012.)
|
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈
ω ⇒ ⊢ (𝐴 +o 𝐵) ∈ ω |
|
Theorem | nnmcli 6507 |
ω is closed under multiplication. Inference form
of nnmcl 6505.
(Contributed by Scott Fenton, 20-Apr-2012.)
|
⊢ 𝐴 ∈ ω & ⊢ 𝐵 ∈
ω ⇒ ⊢ (𝐴 ·o 𝐵) ∈ ω |
|
Theorem | nnacom 6508 |
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 6509 |
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 6510 |
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 6511 |
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 6512 |
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 6513 |
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 6514 |
Distributive law for natural numbers (right-distributivity). (Contributed
by Jim Kingdon, 3-Dec-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) ·o 𝐶) = ((𝐴 ·o 𝐶) +o (𝐵 ·o 𝐶))) |
|
Theorem | nnsucelsuc 6515 |
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucelsucr 4525, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucelsucexmid 4547.
(Contributed by Jim Kingdon, 25-Aug-2019.)
|
⊢ (𝐵 ∈ ω → (𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵)) |
|
Theorem | nnsucsssuc 6516 |
Membership is inherited by successors. The reverse direction holds for
all ordinals, as seen at onsucsssucr 4526, but the forward direction, for
all ordinals, implies excluded middle as seen as onsucsssucexmid 4544.
(Contributed by Jim Kingdon, 25-Aug-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ suc 𝐴 ⊆ suc 𝐵)) |
|
Theorem | nntri3or 6517 |
Trichotomy for natural numbers. (Contributed by Jim Kingdon,
25-Aug-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) |
|
Theorem | nntri2 6518 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28-Aug-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴))) |
|
Theorem | nnsucuniel 6519 |
Given an element 𝐴 of the union of a natural number
𝐵,
suc 𝐴 is an element of 𝐵 itself.
The reverse direction holds
for all ordinals (sucunielr 4527). The forward direction for all
ordinals implies excluded middle (ordsucunielexmid 4548). (Contributed
by Jim Kingdon, 13-Mar-2022.)
|
⊢ (𝐵 ∈ ω → (𝐴 ∈ ∪ 𝐵 ↔ suc 𝐴 ∈ 𝐵)) |
|
Theorem | nntri1 6520 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
28-Aug-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴)) |
|
Theorem | nntri3 6521 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-May-2020.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 = 𝐵 ↔ (¬ 𝐴 ∈ 𝐵 ∧ ¬ 𝐵 ∈ 𝐴))) |
|
Theorem | nntri2or2 6522 |
A trichotomy law for natural numbers. (Contributed by Jim Kingdon,
15-Sep-2021.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) |
|
Theorem | nndceq 6523 |
Equality of natural numbers is decidable. Theorem 7.2.6 of [HoTT], p.
(varies). For the specific case where 𝐵 is zero, see nndceq0 4635.
(Contributed by Jim Kingdon, 31-Aug-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
DECID 𝐴 =
𝐵) |
|
Theorem | nndcel 6524 |
Set membership between two natural numbers is decidable. (Contributed by
Jim Kingdon, 6-Sep-2019.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) →
DECID 𝐴
∈ 𝐵) |
|
Theorem | nnsseleq 6525 |
For natural numbers, inclusion is equivalent to membership or equality.
(Contributed by Jim Kingdon, 16-Sep-2021.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵))) |
|
Theorem | nnsssuc 6526 |
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 6527 |
Transitive law for natural numbers. (Contributed by Jim Kingdon,
22-Jul-2023.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
|
Theorem | dcdifsnid 6528* |
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 3753 from subset to equality but the proof relies
on equality being
decidable. (Contributed by Jim Kingdon, 17-Jun-2022.)
|
⊢ ((∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 DECID 𝑥 = 𝑦 ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
|
Theorem | fnsnsplitdc 6529* |
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 6530* |
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 6531 |
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 3753
from subset to equality but the proof relies on equality being
decidable. (Contributed by Jim Kingdon, 31-Aug-2021.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
|
Theorem | nnaordi 6532 |
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 6533 |
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 6534 |
Ordering property of addition of natural numbers. (Contributed by NM,
9-Nov-2002.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ∈ 𝐵 ↔ (𝐴 +o 𝐶) ∈ (𝐵 +o 𝐶))) |
|
Theorem | nnaword 6535 |
Weak ordering property of addition. (Contributed by NM, 17-Sep-1995.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +o 𝐴) ⊆ (𝐶 +o 𝐵))) |
|
Theorem | nnacan 6536 |
Cancellation law for addition of natural numbers. (Contributed by NM,
27-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) → ((𝐴 +o 𝐵) = (𝐴 +o 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | nnaword1 6537 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
(Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐴 ⊆ (𝐴 +o 𝐵)) |
|
Theorem | nnaword2 6538 |
Weak ordering property of addition. (Contributed by NM, 9-Nov-2002.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → 𝐴 ⊆ (𝐵 +o 𝐴)) |
|
Theorem | nnawordi 6539 |
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 6540 |
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 6541 |
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 6542 |
Weak ordering property of ordinal multiplication. (Contributed by Mario
Carneiro, 17-Nov-2014.)
|
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐶) → (𝐴 ⊆ 𝐵 ↔ (𝐶 ·o 𝐴) ⊆ (𝐶 ·o 𝐵))) |
|
Theorem | nnmcan 6543 |
Cancellation law for multiplication of natural numbers. (Contributed by
NM, 26-Oct-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ (((𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝐵) = (𝐴 ·o 𝐶) ↔ 𝐵 = 𝐶)) |
|
Theorem | 1onn 6544 |
One is a natural number. (Contributed by NM, 29-Oct-1995.)
|
⊢ 1o ∈
ω |
|
Theorem | 2onn 6545 |
The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004.)
|
⊢ 2o ∈
ω |
|
Theorem | 3onn 6546 |
The ordinal 3 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ 3o ∈
ω |
|
Theorem | 4onn 6547 |
The ordinal 4 is a natural number. (Contributed by Mario Carneiro,
5-Jan-2016.)
|
⊢ 4o ∈
ω |
|
Theorem | 2ssom 6548 |
The ordinal 2 is included in the set of natural number ordinals.
(Contributed by BJ, 5-Aug-2024.)
|
⊢ 2o ⊆
ω |
|
Theorem | nnm1 6549 |
Multiply an element of ω by 1o. (Contributed by Mario
Carneiro, 17-Nov-2014.)
|
⊢ (𝐴 ∈ ω → (𝐴 ·o 1o) =
𝐴) |
|
Theorem | nnm2 6550 |
Multiply an element of ω by 2o. (Contributed by Scott Fenton,
18-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
⊢ (𝐴 ∈ ω → (𝐴 ·o 2o) =
(𝐴 +o 𝐴)) |
|
Theorem | nn2m 6551 |
Multiply an element of ω by 2o. (Contributed by Scott Fenton,
16-Apr-2012.) (Revised by Mario Carneiro, 17-Nov-2014.)
|
⊢ (𝐴 ∈ ω → (2o
·o 𝐴) =
(𝐴 +o 𝐴)) |
|
Theorem | nnaordex 6552* |
Equivalence for ordering. Compare Exercise 23 of [Enderton] p. 88.
(Contributed by NM, 5-Dec-1995.) (Revised by Mario Carneiro,
15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ∈ 𝐵 ↔ ∃𝑥 ∈ ω (∅ ∈ 𝑥 ∧ (𝐴 +o 𝑥) = 𝐵))) |
|
Theorem | nnawordex 6553* |
Equivalence for weak ordering of natural numbers. (Contributed by NM,
8-Nov-2002.) (Revised by Mario Carneiro, 15-Nov-2014.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ⊆ 𝐵 ↔ ∃𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵)) |
|
Theorem | nnm00 6554 |
The product of two natural numbers is zero iff at least one of them is
zero. (Contributed by Jim Kingdon, 11-Nov-2004.)
|
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → ((𝐴 ·o 𝐵) = ∅ ↔ (𝐴 = ∅ ∨ 𝐵 = ∅))) |
|
2.6.25 Equivalence relations and
classes
|
|
Syntax | wer 6555 |
Extend the definition of a wff to include the equivalence predicate.
|
wff 𝑅 Er 𝐴 |
|
Syntax | cec 6556 |
Extend the definition of a class to include equivalence class.
|
class [𝐴]𝑅 |
|
Syntax | cqs 6557 |
Extend the definition of a class to include quotient set.
|
class (𝐴 / 𝑅) |
|
Definition | df-er 6558 |
Define the equivalence relation predicate. Our notation is not standard.
A formal notation doesn't seem to exist in the literature; instead only
informal English tends to be used. The present definition, although
somewhat cryptic, nicely avoids dummy variables. In dfer2 6559 we derive a
more typical definition. We show that an equivalence relation is
reflexive, symmetric, and transitive in erref 6578, ersymb 6572, and ertr 6573.
(Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro,
2-Nov-2015.)
|
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) |
|
Theorem | dfer2 6559* |
Alternate definition of equivalence predicate. (Contributed by NM,
3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))) |
|
Definition | df-ec 6560 |
Define the 𝑅-coset of 𝐴. Exercise 35 of [Enderton] p. 61. This
is called the equivalence class of 𝐴 modulo 𝑅 when 𝑅 is an
equivalence relation (i.e. when Er 𝑅; see dfer2 6559). In this case,
𝐴 is a representative (member) of the
equivalence class [𝐴]𝑅,
which contains all sets that are equivalent to 𝐴. Definition of
[Enderton] p. 57 uses the notation [𝐴]
(subscript) 𝑅, although
we simply follow the brackets by 𝑅 since we don't have subscripted
expressions. For an alternate definition, see dfec2 6561. (Contributed by
NM, 23-Jul-1995.)
|
⊢ [𝐴]𝑅 = (𝑅 “ {𝐴}) |
|
Theorem | dfec2 6561* |
Alternate definition of 𝑅-coset of 𝐴. Definition 34 of
[Suppes] p. 81. (Contributed by NM,
3-Jan-1997.) (Proof shortened by
Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 ∈ 𝑉 → [𝐴]𝑅 = {𝑦 ∣ 𝐴𝑅𝑦}) |
|
Theorem | ecexg 6562 |
An equivalence class modulo a set is a set. (Contributed by NM,
24-Jul-1995.)
|
⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V) |
|
Theorem | ecexr 6563 |
An inhabited equivalence class implies the representative is a set.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
⊢ (𝐴 ∈ [𝐵]𝑅 → 𝐵 ∈ V) |
|
Definition | df-qs 6564* |
Define quotient set. 𝑅 is usually an equivalence relation.
Definition of [Enderton] p. 58.
(Contributed by NM, 23-Jul-1995.)
|
⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} |
|
Theorem | ereq1 6565 |
Equality theorem for equivalence predicate. (Contributed by NM,
4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴)) |
|
Theorem | ereq2 6566 |
Equality theorem for equivalence predicate. (Contributed by Mario
Carneiro, 12-Aug-2015.)
|
⊢ (𝐴 = 𝐵 → (𝑅 Er 𝐴 ↔ 𝑅 Er 𝐵)) |
|
Theorem | errel 6567 |
An equivalence relation is a relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → Rel 𝑅) |
|
Theorem | erdm 6568 |
The domain of an equivalence relation. (Contributed by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴) |
|
Theorem | ercl 6569 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑋) |
|
Theorem | ersym 6570 |
An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐴) |
|
Theorem | ercl2 6571 |
Elementhood in the field of an equivalence relation. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑋) |
|
Theorem | ersymb 6572 |
An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴)) |
|
Theorem | ertr 6573 |
An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) |
|
Theorem | ertrd 6574 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | ertr2d 6575 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐴) |
|
Theorem | ertr3d 6576 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐵𝑅𝐴)
& ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | ertr4d 6577 |
A transitivity relation for equivalences. (Contributed by Mario
Carneiro, 9-Jul-2014.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵)
& ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) |
|
Theorem | erref 6578 |
An equivalence relation is reflexive on its field. Compare Theorem 3M
of [Enderton] p. 56. (Contributed by
Mario Carneiro, 6-May-2013.)
(Revised by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → 𝑅 Er 𝑋)
& ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐴) |
|
Theorem | ercnv 6579 |
The converse of an equivalence relation is itself. (Contributed by
Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅) |
|
Theorem | errn 6580 |
The range and domain of an equivalence relation are equal. (Contributed
by Rodolfo Medina, 11-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → ran 𝑅 = 𝐴) |
|
Theorem | erssxp 6581 |
An equivalence relation is a subset of the cartesian product of the field.
(Contributed by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴)) |
|
Theorem | erex 6582 |
An equivalence relation is a set if its domain is a set. (Contributed by
Rodolfo Medina, 15-Oct-2010.) (Proof shortened by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → (𝐴 ∈ 𝑉 → 𝑅 ∈ V)) |
|
Theorem | erexb 6583 |
An equivalence relation is a set if and only if its domain is a set.
(Contributed by Rodolfo Medina, 15-Oct-2010.) (Revised by Mario Carneiro,
12-Aug-2015.)
|
⊢ (𝑅 Er 𝐴 → (𝑅 ∈ V ↔ 𝐴 ∈ V)) |
|
Theorem | iserd 6584* |
A reflexive, symmetric, transitive relation is an equivalence relation
on its domain. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised
by Mario Carneiro, 12-Aug-2015.)
|
⊢ (𝜑 → Rel 𝑅)
& ⊢ ((𝜑 ∧ 𝑥𝑅𝑦) → 𝑦𝑅𝑥)
& ⊢ ((𝜑 ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧)
& ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥)) ⇒ ⊢ (𝜑 → 𝑅 Er 𝐴) |
|
Theorem | brdifun 6585 |
Evaluate the incomparability relation. (Contributed by Mario Carneiro,
9-Jul-2014.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ <
)) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) |
|
Theorem | swoer 6586* |
Incomparability under a strict weak partial order is an equivalence
relation. (Contributed by Mario Carneiro, 9-Jul-2014.) (Revised by
Mario Carneiro, 12-Aug-2015.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Er 𝑋) |
|
Theorem | swoord1 6587* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶)) |
|
Theorem | swoord2 6588* |
The incomparability equivalence relation is compatible with the
original order. (Contributed by Mario Carneiro, 31-Dec-2014.)
|
⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦))
& ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋)
& ⊢ (𝜑 → 𝐶 ∈ 𝑋)
& ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵)) |
|
Theorem | eqerlem 6589* |
Lemma for eqer 6590. (Contributed by NM, 17-Mar-2008.) (Proof
shortened
by Mario Carneiro, 6-Dec-2016.)
|
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
& ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝐴 = 𝐵} ⇒ ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴) |
|
Theorem | eqer 6590* |
Equivalence relation involving equality of dependent classes 𝐴(𝑥)
and 𝐵(𝑦). (Contributed by NM, 17-Mar-2008.)
(Revised by Mario
Carneiro, 12-Aug-2015.)
|
⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵)
& ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝐴 = 𝐵} ⇒ ⊢ 𝑅 Er V |
|
Theorem | ider 6591 |
The identity relation is an equivalence relation. (Contributed by NM,
10-May-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof
shortened by Mario Carneiro, 9-Jul-2014.)
|
⊢ I Er V |
|
Theorem | 0er 6592 |
The empty set is an equivalence relation on the empty set. (Contributed
by Mario Carneiro, 5-Sep-2015.)
|
⊢ ∅ Er ∅ |
|
Theorem | eceq1 6593 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶) |
|
Theorem | eceq1d 6594 |
Equality theorem for equivalence class (deduction form). (Contributed
by Jim Kingdon, 31-Dec-2019.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) |
|
Theorem | eceq2 6595 |
Equality theorem for equivalence class. (Contributed by NM,
23-Jul-1995.)
|
⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵) |
|
Theorem | eceq2i 6596 |
Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶,
inference version. (Contributed by Peter Mazsa, 11-May-2021.)
|
⊢ 𝐴 = 𝐵 ⇒ ⊢ [𝐶]𝐴 = [𝐶]𝐵 |
|
Theorem | eceq2d 6597 |
Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶,
deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.)
|
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵) |
|
Theorem | elecg 6598 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by Mario Carneiro, 9-Jul-2014.)
|
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) |
|
Theorem | elec 6599 |
Membership in an equivalence class. Theorem 72 of [Suppes] p. 82.
(Contributed by NM, 23-Jul-1995.)
|
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈
V ⇒ ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴) |
|
Theorem | relelec 6600 |
Membership in an equivalence class when 𝑅 is a relation. (Contributed
by Mario Carneiro, 11-Sep-2015.)
|
⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) |