Home | Metamath
Proof Explorer Theorem List (p. 55 of 460) | < 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: | Metamath Proof Explorer
(1-28853) |
Hilbert Space Explorer
(28854-30376) |
Users' Mathboxes
(30377-45962) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ssopab2 5401 | Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.) |
⊢ (∀𝑥∀𝑦(𝜑 → 𝜓) → {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓}) | ||
Theorem | ssopab2bw 5402* | Equivalence of ordered pair abstraction subclass and implication. Version of ssopab2b 5404 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 27-Dec-1996.) (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) | ||
Theorem | eqopab2bw 5403* | Equivalence of ordered pair abstraction equality and biconditional. Version of eqopab2b 5407 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by Mario Carneiro, 4-Jan-2017.) (Revised by Gino Giotto, 26-Jan-2024.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓)) | ||
Theorem | ssopab2b 5404 | Equivalence of ordered pair abstraction subclass and implication. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker ssopab2bw 5402 when possible. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.) (New usage is discouraged.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 → 𝜓)) | ||
Theorem | ssopab2i 5405 | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜓} | ||
Theorem | ssopab2dv 5406* | Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
⊢ (𝜑 → (𝜓 → 𝜒)) ⇒ ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} ⊆ {〈𝑥, 𝑦〉 ∣ 𝜒}) | ||
Theorem | eqopab2b 5407 | Equivalence of ordered pair abstraction equality and biconditional. Usage of this theorem is discouraged because it depends on ax-13 2372. Use the weaker eqopab2bw 5403 when possible. (Contributed by Mario Carneiro, 4-Jan-2017.) (New usage is discouraged.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} ↔ ∀𝑥∀𝑦(𝜑 ↔ 𝜓)) | ||
Theorem | opabn0 5408 | Nonempty ordered pair class abstraction. (Contributed by NM, 10-Oct-2007.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥∃𝑦𝜑) | ||
Theorem | opab0 5409 | Empty ordered pair class abstraction. (Contributed by AV, 29-Oct-2021.) |
⊢ ({〈𝑥, 𝑦〉 ∣ 𝜑} = ∅ ↔ ∀𝑥∀𝑦 ¬ 𝜑) | ||
Theorem | csbopab 5410* | Move substitution into a class abstraction. Version of csbopabgALT 5411 without a sethood antecedent but depending on more axioms. (Contributed by NM, 6-Aug-2007.) (Revised by NM, 23-Aug-2018.) |
⊢ ⦋𝐴 / 𝑥⦌{〈𝑦, 𝑧〉 ∣ 𝜑} = {〈𝑦, 𝑧〉 ∣ [𝐴 / 𝑥]𝜑} | ||
Theorem | csbopabgALT 5411* | Move substitution into a class abstraction. Version of csbopab 5410 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 5412* | Move substitution into a maps-to notation. (Contributed by AV, 26-Sep-2019.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ ⦋𝐴 / 𝑥⦌𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍)) | ||
Theorem | csbmpt2 5413* | Move substitution into the second part of a maps-to notation. (Contributed by AV, 26-Sep-2019.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝑦 ∈ 𝑌 ↦ 𝑍) = (𝑦 ∈ 𝑌 ↦ ⦋𝐴 / 𝑥⦌𝑍)) | ||
Theorem | iunopab 5414* | Move indexed union inside an ordered-pair class abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.) |
⊢ ∪ 𝑧 ∈ 𝐴 {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ ∃𝑧 ∈ 𝐴 𝜑} | ||
Theorem | elopabr 5415* | Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ 𝑥𝑅𝑦} → 𝐴 ∈ 𝑅) | ||
Theorem | elopabran 5416* | Membership in an ordered-pair class abstraction defined by a restricted binary relation. (Contributed by AV, 16-Feb-2021.) |
⊢ (𝐴 ∈ {〈𝑥, 𝑦〉 ∣ (𝑥𝑅𝑦 ∧ 𝜓)} → 𝐴 ∈ 𝑅) | ||
Theorem | rbropapd 5417* | Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
⊢ (𝜑 → 𝑀 = {〈𝑓, 𝑝〉 ∣ (𝑓𝑊𝑝 ∧ 𝜓)}) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒)))) | ||
Theorem | rbropap 5418* | 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 5419* | 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 5420 | The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) Reduce axiom usage and shorten proof. (Revised by Gino Giotto, 3-Oct-2024.) |
⊢ ¬ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | 0nelopabOLD 5421 | Obsolete version of 0nelopab 5420 as of 3-Oct-2024. (Contributed by Alexander van der Vekens, 5-Nov-2017.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ¬ ∅ ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} | ||
Theorem | brabv 5422 | 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 5423 | 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 5424 | Obsolete version of pwunss 4508 as of 30-Dec-2023. (Contributed by NM, 23-Nov-2003.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴 ∪ 𝐵) | ||
Theorem | pwssun 5425 | 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 5426 | Obsolete proof of pwundif 4514 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 5427 | 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 5428 | Extend the definition of a class to include the identity relation. |
class I | ||
Definition | df-id 5429* | Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 I 5 and ¬ 4 I 5 (ex-id 28371). (Contributed by NM, 13-Aug-1995.) |
⊢ I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} | ||
Theorem | dfid4 5430 | The identity function expressed using maps-to notation. (Contributed by Scott Fenton, 15-Dec-2017.) |
⊢ I = (𝑥 ∈ V ↦ 𝑥) | ||
Theorem | dfid3 5431 | A stronger version of df-id 5429 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 Definition df-id 5429 when sufficient, since the derivation of dfid3 5431 is nontrivial and uses auxiliary axioms ax-10 2145 to ax-13 2372. (New usage is discouraged.) |
⊢ I = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} | ||
Theorem | dfid2 5432 | Alternate definition of the identity relation. (Contributed by NM, 15-Mar-2007.) Use df-id 5429 when sufficient (see comment at dfid3 5431). (New usage is discouraged.) |
⊢ I = {〈𝑥, 𝑥〉 ∣ 𝑥 = 𝑥} | ||
Syntax | cep 5433 | Extend class notation to include the membership relation. |
class E | ||
Definition | df-eprel 5434* | 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 5435). Thus, ⊢ 5 E {1, 5} (ex-eprel 28370). (Contributed by NM, 13-Aug-1995.) |
⊢ E = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ 𝑦} | ||
Theorem | epelg 5435 | The membership relation and the membership predicate agree when the "containing" class is a set. General version of epel 5437 and closed form of epeli 5436. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) (Proof shortened by BJ, 14-Jul-2023.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | epeli 5436 | The membership relation and the membership predicate agree when the "containing" class is a set. Inference associated with epelg 5435. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | epel 5437 | 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 5438 | An example for the membership relation. (Contributed by AV, 19-Jun-2022.) |
⊢ ∅ E {∅} | ||
Theorem | epn0 5439 | The membership relation is nonempty. (Contributed by AV, 19-Jun-2022.) |
⊢ E ≠ ∅ | ||
We have not yet defined relations (df-rel 5532), 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 typically it represents what we will later call a "relation". | ||
Syntax | wpo 5440 | Extend wff notation to include the strict partial ordering predicate. Read: "𝑅 is a partial order on 𝐴". |
wff 𝑅 Po 𝐴 | ||
Syntax | wor 5441 | Extend wff notation to include the strict total ordering predicate. Read: "𝑅 orders 𝐴". |
wff 𝑅 Or 𝐴 | ||
Definition | df-po 5442* | 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 28372). (Contributed by NM, 16-Mar-1997.) |
⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) | ||
Definition | df-so 5443* | Define the strict complete (linear) order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. For example, < Or ℝ is true (ltso 10799). Equivalent to Definition 6.19(1) of [TakeutiZaring] p. 29. (Contributed by NM, 21-Jan-1996.) |
⊢ (𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) | ||
Theorem | poss 5444 | 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 5445 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴)) | ||
Theorem | poeq2 5446 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵)) | ||
Theorem | nfpo 5447 | Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Po 𝐴 | ||
Theorem | nfso 5448 | Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Or 𝐴 | ||
Theorem | pocl 5449 | Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.) Reduce axiom usage and shorten proof. (Revised by Gino Giotto, 3-Oct-2024.) |
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) | ||
Theorem | poclOLD 5450 | Obsolete version of pocl 5449 as of 3-Oct-2024. (Contributed by NM, 27-Mar-1997.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) | ||
Theorem | ispod 5451* | Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
Theorem | swopolem 5452* | Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌))) | ||
Theorem | swopo 5453* | A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
Theorem | poirr 5454 | A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | potr 5455 | A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | po2nr 5456 | A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
Theorem | po3nr 5457 | A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
Theorem | po2ne 5458 | Two classes which are in a partial order relation are not equal. (Contributed by AV, 13-Mar-2023.) |
⊢ ((𝑅 Po 𝑉 ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) ∧ 𝐴𝑅𝐵) → 𝐴 ≠ 𝐵) | ||
Theorem | po0 5459 | 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 5460* | A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.) |
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ 𝑋𝑅𝑌} & ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌) ⇒ ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴) | ||
Theorem | sopo 5461 | A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.) |
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) | ||
Theorem | soss 5462 | 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 5463 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) | ||
Theorem | soeq2 5464 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) | ||
Theorem | sonr 5465 | A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | sotr 5466 | A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | solin 5467 | A strict order relation is linear (satisfies trichotomy). (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) | ||
Theorem | so2nr 5468 | A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
Theorem | so3nr 5469 | A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
Theorem | sotric 5470 | A strict order relation satisfies strict trichotomy. (Contributed by NM, 19-Feb-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) | ||
Theorem | sotrieq 5471 | Trichotomy law for strict order relation. (Contributed by NM, 9-Apr-1996.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) | ||
Theorem | sotrieq2 5472 | Trichotomy law for strict order relation. (Contributed by NM, 5-May-1999.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 = 𝐶 ↔ (¬ 𝐵𝑅𝐶 ∧ ¬ 𝐶𝑅𝐵))) | ||
Theorem | soasym 5473 | Asymmetry law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴)) → (𝑋𝑅𝑌 → ¬ 𝑌𝑅𝑋)) | ||
Theorem | sotr2 5474 | A transitivity relation. (Read 𝐵 ≤ 𝐶 and 𝐶 < 𝐷 implies 𝐵 < 𝐷.) (Contributed by Mario Carneiro, 10-May-2013.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((¬ 𝐶𝑅𝐵 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | issod 5475* | 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 5476* | 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 5477* | Deduce strict ordering from its properties. (Contributed by NM, 29-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → (𝑥𝑅𝑦 ↔ ¬ (𝑥 = 𝑦 ∨ 𝑦𝑅𝑥))) & ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ 𝑅 Or 𝐴 | ||
Theorem | so0 5478 | 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 5479* | 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 5480 | Extend wff notation to include the well-founded predicate. Read: "𝑅 is a well-founded relation on 𝐴". |
wff 𝑅 Fr 𝐴 | ||
Syntax | wse 5481 | Extend wff notation to include the set-like predicate. Read: "𝑅 is set-like on 𝐴". |
wff 𝑅 Se 𝐴 | ||
Syntax | wwe 5482 | Extend wff notation to include the well-ordering predicate. Read: "𝑅 well-orders 𝐴". |
wff 𝑅 We 𝐴 | ||
Definition | df-fr 5483* | Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 5489 and dffr3 5936. A class is called well-founded when the membership relation E (see df-eprel 5434) 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 5484* | Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.) |
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) | ||
Definition | df-we 5485 | Define the well-ordering predicate. For an alternate definition, see dfwe2 7515. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)) | ||
Theorem | fri 5486* | Property of well-founded relation (one direction of definition). (Contributed by NM, 18-Mar-1997.) |
⊢ (((𝐵 ∈ 𝐶 ∧ 𝑅 Fr 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | seex 5487* | 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 5488 | Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴) | ||
Theorem | dffr2 5489* | 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 2145, ax-11 2162, ax-12 2179, but use ax-8 2116. (Revised by Gino Giotto, 3-Oct-2024.) |
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 {𝑧 ∈ 𝑥 ∣ 𝑧𝑅𝑦} = ∅)) | ||
Theorem | dffr2ALT 5490* | Alternate proof of dffr2 5489, which avoids ax-8 2116 but requires ax-10 2145, ax-11 2162, ax-12 2179. (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 5491* | 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 5492 | 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 5493 | Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝑅 ⊆ 𝑆 → (𝑆 Se 𝐴 → 𝑅 Se 𝐴)) | ||
Theorem | sess2 5494 | Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Se 𝐵 → 𝑅 Se 𝐴)) | ||
Theorem | freq1 5495 | Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) | ||
Theorem | freq2 5496 | Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵)) | ||
Theorem | seeq1 5497 | Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝑅 = 𝑆 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴)) | ||
Theorem | seeq2 5498 | Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝐴 = 𝐵 → (𝑅 Se 𝐴 ↔ 𝑅 Se 𝐵)) | ||
Theorem | nffr 5499 | 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 5500 | Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Se 𝐴 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |