| Metamath
Proof Explorer Theorem List (p. 88 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | nnasmo 8701* | There is at most one left additive inverse for natural number addition. (Contributed by Scott Fenton, 17-Oct-2024.) |
| ⊢ (𝐴 ∈ ω → ∃*𝑥 ∈ ω (𝐴 +o 𝑥) = 𝐵) | ||
| Theorem | eldifsucnn 8702* | Condition for membership in the difference of ω and a nonzero finite ordinal. (Contributed by Scott Fenton, 24-Oct-2024.) |
| ⊢ (𝐴 ∈ ω → (𝐵 ∈ (ω ∖ suc 𝐴) ↔ ∃𝑥 ∈ (ω ∖ 𝐴)𝐵 = suc 𝑥)) | ||
| Syntax | cnadd 8703 | Declare the syntax for natural ordinal addition. See df-nadd 8704. |
| class +no | ||
| Definition | df-nadd 8704* | Define natural ordinal addition. This is a commutative form of addition over the ordinals. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ +no = frecs({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), (𝑧 ∈ V, 𝑎 ∈ V ↦ ∩ {𝑤 ∈ On ∣ ((𝑎 “ ({(1st ‘𝑧)} × (2nd ‘𝑧))) ⊆ 𝑤 ∧ (𝑎 “ ((1st ‘𝑧) × {(2nd ‘𝑧)})) ⊆ 𝑤)})) | ||
| Theorem | on2recsfn 8705* | Show that double recursion over ordinals yields a function over pairs of ordinals. (Contributed by Scott Fenton, 3-Sep-2024.) |
| ⊢ 𝐹 = frecs({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 𝐺) ⇒ ⊢ 𝐹 Fn (On × On) | ||
| Theorem | on2recsov 8706* | Calculate the value of the double ordinal recursion operator. (Contributed by Scott Fenton, 3-Sep-2024.) |
| ⊢ 𝐹 = frecs({〈𝑥, 𝑦〉 ∣ (𝑥 ∈ (On × On) ∧ 𝑦 ∈ (On × On) ∧ (((1st ‘𝑥) E (1st ‘𝑦) ∨ (1st ‘𝑥) = (1st ‘𝑦)) ∧ ((2nd ‘𝑥) E (2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}, (On × On), 𝐺) ⇒ ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐹𝐵) = (〈𝐴, 𝐵〉𝐺(𝐹 ↾ ((suc 𝐴 × suc 𝐵) ∖ {〈𝐴, 𝐵〉})))) | ||
| Theorem | on2ind 8707* | Double induction over ordinal numbers. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ (𝑎 = 𝑐 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝑑 → (𝜓 ↔ 𝜒)) & ⊢ (𝑎 = 𝑐 → (𝜃 ↔ 𝜒)) & ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜏)) & ⊢ (𝑏 = 𝑌 → (𝜏 ↔ 𝜂)) & ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On) → ((∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑏 𝜒 ∧ ∀𝑐 ∈ 𝑎 𝜓 ∧ ∀𝑑 ∈ 𝑏 𝜃) → 𝜑)) ⇒ ⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ On) → 𝜂) | ||
| Theorem | on3ind 8708* | Triple induction over ordinals. (Contributed by Scott Fenton, 4-Sep-2024.) |
| ⊢ (𝑎 = 𝑑 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝑒 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝑓 → (𝜒 ↔ 𝜃)) & ⊢ (𝑎 = 𝑑 → (𝜏 ↔ 𝜃)) & ⊢ (𝑏 = 𝑒 → (𝜂 ↔ 𝜏)) & ⊢ (𝑏 = 𝑒 → (𝜁 ↔ 𝜃)) & ⊢ (𝑐 = 𝑓 → (𝜎 ↔ 𝜏)) & ⊢ (𝑎 = 𝑋 → (𝜑 ↔ 𝜌)) & ⊢ (𝑏 = 𝑌 → (𝜌 ↔ 𝜇)) & ⊢ (𝑐 = 𝑍 → (𝜇 ↔ 𝜆)) & ⊢ ((𝑎 ∈ On ∧ 𝑏 ∈ On ∧ 𝑐 ∈ On) → (((∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜃 ∧ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑏 𝜒 ∧ ∀𝑑 ∈ 𝑎 ∀𝑓 ∈ 𝑐 𝜁) ∧ (∀𝑑 ∈ 𝑎 𝜓 ∧ ∀𝑒 ∈ 𝑏 ∀𝑓 ∈ 𝑐 𝜏 ∧ ∀𝑒 ∈ 𝑏 𝜎) ∧ ∀𝑓 ∈ 𝑐 𝜂) → 𝜑)) ⇒ ⊢ ((𝑋 ∈ On ∧ 𝑌 ∈ On ∧ 𝑍 ∈ On) → 𝜆) | ||
| Theorem | coflton 8709* | Cofinality theorem for ordinals. If 𝐴 is cofinal with 𝐵 and 𝐵 precedes 𝐶, then 𝐴 precedes 𝐶. Compare cofsslt 27952 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ⊆ On) & ⊢ (𝜑 → 𝐵 ⊆ On) & ⊢ (𝜑 → 𝐶 ⊆ On) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∀𝑤 ∈ 𝐶 𝑧 ∈ 𝑤) ⇒ ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐶 𝑎 ∈ 𝑐) | ||
| Theorem | cofon1 8710* | Cofinality theorem for ordinals. If 𝐴 is cofinal with 𝐵 and the upper bound of 𝐴 dominates 𝐵, then their upper bounds are equal. Compare with cofcut1 27954 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝒫 On) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) & ⊢ (𝜑 → 𝐵 ⊆ ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧}) ⇒ ⊢ (𝜑 → ∩ {𝑧 ∈ On ∣ 𝐴 ⊆ 𝑧} = ∩ {𝑤 ∈ On ∣ 𝐵 ⊆ 𝑤}) | ||
| Theorem | cofon2 8711* | Cofinality theorem for ordinals. If 𝐴 and 𝐵 are mutually cofinal, then their upper bounds agree. Compare cofcut2 27956 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝒫 On) & ⊢ (𝜑 → 𝐵 ∈ 𝒫 On) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝑥 ⊆ 𝑦) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐵 ∃𝑤 ∈ 𝐴 𝑧 ⊆ 𝑤) ⇒ ⊢ (𝜑 → ∩ {𝑎 ∈ On ∣ 𝐴 ⊆ 𝑎} = ∩ {𝑏 ∈ On ∣ 𝐵 ⊆ 𝑏}) | ||
| Theorem | cofonr 8712* | Inverse cofinality law for ordinals. Contrast with cofcutr 27958 for surreals. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥}) ⇒ ⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝑋 𝑦 ⊆ 𝑧) | ||
| Theorem | naddfn 8713 | Natural addition is a function over pairs of ordinals. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ +no Fn (On × On) | ||
| Theorem | naddcllem 8714* | Lemma for ordinal addition closure. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +no 𝐵) ∈ On ∧ (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)})) | ||
| Theorem | naddcl 8715 | Closure law for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) ∈ On) | ||
| Theorem | naddov 8716* | The value of natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ⊆ 𝑥 ∧ ( +no “ (𝐴 × {𝐵})) ⊆ 𝑥)}) | ||
| Theorem | naddov2 8717* | Alternate expression for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (∀𝑦 ∈ 𝐵 (𝐴 +no 𝑦) ∈ 𝑥 ∧ ∀𝑧 ∈ 𝐴 (𝑧 +no 𝐵) ∈ 𝑥)}) | ||
| Theorem | naddov3 8718* | Alternate expression for natural addition. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = ∩ {𝑥 ∈ On ∣ (( +no “ ({𝐴} × 𝐵)) ∪ ( +no “ (𝐴 × {𝐵}))) ⊆ 𝑥}) | ||
| Theorem | naddf 8719 | Function statement for natural addition. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ +no :(On × On)⟶On | ||
| Theorem | naddcom 8720 | Natural addition commutes. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no 𝐵) = (𝐵 +no 𝐴)) | ||
| Theorem | naddrid 8721 | Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 26-Aug-2024.) |
| ⊢ (𝐴 ∈ On → (𝐴 +no ∅) = 𝐴) | ||
| Theorem | naddlid 8722 | Ordinal zero is the additive identity for natural addition. (Contributed by Scott Fenton, 20-Feb-2025.) |
| ⊢ (𝐴 ∈ On → (∅ +no 𝐴) = 𝐴) | ||
| Theorem | naddssim 8723 | Ordinal less-than-or-equal is preserved by natural addition. (Contributed by Scott Fenton, 7-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 → (𝐴 +no 𝐶) ⊆ (𝐵 +no 𝐶))) | ||
| Theorem | naddelim 8724 | Ordinal less-than is preserved by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 → (𝐴 +no 𝐶) ∈ (𝐵 +no 𝐶))) | ||
| Theorem | naddel1 8725 | Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐴 +no 𝐶) ∈ (𝐵 +no 𝐶))) | ||
| Theorem | naddel2 8726 | Ordinal less-than is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ∈ 𝐵 ↔ (𝐶 +no 𝐴) ∈ (𝐶 +no 𝐵))) | ||
| Theorem | naddss1 8727 | Ordinal less-than-or-equal is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐴 +no 𝐶) ⊆ (𝐵 +no 𝐶))) | ||
| Theorem | naddss2 8728 | Ordinal less-than-or-equal is not affected by natural addition. (Contributed by Scott Fenton, 9-Sep-2024.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ⊆ 𝐵 ↔ (𝐶 +no 𝐴) ⊆ (𝐶 +no 𝐵))) | ||
| Theorem | naddword1 8729 | Weak-ordering principle for natural addition. (Contributed by Scott Fenton, 21-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐴 +no 𝐵)) | ||
| Theorem | naddword2 8730 | Weak-ordering principle for natural addition. (Contributed by Scott Fenton, 15-Feb-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ⊆ (𝐵 +no 𝐴)) | ||
| Theorem | naddunif 8731* | Uniformity theorem for natural addition. If 𝐴 is the upper bound of 𝑋 and 𝐵 is the upper bound of 𝑌, then (𝐴 +no 𝐵) can be expressed in terms of 𝑋 and 𝑌. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → 𝐵 ∈ On) & ⊢ (𝜑 → 𝐴 = ∩ {𝑥 ∈ On ∣ 𝑋 ⊆ 𝑥}) & ⊢ (𝜑 → 𝐵 = ∩ {𝑦 ∈ On ∣ 𝑌 ⊆ 𝑦}) ⇒ ⊢ (𝜑 → (𝐴 +no 𝐵) = ∩ {𝑧 ∈ On ∣ (( +no “ (𝑋 × {𝐵})) ∪ ( +no “ ({𝐴} × 𝑌))) ⊆ 𝑧}) | ||
| Theorem | naddasslem1 8732* | Lemma for naddass 8734. Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) +no 𝐶) = ∩ {𝑥 ∈ On ∣ (∀𝑎 ∈ 𝐴 ((𝑎 +no 𝐵) +no 𝐶) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝐵 ((𝐴 +no 𝑏) +no 𝐶) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝐶 ((𝐴 +no 𝐵) +no 𝑐) ∈ 𝑥)}) | ||
| Theorem | naddasslem2 8733* | Lemma for naddass 8734. Expand out the expression for natural addition of three arguments. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 +no (𝐵 +no 𝐶)) = ∩ {𝑥 ∈ On ∣ (∀𝑎 ∈ 𝐴 (𝑎 +no (𝐵 +no 𝐶)) ∈ 𝑥 ∧ ∀𝑏 ∈ 𝐵 (𝐴 +no (𝑏 +no 𝐶)) ∈ 𝑥 ∧ ∀𝑐 ∈ 𝐶 (𝐴 +no (𝐵 +no 𝑐)) ∈ 𝑥)}) | ||
| Theorem | naddass 8734 | Natural ordinal addition is associative. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) +no 𝐶) = (𝐴 +no (𝐵 +no 𝐶))) | ||
| Theorem | nadd32 8735 | Commutative/associative law that swaps the last two terms in a triple sum. (Contributed by Scott Fenton, 20-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +no 𝐵) +no 𝐶) = ((𝐴 +no 𝐶) +no 𝐵)) | ||
| Theorem | nadd4 8736 | Rearragement of terms in a quadruple sum. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ((𝐴 +no 𝐵) +no (𝐶 +no 𝐷)) = ((𝐴 +no 𝐶) +no (𝐵 +no 𝐷))) | ||
| Theorem | nadd42 8737 | Rearragement of terms in a quadruple sum. (Contributed by Scott Fenton, 5-Feb-2025.) |
| ⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐶 ∈ On ∧ 𝐷 ∈ On)) → ((𝐴 +no 𝐵) +no (𝐶 +no 𝐷)) = ((𝐴 +no 𝐶) +no (𝐷 +no 𝐵))) | ||
| Theorem | naddel12 8738 | Natural addition to both sides of ordinal less-than. (Contributed by Scott Fenton, 7-Feb-2025.) |
| ⊢ ((𝐶 ∈ On ∧ 𝐷 ∈ On) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (𝐴 +no 𝐵) ∈ (𝐶 +no 𝐷))) | ||
| Theorem | naddsuc2 8739 | Natural addition with successor. (Contributed by RP, 1-Jan-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +no suc 𝐵) = suc (𝐴 +no 𝐵)) | ||
| Theorem | naddoa 8740 | Natural addition of a natural is the same as regular addition. (Contributed by Scott Fenton, 20-Aug-2025.) |
| ⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ ω) → (𝐴 +no 𝐵) = (𝐴 +o 𝐵)) | ||
| Theorem | omnaddcl 8741 | The naturals are closed under natural addition. (Contributed by Scott Fenton, 20-Aug-2025.) |
| ⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 +no 𝐵) ∈ ω) | ||
| Syntax | wer 8742 | Extend the definition of a wff to include the equivalence predicate. |
| wff 𝑅 Er 𝐴 | ||
| Syntax | cec 8743 | Extend the definition of a class to include equivalence class. |
| class [𝐴]𝑅 | ||
| Syntax | cqs 8744 | Extend the definition of a class to include quotient set. |
| class (𝐴 / 𝑅) | ||
| Definition | df-er 8745 | 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 8746 we derive a more typical definition. We show that an equivalence relation is reflexive, symmetric, and transitive in erref 8765, ersymb 8759, and ertr 8760. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 2-Nov-2015.) |
| ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ (◡𝑅 ∪ (𝑅 ∘ 𝑅)) ⊆ 𝑅)) | ||
| Theorem | dfer2 8746* | Alternate definition of equivalence predicate. (Contributed by NM, 3-Jan-1997.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝑅 Er 𝐴 ↔ (Rel 𝑅 ∧ dom 𝑅 = 𝐴 ∧ ∀𝑥∀𝑦∀𝑧((𝑥𝑅𝑦 → 𝑦𝑅𝑥) ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))) | ||
| Definition | df-ec 8747 | 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 8746). 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 8748. (Contributed by NM, 23-Jul-1995.) |
| ⊢ [𝐴]𝑅 = (𝑅 “ {𝐴}) | ||
| Theorem | dfec2 8748* | 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 8749 | An equivalence class modulo a set is a set. (Contributed by NM, 24-Jul-1995.) |
| ⊢ (𝑅 ∈ 𝐵 → [𝐴]𝑅 ∈ V) | ||
| Theorem | ecexr 8750 | A nonempty equivalence class implies the representative is a set. (Contributed by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝐴 ∈ [𝐵]𝑅 → 𝐵 ∈ V) | ||
| Definition | df-qs 8751* | Define quotient set. 𝑅 is usually an equivalence relation. Definition of [Enderton] p. 58. (Contributed by NM, 23-Jul-1995.) |
| ⊢ (𝐴 / 𝑅) = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = [𝑥]𝑅} | ||
| Theorem | ereq1 8752 | Equality theorem for equivalence predicate. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝑅 = 𝑆 → (𝑅 Er 𝐴 ↔ 𝑆 Er 𝐴)) | ||
| Theorem | ereq2 8753 | Equality theorem for equivalence predicate. (Contributed by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝐴 = 𝐵 → (𝑅 Er 𝐴 ↔ 𝑅 Er 𝐵)) | ||
| Theorem | errel 8754 | An equivalence relation is a relation. (Contributed by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝑅 Er 𝐴 → Rel 𝑅) | ||
| Theorem | erdm 8755 | The domain of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝑅 Er 𝐴 → dom 𝑅 = 𝐴) | ||
| Theorem | ercl 8756 | Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴 ∈ 𝑋) | ||
| Theorem | ersym 8757 | An equivalence relation is symmetric. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵𝑅𝐴) | ||
| Theorem | ercl2 8758 | Elementhood in the field of an equivalence relation. (Contributed by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐵 ∈ 𝑋) | ||
| Theorem | ersymb 8759 | An equivalence relation is symmetric. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ 𝐵𝑅𝐴)) | ||
| Theorem | ertr 8760 | An equivalence relation is transitive. (Contributed by NM, 4-Jun-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶)) | ||
| Theorem | ertrd 8761 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
| Theorem | ertr2d 8762 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐶𝑅𝐴) | ||
| Theorem | ertr3d 8763 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐵𝑅𝐴) & ⊢ (𝜑 → 𝐵𝑅𝐶) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
| Theorem | ertr4d 8764 | A transitivity relation for equivalences. (Contributed by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) & ⊢ (𝜑 → 𝐶𝑅𝐵) ⇒ ⊢ (𝜑 → 𝐴𝑅𝐶) | ||
| Theorem | erref 8765 | 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 8766 | The converse of an equivalence relation is itself. (Contributed by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝑅 Er 𝐴 → ◡𝑅 = 𝑅) | ||
| Theorem | errn 8767 | 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 8768 | An equivalence relation is a subset of the cartesian product of the field. (Contributed by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝑅 Er 𝐴 → 𝑅 ⊆ (𝐴 × 𝐴)) | ||
| Theorem | erex 8769 | 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 8770 | 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 8771* | 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 | iseri 8772* | A reflexive, symmetric, transitive relation is an equivalence relation on its domain. Inference version of iserd 8771, which avoids the need to provide a "dummy antecedent" 𝜑 if there is no natural one to choose. (Contributed by AV, 30-Apr-2021.) |
| ⊢ Rel 𝑅 & ⊢ (𝑥𝑅𝑦 → 𝑦𝑅𝑥) & ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) & ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥) ⇒ ⊢ 𝑅 Er 𝐴 | ||
| Theorem | iseriALT 8773* | Alternate proof of iseri 8772, avoiding the usage of mptru 1547 and ⊤ as antecedent by using ax-mp 5 and one of the hypotheses as antecedent. This results, however, in a slightly longer proof. (Contributed by AV, 30-Apr-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ Rel 𝑅 & ⊢ (𝑥𝑅𝑦 → 𝑦𝑅𝑥) & ⊢ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) & ⊢ (𝑥 ∈ 𝐴 ↔ 𝑥𝑅𝑥) ⇒ ⊢ 𝑅 Er 𝐴 | ||
| Theorem | brinxper 8774* | Conditions for a reflexive, symmetric and transitive binary relation to be an equivalence relation over a class 𝑉. (Contributed by AV, 11-Jun-2025.) |
| ⊢ (𝑥 ∈ 𝑉 → 𝑥 ∼ 𝑥) & ⊢ (𝑥 ∈ 𝑉 → (𝑥 ∼ 𝑦 → 𝑦 ∼ 𝑥)) & ⊢ (𝑥 ∈ 𝑉 → ((𝑥 ∼ 𝑦 ∧ 𝑦 ∼ 𝑧) → 𝑥 ∼ 𝑧)) ⇒ ⊢ ( ∼ ∩ (𝑉 × 𝑉)) Er 𝑉 | ||
| Theorem | brdifun 8775 | Evaluate the incomparability relation. (Contributed by Mario Carneiro, 9-Jul-2014.) |
| ⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ↔ ¬ (𝐴 < 𝐵 ∨ 𝐵 < 𝐴))) | ||
| Theorem | swoer 8776* | 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 8777* | The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.) |
| ⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶)) | ||
| Theorem | swoord2 8778* | The incomparability equivalence relation is compatible with the original order. (Contributed by Mario Carneiro, 31-Dec-2014.) |
| ⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) & ⊢ (𝜑 → 𝐶 ∈ 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → (𝐶 < 𝐴 ↔ 𝐶 < 𝐵)) | ||
| Theorem | swoso 8779* | If the incomparability relation is equivalent to equality in a subset, then the partial order strictly orders the subset. (Contributed by Mario Carneiro, 30-Dec-2014.) |
| ⊢ 𝑅 = ((𝑋 × 𝑋) ∖ ( < ∪ ◡ < )) & ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 < 𝑧 → ¬ 𝑧 < 𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑥 < 𝑦 → (𝑥 < 𝑧 ∨ 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝑌 ⊆ 𝑋) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ∧ 𝑥𝑅𝑦)) → 𝑥 = 𝑦) ⇒ ⊢ (𝜑 → < Or 𝑌) | ||
| Theorem | eqerlem 8780* | Lemma for eqer 8781. (Contributed by NM, 17-Mar-2008.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) |
| ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝐴 = 𝐵} ⇒ ⊢ (𝑧𝑅𝑤 ↔ ⦋𝑧 / 𝑥⦌𝐴 = ⦋𝑤 / 𝑥⦌𝐴) | ||
| Theorem | eqer 8781* | Equivalence relation involving equality of dependent classes 𝐴(𝑥) and 𝐵(𝑦). (Contributed by NM, 17-Mar-2008.) (Revised by Mario Carneiro, 12-Aug-2015.) (Proof shortened by AV, 1-May-2021.) |
| ⊢ (𝑥 = 𝑦 → 𝐴 = 𝐵) & ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝐴 = 𝐵} ⇒ ⊢ 𝑅 Er V | ||
| Theorem | ider 8782 | 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 8783 | The empty set is an equivalence relation on the empty set. (Contributed by Mario Carneiro, 5-Sep-2015.) (Proof shortened by AV, 1-May-2021.) |
| ⊢ ∅ Er ∅ | ||
| Theorem | eceq1 8784 | Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.) |
| ⊢ (𝐴 = 𝐵 → [𝐴]𝐶 = [𝐵]𝐶) | ||
| Theorem | eceq1d 8785 | Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝐶 = [𝐵]𝐶) | ||
| Theorem | eceq2 8786 | Equality theorem for equivalence class. (Contributed by NM, 23-Jul-1995.) |
| ⊢ (𝐴 = 𝐵 → [𝐶]𝐴 = [𝐶]𝐵) | ||
| Theorem | eceq2i 8787 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, inference version. (Contributed by Peter Mazsa, 11-May-2021.) |
| ⊢ 𝐴 = 𝐵 ⇒ ⊢ [𝐶]𝐴 = [𝐶]𝐵 | ||
| Theorem | eceq2d 8788 | Equality theorem for the 𝐴-coset and 𝐵-coset of 𝐶, deduction version. (Contributed by Peter Mazsa, 23-Apr-2021.) |
| ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → [𝐶]𝐴 = [𝐶]𝐵) | ||
| Theorem | elecg 8789 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by Mario Carneiro, 9-Jul-2014.) |
| ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | ||
| Theorem | ecref 8790 | All elements are in their own equivalence class. (Contributed by Thierry Arnoux, 14-Feb-2025.) |
| ⊢ ((𝑅 Er 𝑋 ∧ 𝐴 ∈ 𝑋) → 𝐴 ∈ [𝐴]𝑅) | ||
| Theorem | elec 8791 | Membership in an equivalence class. Theorem 72 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) |
| ⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴) | ||
| Theorem | relelec 8792 | Membership in an equivalence class when 𝑅 is a relation. (Contributed by Mario Carneiro, 11-Sep-2015.) |
| ⊢ (Rel 𝑅 → (𝐴 ∈ [𝐵]𝑅 ↔ 𝐵𝑅𝐴)) | ||
| Theorem | ecss 8793 | An equivalence class is a subset of the domain. (Contributed by NM, 6-Aug-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) ⇒ ⊢ (𝜑 → [𝐴]𝑅 ⊆ 𝑋) | ||
| Theorem | ecdmn0 8794 | A representative of a nonempty equivalence class belongs to the domain of the equivalence relation. (Contributed by NM, 15-Feb-1996.) (Revised by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝐴 ∈ dom 𝑅 ↔ [𝐴]𝑅 ≠ ∅) | ||
| Theorem | ereldm 8795 | Equality of equivalence classes implies equivalence of domain membership. (Contributed by NM, 28-Jan-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅) ⇒ ⊢ (𝜑 → (𝐴 ∈ 𝑋 ↔ 𝐵 ∈ 𝑋)) | ||
| Theorem | erth 8796 | Basic property of equivalence relations. Theorem 73 of [Suppes] p. 82. (Contributed by NM, 23-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅)) | ||
| Theorem | erth2 8797 | Basic property of equivalence relations. Compare Theorem 73 of [Suppes] p. 82. Assumes membership of the second argument in the domain. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐴𝑅𝐵 ↔ [𝐴]𝑅 = [𝐵]𝑅)) | ||
| Theorem | erthi 8798 | Basic property of equivalence relations. Part of Lemma 3N of [Enderton] p. 57. (Contributed by NM, 30-Jul-1995.) (Revised by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝜑 → 𝑅 Er 𝑋) & ⊢ (𝜑 → 𝐴𝑅𝐵) ⇒ ⊢ (𝜑 → [𝐴]𝑅 = [𝐵]𝑅) | ||
| Theorem | erdisj 8799 | Equivalence classes do not overlap. In other words, two equivalence classes are either equal or disjoint. Theorem 74 of [Suppes] p. 83. (Contributed by NM, 15-Jun-2004.) (Revised by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝑅 Er 𝑋 → ([𝐴]𝑅 = [𝐵]𝑅 ∨ ([𝐴]𝑅 ∩ [𝐵]𝑅) = ∅)) | ||
| Theorem | ecidsn 8800 | An equivalence class modulo the identity relation is a singleton. (Contributed by NM, 24-Oct-2004.) |
| ⊢ [𝐴] I = {𝐴} | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |