![]() |
Metamath
Proof Explorer Theorem List (p. 55 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ssopab2b 5401 | Equivalence of ordered pair abstraction subclass and implication. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker ssopab2bw 5399 when possible. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) (New usage is discouraged.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) | ||
Theorem | ssopab2i 5402 | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} | ||
Theorem | ssopab2dv 5403* | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜒}) | ||
Theorem | eqopab2b 5404 | Equivalence of ordered pair abstraction equality and biconditional. Usage of this theorem is discouraged because it depends on ax-13 2379. Use the weaker eqopab2bw 5400 when possible. (Contributed by Mario Carneiro, 4-Jan-2017.) (New usage is discouraged.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓)) | ||
Theorem | opabn0 5405 | Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥∃𝑦𝜑) | ||
Theorem | opab0 5406 | Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = ∅ ↔ ∀𝑥∀𝑦 ¬ 𝜑) | ||
Theorem | csbopab 5407* | Move substitution into a class abstraction. Version of csbopabgALT 5408 without a sethood antecedent but depending on more axioms. (Contributed by NM, 6-Aug-2007.) (Revised by NM, 23-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{〈𝑦, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ [𝐴 / 𝑥]𝜑} | ||
Theorem | csbopabgALT 5408* | Move substitution into a class abstraction. Version of csbopab 5407 with a sethood antecedent but depending on fewer axioms. (Contributed by NM, 6-Aug-2007.) (Proof shortened by Mario Carneiro, 17-Nov-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌{〈𝑦, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ [𝐴 / 𝑥]𝜑}) | ||
Theorem | csbmpt12 5409* | Move substitution into a maps-to notation. (Contributed by AV, 26-Sep-2019.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍)) | ||
Theorem | csbmpt2 5410* | Move substitution into the second part of a maps-to notation. (Contributed by AV, 26-Sep-2019.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ 𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍)) | ||
Theorem | iunopab 5411* | Move indexed union inside an ordered-pair class abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ ∪ 𝑧 ∈ 𝐴 {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 𝜑} | ||
Theorem | elopabr 5412* | Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} → 𝐴 ∈ 𝑅) | ||
Theorem | elopabran 5413* | Membership in an ordered-pair class abstraction defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} → 𝐴 ∈ 𝑅) | ||
Theorem | rbropapd 5414* | Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
⊢ (𝜑 → 𝑀 = {〈𝑓, 𝑝〉 ∣ (𝑓𝑊𝑝 ∧ 𝜓)}) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒)))) | ||
Theorem | rbropap 5415* | Properties of a pair in a restricted binary relation 𝑀 expressed as an ordered-pair class abstraction: 𝑀 is the binary relation 𝑊 restricted by the condition 𝜓. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝜑 → 𝑀 = {〈𝑓, 𝑝〉 ∣ (𝑓𝑊𝑝 ∧ 𝜓)}) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒))) | ||
Theorem | 2rbropap 5416* | Properties of a pair in a restricted binary relation 𝑀 expressed as an ordered-pair class abstraction: 𝑀 is the binary relation 𝑊 restricted by the conditions 𝜓 and 𝜏. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝜑 → 𝑀 = {〈𝑓, 𝑝〉 ∣ (𝑓𝑊𝑝 ∧ 𝜓 ∧ 𝜏)}) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒)) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜏 ↔ 𝜃)) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒 ∧ 𝜃))) | ||
Theorem | 0nelopab 5417 | The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
⊢ ¬ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | brabv 5418 | If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
⊢ (𝑋{〈𝑥, 𝑦〉 ∣ 𝜑}𝑌 → (𝑋 ∈ V ∧ 𝑌 ∈ V)) | ||
Theorem | pwin 5419 | The power class of the intersection of two classes is the intersection of their power classes. Exercise 4.12(j) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) |
⊢ 𝒫 (𝐴 ∩ 𝐵) = (𝒫 𝐴 ∩ 𝒫 𝐵) | ||
Theorem | pwunssOLD 5420 | Obsolete version of pwunss 4517 as of 30-Dec-2023. (Contributed by NM, 23-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵) | ||
Theorem | pwssun 5421 | The power class of the union of two classes is a subset of the union of their power classes, iff one class is a subclass of the other. Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ 𝒫 (𝐴 ∪ 𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵)) | ||
Theorem | pwundifOLD 5422 | Obsolete proof of pwundif 4523 as of 26-Dec-2023. (Contributed by NM, 25-Mar-2007.) (Proof shortened by Thierry Arnoux, 20-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝒫 (𝐴 ∪ 𝐵) = ((𝒫 (𝐴 ∪ 𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) | ||
Theorem | pwun 5423 | The power class of the union of two classes equals the union of their power classes, iff one class is a subclass of the other. Part of Exercise 7(b) of [Enderton] p. 28. (Contributed by NM, 23-Nov-2003.) |
⊢ ((𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴) ↔ 𝒫 (𝐴 ∪ 𝐵) = (𝒫 𝐴 ∪ 𝒫 𝐵)) | ||
Syntax | cid 5424 | Extend the definition of a class to include the identity relation. |
class I | ||
Definition | df-id 5425* | Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 I 5 and ¬ 4 I 5 (ex-id 28219). (Contributed by NM, 13-Aug-1995.) |
⊢ I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} | ||
Theorem | dfid4 5426 | The identity function expressed using maps-to notation. (Contributed by Scott Fenton, 15-Dec-2017.) |
⊢ I = (𝑥 ∈ V ↦ 𝑥) | ||
Theorem | dfid3 5427 | A stronger version of df-id 5425 that does not require 𝑥 and 𝑦 to be disjoint. This is not the "official" definition since our definition soundness check without this requirement would be much more complex. The proof can be instructive in showing how disjoint variable requirements may be eliminated, a task that is not necessarily obvious. (Contributed by NM, 5-Feb-2008.) (Revised by Mario Carneiro, 18-Nov-2016.) Use directly the definition df-id 5425 when sufficient, since the derivation of dfid3 5427 is nontrivial and uses auxiliary axioms ax-10 2142 to ax-13 2379. (New usage is discouraged.) |
⊢ I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} | ||
Theorem | dfid2 5428 | Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.) Use df-id 5425 when sufficient (see comment at dfid3 5427). (New usage is discouraged.) |
⊢ I = {〈𝑥, 𝑥〉 ∣ 𝑥 = 𝑥} | ||
Syntax | cep 5429 | Extend class notation to include the membership relation. |
class E | ||
Definition | df-eprel 5430* | Define the membership relation (also called "epsilon relation" since it is sometimes denoted by the lowercase Greek letter "epsilon"). Similar to Definition 6.22 of [TakeutiZaring] p. 30. The membership relation and the membership predicate agree, that is, (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵), when 𝐵 is a set (see epelg 5431). Thus, ⊢ 5 E {1, 5} (ex-eprel 28218). (Contributed by NM, 13-Aug-1995.) |
⊢ E = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ 𝑦} | ||
Theorem | epelg 5431 | The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5433 and closed form of epeli 5432. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof shortened by BJ, 14-Jul-2023.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | epeli 5432 | The membership relation and the membership predicate agree when the "containing" class is a set. Inference associated with epelg 5431. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | epel 5433 | The membership relation and the membership predicate agree when the "containing" class is a setvar. (Contributed by NM, 13-Aug-1995.) Replace the first setvar variable with a class variable. (Revised by BJ, 13-Sep-2022.) |
⊢ (𝐴 E 𝑥 ↔ 𝐴 ∈ 𝑥) | ||
Theorem | 0sn0ep 5434 | An example for the membership relation. (Contributed by AV, 19-Jun-2022.) |
⊢ ∅ E {∅} | ||
Theorem | epn0 5435 | The membership relation is nonempty. (Contributed by AV, 19-Jun-2022.) |
⊢ E ≠ ∅ | ||
We have not yet defined relations (df-rel 5526), but here we introduce a few related notions we will use to develop ordinals. The class variable 𝑅 is no different from other class variables, but it reminds us that normally it represents what we will later call a "relation". | ||
Syntax | wpo 5436 | Extend wff notation to include the strict partial ordering predicate. Read: "𝑅 is a partial order on 𝐴". |
wff 𝑅 Po 𝐴 | ||
Syntax | wor 5437 | Extend wff notation to include the strict total ordering predicate. Read: "𝑅 orders 𝐴". |
wff 𝑅 Or 𝐴 | ||
Definition | df-po 5438* | Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on 𝐴. For example, < Po ℝ is true, while ≤ Po ℝ is false (ex-po 28220). (Contributed by NM, 16-Mar-1997.) |
⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) | ||
Definition | df-so 5439* | Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 10710). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.) |
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
Theorem | poss 5440 | Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) |
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Po 𝐵 → 𝑅 Po 𝐴)) | ||
Theorem | poeq1 5441 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴)) | ||
Theorem | poeq2 5442 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵)) | ||
Theorem | nfpo 5443 | Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Po 𝐴 | ||
Theorem | nfso 5444 | Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Or 𝐴 | ||
Theorem | pocl 5445 | Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) | ||
Theorem | ispod 5446* | Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
Theorem | swopolem 5447* | Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌))) | ||
Theorem | swopo 5448* | A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
Theorem | poirr 5449 | A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | potr 5450 | A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | po2nr 5451 | A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
Theorem | po3nr 5452 | A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
Theorem | po2ne 5453 | Two classes which are in a partial order relation are not equal. (Contributed by AV, 13-Mar-2023.) |
⊢ ((𝑅 Po 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴𝑅𝐵) → 𝐴 ≠ 𝐵) | ||
Theorem | po0 5454 | Any relation is a partial ordering of the empty set. (Contributed by NM, 28-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ 𝑅 Po ∅ | ||
Theorem | pofun 5455* | A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.) |
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ 𝑋𝑅𝑌} & ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌) ⇒ ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴) | ||
Theorem | sopo 5456 | A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.) |
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) | ||
Theorem | soss 5457 | 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 5458 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) | ||
Theorem | soeq2 5459 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) | ||
Theorem | sonr 5460 | A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | sotr 5461 | A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | solin 5462 | A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) | ||
Theorem | so2nr 5463 | A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
Theorem | so3nr 5464 | A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
Theorem | sotric 5465 | A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) | ||
Theorem | sotrieq 5466 | Trichotomy law for strict order relation. (Contributed by NM, 9-Apr-1996.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) | ||
Theorem | sotrieq2 5467 | Trichotomy law for strict order relation. (Contributed by NM, 5-May-1999.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 ↔ (¬ 𝐵𝑅𝐶 ∧ ¬ 𝐶𝑅𝐵))) | ||
Theorem | soasym 5468 | Asymmetry law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋𝑅𝑌 → ¬ 𝑌𝑅𝑋)) | ||
Theorem | sotr2 5469 | A transitivity relation. (Read 𝐵 ≤ 𝐶 and 𝐶 < 𝐷 implies 𝐵 < 𝐷.) (Contributed by Mario Carneiro, 10-May-2013.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((¬ 𝐶𝑅𝐵 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | issod 5470* | 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 5471* | 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 5472* | Deduce strict ordering from its properties. (Contributed by NM, 29-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ 𝑅 Or 𝐴 | ||
Theorem | so0 5473 | 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 5474* | A totally ordered set has at most one minimal element. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by NM, 16-Jun-2017.) |
⊢ (𝑅 Or 𝐴 → ∃*𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ¬ 𝑦𝑅𝑥) | ||
Syntax | wfr 5475 | Extend wff notation to include the well-founded predicate. Read: "𝑅 is a well-founded relation on 𝐴". |
wff 𝑅 Fr 𝐴 | ||
Syntax | wse 5476 | Extend wff notation to include the set-like predicate. Read: "𝑅 is set-like on 𝐴". |
wff 𝑅 Se 𝐴 | ||
Syntax | wwe 5477 | Extend wff notation to include the well-ordering predicate. Read: "𝑅 well-orders 𝐴". |
wff 𝑅 We 𝐴 | ||
Definition | df-fr 5478* | Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5484 and dffr3 5929. A class is called well-founded when the membership relation E (see df-eprel 5430) 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 5479* | Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.) |
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) | ||
Definition | df-we 5480 | Define the well-ordering predicate. For an alternate definition, see dfwe2 7476. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | ||
Theorem | fri 5481* | Property of well-founded relation (one direction of definition). (Contributed by NM, 18-Mar-1997.) |
⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | seex 5482* | 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 5483 | Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴) | ||
Theorem | dffr2 5484* | 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.) |
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 {𝑧 ∈ 𝑥 ∣ 𝑧𝑅𝑦} = ∅)) | ||
Theorem | frc 5485* | 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 5486 | 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 5487 | Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝑅 ⊆ 𝑆 → (𝑆 Se 𝐴 → 𝑅 Se 𝐴)) | ||
Theorem | sess2 5488 | Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Se 𝐵 → 𝑅 Se 𝐴)) | ||
Theorem | freq1 5489 | Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) | ||
Theorem | freq2 5490 | Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵)) | ||
Theorem | seeq1 5491 | Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝑅 = 𝑆 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴)) | ||
Theorem | seeq2 5492 | Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝐴 = 𝐵 → (𝑅 Se 𝐴 ↔ 𝑅 Se 𝐵)) | ||
Theorem | nffr 5493 | 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 5494 | 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 5495 | 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 5496 | 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 5497 | 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 5498 | Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.) |
⊢ 𝑅 Fr ∅ | ||
Theorem | frminex 5499* | 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 5500 | A well-founded class does not belong to itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.) |
⊢ ( E Fr 𝐴 → ¬ 𝐴 ∈ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |