| Metamath
Proof Explorer Theorem List (p. 57 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 | ispod 5601* | Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.) |
| ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
| Theorem | swopolem 5602* | Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.) |
| ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌))) | ||
| Theorem | swopo 5603* | A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.) |
| ⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
| Theorem | poirr 5604 | A partial order is irreflexive. (Contributed by NM, 27-Mar-1997.) |
| ⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
| Theorem | potr 5605 | A partial order is a transitive relation. (Contributed by NM, 27-Mar-1997.) |
| ⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
| Theorem | po2nr 5606 | A partial order has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.) |
| ⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
| Theorem | po3nr 5607 | A partial order has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.) |
| ⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
| Theorem | po2ne 5608 | Two sets related by a partial order are not equal. (Contributed by AV, 13-Mar-2023.) |
| ⊢ ((𝑅 Po 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴𝑅𝐵) → 𝐴 ≠ 𝐵) | ||
| Theorem | po0 5609 | Any relation is a partial order on the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ 𝑅 Po ∅ | ||
| Theorem | pofun 5610* | The inverse image of a partial order is a partial order. (Contributed by Jeff Madsen, 18-Jun-2011.) |
| ⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ 𝑋𝑅𝑌} & ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌) ⇒ ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴) | ||
| Theorem | sopo 5611 | A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.) |
| ⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) | ||
| Theorem | soss 5612 | Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Or 𝐵 → 𝑅 Or 𝐴)) | ||
| Theorem | soeq1 5613 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
| ⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) | ||
| Theorem | soeq2 5614 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
| ⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) | ||
| Theorem | soeq12d 5615 | Equality deduction for total orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.) (Proof shortened by Matthew House, 10-Sep-2025.) |
| ⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐵)) | ||
| Theorem | sonr 5616 | A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.) |
| ⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
| Theorem | sotr 5617 | A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
| Theorem | sotrd 5618 | Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑅𝑌) & ⊢ (𝜑 → 𝑌𝑅𝑍) ⇒ ⊢ (𝜑 → 𝑋𝑅𝑍) | ||
| Theorem | solin 5619 | A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) | ||
| Theorem | so2nr 5620 | A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
| Theorem | so3nr 5621 | A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
| Theorem | sotric 5622 | A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) | ||
| Theorem | sotrieq 5623 | Trichotomy law for strict order relation. (Contributed by NM, 9-Apr-1996.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) | ||
| Theorem | sotrieq2 5624 | Trichotomy law for strict order relation. (Contributed by NM, 5-May-1999.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 ↔ (¬ 𝐵𝑅𝐶 ∧ ¬ 𝐶𝑅𝐵))) | ||
| Theorem | soasym 5625 | Asymmetry law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋𝑅𝑌 → ¬ 𝑌𝑅𝑋)) | ||
| Theorem | sotr2 5626 | A transitivity relation. (Read 𝐵 ≤ 𝐶 and 𝐶 < 𝐷 implies 𝐵 < 𝐷.) (Contributed by Mario Carneiro, 10-May-2013.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((¬ 𝐶𝑅𝐵 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
| Theorem | issod 5627* | An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝜑 → 𝑅 Po 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → 𝑅 Or 𝐴) | ||
| Theorem | issoi 5628* | An irreflexive, transitive, linear relation is a strict ordering. (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.) |
| ⊢ (𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ⇒ ⊢ 𝑅 Or 𝐴 | ||
| Theorem | isso2i 5629* | Deduce strict ordering from its properties. (Contributed by NM, 29-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.) |
| ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ 𝑅 Or 𝐴 | ||
| Theorem | so0 5630 | Any relation is a strict ordering of the empty set. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ 𝑅 Or ∅ | ||
| Theorem | somo 5631* | A totally ordered set has at most one minimal element. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by NM, 16-Jun-2017.) |
| ⊢ (𝑅 Or 𝐴 → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥) | ||
| Theorem | sotrine 5632 | Trichotomy law for strict orderings. (Contributed by Scott Fenton, 8-Dec-2021.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ≠ 𝐶 ↔ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) | ||
| Theorem | sotr3 5633 | Transitivity law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → ((𝑋𝑅𝑌 ∧ ¬ 𝑍𝑅𝑌) → 𝑋𝑅𝑍)) | ||
| Syntax | wfr 5634 | Extend wff notation to include the well-founded predicate. Read: "𝑅 is a well-founded relation on 𝐴". |
| wff 𝑅 Fr 𝐴 | ||
| Syntax | wse 5635 | Extend wff notation to include the set-like predicate. Read: "𝑅 is set-like on 𝐴". |
| wff 𝑅 Se 𝐴 | ||
| Syntax | wwe 5636 | Extend wff notation to include the well-ordering predicate. Read: "𝑅 well-orders 𝐴". |
| wff 𝑅 We 𝐴 | ||
| Definition | df-fr 5637* | Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5646 and dffr3 6117. A class is called well-founded when the membership relation E (see df-eprel 5584) is well-founded on it, that is, 𝐴 is well-founded if E Fr 𝐴 (some sources request that the membership relation be well-founded on its transitive closure). (Contributed by NM, 3-Apr-1994.) |
| ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦)) | ||
| Definition | df-se 5638* | Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.) |
| ⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) | ||
| Definition | df-we 5639 | Define the well-ordering predicate. For an alternate definition, see dfwe2 7794. (Contributed by NM, 3-Apr-1994.) |
| ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | ||
| Theorem | dffr6 5640* | Alternate definition of df-fr 5637. See dffr5 35754 for a definition without dummy variables (but note that their equivalence uses ax-sep 5296). (Contributed by BJ, 16-Nov-2024.) |
| ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥 ∈ (𝒫 𝐴 ∖ {∅})∃𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 ¬ 𝑧𝑅𝑦) | ||
| Theorem | frd 5641* | A nonempty subset of an 𝑅-well-founded class has an 𝑅-minimal element (deduction form). (Contributed by BJ, 16-Nov-2024.) |
| ⊢ (𝜑 → 𝑅 Fr 𝐴) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ≠ ∅) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
| Theorem | fri 5642* | A nonempty subset of an 𝑅-well-founded class has an 𝑅-minimal element (inference form). (Contributed by BJ, 16-Nov-2024.) (Proof shortened by BJ, 19-Nov-2024.) |
| ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
| Theorem | friOLD 5643* | Obsolete version of fri 5642 as of 16-Nov-2024. (Contributed by NM, 18-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
| Theorem | seex 5644* | The 𝑅-preimage of an element of the base set in a set-like relation is a set. (Contributed by Mario Carneiro, 19-Nov-2014.) |
| ⊢ ((𝑅 Se 𝐴 ∧ 𝐵 ∈ 𝐴) → {𝑥 ∈ 𝐴 ∣ 𝑥𝑅𝐵} ∈ V) | ||
| Theorem | exse 5645 | Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.) |
| ⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴) | ||
| Theorem | dffr2 5646* | Alternate definition of well-founded relation. Similar to Definition 6.21 of [TakeutiZaring] p. 30. (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Mario Carneiro, 23-Jun-2015.) Avoid ax-10 2141, ax-11 2157, ax-12 2177, but use ax-8 2110. (Revised by GG, 3-Oct-2024.) |
| ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 {𝑧 ∈ 𝑥 ∣ 𝑧𝑅𝑦} = ∅)) | ||
| Theorem | dffr2ALT 5647* | Alternate proof of dffr2 5646, which avoids ax-8 2110 but requires ax-10 2141, ax-11 2157, ax-12 2177. (Contributed by NM, 17-Feb-2004.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) (Proof shortened by Mario Carneiro, 23-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 {𝑧 ∈ 𝑥 ∣ 𝑧𝑅𝑦} = ∅)) | ||
| Theorem | frc 5648* | Property of well-founded relation (one direction of definition using class variables). (Contributed by NM, 17-Feb-2004.) (Revised by Mario Carneiro, 19-Nov-2014.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 {𝑦 ∈ 𝐵 ∣ 𝑦𝑅𝑥} = ∅) | ||
| Theorem | frss 5649 | Subset theorem for the well-founded predicate. Exercise 1 of [TakeutiZaring] p. 31. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Fr 𝐵 → 𝑅 Fr 𝐴)) | ||
| Theorem | sess1 5650 | Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
| ⊢ (𝑅 ⊆ 𝑆 → (𝑆 Se 𝐴 → 𝑅 Se 𝐴)) | ||
| Theorem | sess2 5651 | Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝑅 Se 𝐵 → 𝑅 Se 𝐴)) | ||
| Theorem | freq1 5652 | Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.) |
| ⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) | ||
| Theorem | freq2 5653 | Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.) |
| ⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵)) | ||
| Theorem | freq12d 5654 | Equality deduction for well-founded relations. (Contributed by Stefan O'Rear, 19-Jan-2015.) (Proof shortened by Matthew House, 10-Sep-2025.) |
| ⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐵)) | ||
| Theorem | seeq1 5655 | Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
| ⊢ (𝑅 = 𝑆 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴)) | ||
| Theorem | seeq2 5656 | Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
| ⊢ (𝐴 = 𝐵 → (𝑅 Se 𝐴 ↔ 𝑅 Se 𝐵)) | ||
| Theorem | seeq12d 5657 | Equality deduction for the set-like predicate. (Contributed by Matthew House, 10-Sep-2025.) |
| ⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐵)) | ||
| Theorem | nffr 5658 | Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Fr 𝐴 | ||
| Theorem | nfse 5659 | Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Se 𝐴 | ||
| Theorem | nfwe 5660 | Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 We 𝐴 | ||
| Theorem | frirr 5661 | A well-founded relation is irreflexive. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 2-Jan-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) |
| ⊢ ((𝑅 Fr 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
| Theorem | fr2nr 5662 | A well-founded relation has no 2-cycle loops. Special case of Proposition 6.23 of [TakeutiZaring] p. 30. (Contributed by NM, 30-May-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) |
| ⊢ ((𝑅 Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
| Theorem | fr0 5663 | Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.) |
| ⊢ 𝑅 Fr ∅ | ||
| Theorem | frminex 5664* | If an element of a well-founded set satisfies a property 𝜑, then there is a minimal element that satisfies 𝜑. (Contributed by Jeff Madsen, 18-Jun-2010.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
| ⊢ 𝐴 ∈ V & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ (𝑅 Fr 𝐴 → (∃𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → ¬ 𝑦𝑅𝑥)))) | ||
| Theorem | efrirr 5665 | A well-founded class does not belong to itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) |
| ⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴) | ||
| Theorem | efrn2lp 5666 | A well-founded class contains no 2-cycle loops. (Contributed by NM, 19-Apr-1994.) |
| ⊢ (( E Fr 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵 ∈ 𝐶 ∧ 𝐶 ∈ 𝐵)) | ||
| Theorem | epse 5667 | The membership relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the membership relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.) |
| ⊢ E Se 𝐴 | ||
| Theorem | tz7.2 5668 | Similar to Theorem 7.2 of [TakeutiZaring] p. 35, except that the Axiom of Regularity is not required due to the antecedent E Fr 𝐴. (Contributed by NM, 4-May-1994.) |
| ⊢ ((Tr 𝐴 ∧ E Fr 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴)) | ||
| Theorem | dfepfr 5669* | An alternate way of saying that the membership relation is well-founded. (Contributed by NM, 17-Feb-2004.) (Revised by Mario Carneiro, 23-Jun-2015.) |
| ⊢ ( E Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 (𝑥 ∩ 𝑦) = ∅)) | ||
| Theorem | epfrc 5670* | A subset of a well-founded class has a minimal element. (Contributed by NM, 17-Feb-2004.) (Revised by David Abernethy, 22-Feb-2011.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (( E Fr 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅) | ||
| Theorem | wess 5671 | Subset theorem for the well-ordering predicate. Exercise 4 of [TakeutiZaring] p. 31. (Contributed by NM, 19-Apr-1994.) |
| ⊢ (𝐴 ⊆ 𝐵 → (𝑅 We 𝐵 → 𝑅 We 𝐴)) | ||
| Theorem | weeq1 5672 | Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.) |
| ⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) | ||
| Theorem | weeq2 5673 | Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.) |
| ⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵)) | ||
| Theorem | weeq12d 5674 | Equality deduction for well-orderings. (Contributed by Stefan O'Rear, 19-Jan-2015.) (Proof shortened by Matthew House, 10-Sep-2025.) |
| ⊢ (𝜑 → 𝑅 = 𝑆) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐵)) | ||
| Theorem | wefr 5675 | A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.) |
| ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) | ||
| Theorem | weso 5676 | A well-ordering is a strict ordering. (Contributed by NM, 16-Mar-1997.) |
| ⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) | ||
| Theorem | wecmpep 5677 | The elements of a class well-ordered by membership are comparable. (Contributed by NM, 17-May-1994.) |
| ⊢ (( E We 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)) | ||
| Theorem | wetrep 5678 | On a class well-ordered by membership, the membership predicate is transitive. (Contributed by NM, 22-Apr-1994.) |
| ⊢ (( E We 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) | ||
| Theorem | wefrc 5679* | A nonempty subclass of a class well-ordered by membership has a minimal element. Special case of Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by NM, 17-Feb-2004.) |
| ⊢ (( E We 𝐴 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑥 ∈ 𝐵 (𝐵 ∩ 𝑥) = ∅) | ||
| Theorem | we0 5680 | Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.) |
| ⊢ 𝑅 We ∅ | ||
| Theorem | wereu 5681* | A nonempty subset of an 𝑅-well-ordered class has a unique 𝑅 -minimal element. (Contributed by NM, 18-Mar-1997.) (Revised by Mario Carneiro, 28-Apr-2015.) |
| ⊢ ((𝑅 We 𝐴 ∧ (𝐵 ∈ 𝑉 ∧ 𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
| Theorem | wereu2 5682* | A nonempty subclass of an 𝑅-well-ordered and 𝑅-setlike class has a unique 𝑅-minimal element. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 24-Jun-2015.) |
| ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃!𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
| Syntax | cxp 5683 | Extend the definition of a class to include the Cartesian product. |
| class (𝐴 × 𝐵) | ||
| Syntax | ccnv 5684 | Extend the definition of a class to include the converse of a class. |
| class ◡𝐴 | ||
| Syntax | cdm 5685 | Extend the definition of a class to include the domain of a class. |
| class dom 𝐴 | ||
| Syntax | crn 5686 | Extend the definition of a class to include the range of a class. |
| class ran 𝐴 | ||
| Syntax | cres 5687 | Extend the definition of a class to include the restriction of a class. Read: "the restriction of 𝐴 to 𝐵". |
| class (𝐴 ↾ 𝐵) | ||
| Syntax | cima 5688 | Extend the definition of a class to include the image of a class. Read: "the image of 𝐵 under 𝐴". |
| class (𝐴 “ 𝐵) | ||
| Syntax | ccom 5689 | Extend the definition of a class to include the composition of two classes. (Read: The composition of 𝐴 and 𝐵.) |
| class (𝐴 ∘ 𝐵) | ||
| Syntax | wrel 5690 | Extend the definition of a wff to include the relation predicate. Read: "𝐴 is a relation". |
| wff Rel 𝐴 | ||
| Definition | df-xp 5691* | Define the Cartesian product of two classes. This is also sometimes called the "cross product" but that term also has other meanings; we intentionally choose a less ambiguous term. Definition 9.11 of [Quine] p. 64. For example, ({1, 5} × {2, 7}) = ({〈1, 2〉, 〈1, 7〉} ∪ {〈5, 2〉, 〈5, 7〉}) (ex-xp 30455). Another example is that the set of rational numbers is defined in df-q 12991 using the Cartesian product (ℤ × ℕ); the left- and right-hand sides of the Cartesian product represent the top (integer) and bottom (natural) numbers of a fraction. (Contributed by NM, 4-Jul-1994.) |
| ⊢ (𝐴 × 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)} | ||
| Definition | df-rel 5692 | Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6209 and dfrel3 6218. (Contributed by NM, 1-Aug-1994.) |
| ⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V)) | ||
| Definition | df-cnv 5693* |
Define the converse of a class. Definition 9.12 of [Quine] p. 64. The
converse of a binary relation swaps its arguments, i.e., if 𝐴 ∈
V
and 𝐵 ∈ V then (𝐴◡𝑅𝐵 ↔ 𝐵𝑅𝐴), as proven in brcnv 5893
(see df-br 5144 and df-rel 5692 for more on relations). For example,
◡{〈2,
6〉, 〈3, 9〉} = {〈6, 2〉, 〈9, 3〉}
(ex-cnv 30456).
We use Quine's breve accent (smile) notation. Like Quine, we use it as a prefix, which eliminates the need for parentheses. "Converse" is Quine's terminology. Some authors use a "minus one" exponent and call it "inverse", especially when the argument is a function, although this is not in general a genuine inverse. (Contributed by NM, 4-Jul-1994.) |
| ⊢ ◡𝐴 = {〈𝑥, 𝑦〉 ∣ 𝑦𝐴𝑥} | ||
| Definition | df-co 5694* | Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. For example, ((exp ∘ cos)‘0) = e (ex-co 30457) because (cos‘0) = 1 (see cos0 16186) and (exp‘1) = e (see df-e 16104). Note that Definition 7 of [Suppes] p. 63 reverses 𝐴 and 𝐵, uses / instead of ∘, and calls the operation "relative product". (Contributed by NM, 4-Jul-1994.) |
| ⊢ (𝐴 ∘ 𝐵) = {〈𝑥, 𝑦〉 ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)} | ||
| Definition | df-dm 5695* | Define the domain of a class. Definition 3 of [Suppes] p. 59. For example, 𝐹 = {〈2, 6〉, 〈3, 9〉} → dom 𝐹 = {2, 3} (ex-dm 30458). Another example is the domain of the complex arctangent, (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ 𝐴 ≠ -i ∧ 𝐴 ≠ i)) (for proof see atandm 26919). Contrast with range (defined in df-rn 5696). For alternate definitions see dfdm2 6301, dfdm3 5898, and dfdm4 5906. The notation "dom " is used by Enderton; other authors sometimes use script D. (Contributed by NM, 1-Aug-1994.) |
| ⊢ dom 𝐴 = {𝑥 ∣ ∃𝑦 𝑥𝐴𝑦} | ||
| Definition | df-rn 5696 | Define the range of a class. For example, 𝐹 = {〈2, 6〉, 〈3, 9〉} → ran 𝐹 = {6, 9} (ex-rn 30459). Contrast with domain (defined in df-dm 5695). For alternate definitions, see dfrn2 5899, dfrn3 5900, and dfrn4 6222. The notation "ran " is used by Enderton. The range of a function is often also called "the image of the function" (see definition in [Lang] p. ix), which can be justified by imadmrn 6088. Not to be confused with "codomain" (see df-f 6565), which may be a superset/superclass of the range (see frn 6743). (Contributed by NM, 1-Aug-1994.) |
| ⊢ ran 𝐴 = dom ◡𝐴 | ||
| Definition | df-res 5697 | Define the restriction of a class. Definition 6.6(1) of [TakeutiZaring] p. 24. For example, the expression (exp ↾ ℝ) (used in reeff1 16156) means "the exponential function e to the x, but the exponent x must be in the reals" (df-ef 16103 defines the exponential function, which normally allows the exponent to be a complex number). Another example is (𝐹 = {〈2, 6〉, 〈3, 9〉} ∧ 𝐵 = {1, 2}) → (𝐹 ↾ 𝐵) = {〈2, 6〉} (ex-res 30460). We do not introduce a special syntax for the corestriction of a class: it will be expressed either as the intersection (𝐴 ∩ (V × 𝐵)) or as the converse of the restricted converse (see cnvrescnv 6215). (Contributed by NM, 2-Aug-1994.) |
| ⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × V)) | ||
| Definition | df-ima 5698 | Define the image of a class (as restricted by another class). Definition 6.6(2) of [TakeutiZaring] p. 24. For example, (𝐹 = {〈2, 6〉, 〈3, 9〉} ∧ 𝐵 = {1, 2}) → (𝐹 “ 𝐵) = {6} (ex-ima 30461). Contrast with restriction (df-res 5697) and range (df-rn 5696). For an alternate definition, see dfima2 6080. (Contributed by NM, 2-Aug-1994.) |
| ⊢ (𝐴 “ 𝐵) = ran (𝐴 ↾ 𝐵) | ||
| Theorem | xpeq1 5699 | Equality theorem for Cartesian product. (Contributed by NM, 4-Jul-1994.) |
| ⊢ (𝐴 = 𝐵 → (𝐴 × 𝐶) = (𝐵 × 𝐶)) | ||
| Theorem | xpss12 5700 | Subset theorem for Cartesian product. Generalization of Theorem 101 of [Suppes] p. 52. (Contributed by NM, 26-Aug-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
| ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 × 𝐶) ⊆ (𝐵 × 𝐷)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |