Home Intuitionistic Logic ExplorerTheorem List (p. 41 of 110) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 4001-4100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremopthg 4001 Ordered pair theorem. 𝐶 and 𝐷 are not required to be sets under our specific ordered pair definition. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷)))

Theoremopthg2 4002 Ordered pair theorem. (Contributed by NM, 14-Oct-2005.) (Revised by Mario Carneiro, 26-Apr-2015.)
((𝐶𝑉𝐷𝑊) → (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷)))

Theoremopth2 4003 Ordered pair theorem. (Contributed by NM, 21-Sep-2014.)
𝐶 ∈ V    &   𝐷 ∈ V       (⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷))

Theoremotth2 4004 Ordered triple theorem, with triple express with ordered pairs. (Contributed by NM, 1-May-1995.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝑅 ∈ V       (⟨⟨𝐴, 𝐵⟩, 𝑅⟩ = ⟨⟨𝐶, 𝐷⟩, 𝑆⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷𝑅 = 𝑆))

Theoremotth 4005 Ordered triple theorem. (Contributed by NM, 25-Sep-2014.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝑅 ∈ V       (⟨𝐴, 𝐵, 𝑅⟩ = ⟨𝐶, 𝐷, 𝑆⟩ ↔ (𝐴 = 𝐶𝐵 = 𝐷𝑅 = 𝑆))

Theoremeqvinop 4006* A variable introduction law for ordered pairs. Analog of Lemma 15 of [Monk2] p. 109. (Contributed by NM, 28-May-1995.)
𝐵 ∈ V    &   𝐶 ∈ V       (𝐴 = ⟨𝐵, 𝐶⟩ ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ ⟨𝑥, 𝑦⟩ = ⟨𝐵, 𝐶⟩))

Theoremcopsexg 4007* Substitution of class 𝐴 for ordered pair 𝑥, 𝑦. (Contributed by NM, 27-Dec-1996.) (Revised by Andrew Salmon, 11-Jul-2011.)
(𝐴 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))

Theoremcopsex2t 4008* Closed theorem form of copsex2g 4009. (Contributed by NM, 17-Feb-2013.)
((∀𝑥𝑦((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓)) ∧ (𝐴𝑉𝐵𝑊)) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))

Theoremcopsex2g 4009* Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995.)
((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))       ((𝐴𝑉𝐵𝑊) → (∃𝑥𝑦(⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜓))

Theoremcopsex4g 4010* An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995.)
(((𝑥 = 𝐴𝑦 = 𝐵) ∧ (𝑧 = 𝐶𝑤 = 𝐷)) → (𝜑𝜓))       (((𝐴𝑅𝐵𝑆) ∧ (𝐶𝑅𝐷𝑆)) → (∃𝑥𝑦𝑧𝑤((⟨𝐴, 𝐵⟩ = ⟨𝑥, 𝑦⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑧, 𝑤⟩) ∧ 𝜑) ↔ 𝜓))

Theorem0nelop 4011 A property of ordered pairs. (Contributed by Mario Carneiro, 26-Apr-2015.)
¬ ∅ ∈ ⟨𝐴, 𝐵

Theoremopeqex 4012 Equivalence of existence implied by equality of ordered pairs. (Contributed by NM, 28-May-2008.)
(⟨𝐴, 𝐵⟩ = ⟨𝐶, 𝐷⟩ → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐷 ∈ V)))

Theoremopcom 4013 An ordered pair commutes iff its members are equal. (Contributed by NM, 28-May-2009.)
𝐴 ∈ V    &   𝐵 ∈ V       (⟨𝐴, 𝐵⟩ = ⟨𝐵, 𝐴⟩ ↔ 𝐴 = 𝐵)

Theoremmoop2 4014* "At most one" property of an ordered pair. (Contributed by NM, 11-Apr-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝐵 ∈ V       ∃*𝑥 𝐴 = ⟨𝐵, 𝑥

Theoremopeqsn 4015 Equivalence for an ordered pair equal to a singleton. (Contributed by NM, 3-Jun-2008.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V       (⟨𝐴, 𝐵⟩ = {𝐶} ↔ (𝐴 = 𝐵𝐶 = {𝐴}))

Theoremopeqpr 4016 Equivalence for an ordered pair equal to an unordered pair. (Contributed by NM, 3-Jun-2008.)
𝐴 ∈ V    &   𝐵 ∈ V    &   𝐶 ∈ V    &   𝐷 ∈ V       (⟨𝐴, 𝐵⟩ = {𝐶, 𝐷} ↔ ((𝐶 = {𝐴} ∧ 𝐷 = {𝐴, 𝐵}) ∨ (𝐶 = {𝐴, 𝐵} ∧ 𝐷 = {𝐴})))

Theoremeuotd 4017* Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015.)
(𝜑𝐴 ∈ V)    &   (𝜑𝐵 ∈ V)    &   (𝜑𝐶 ∈ V)    &   (𝜑 → (𝜓 ↔ (𝑎 = 𝐴𝑏 = 𝐵𝑐 = 𝐶)))       (𝜑 → ∃!𝑥𝑎𝑏𝑐(𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝜓))

Theoremuniop 4018 The union of an ordered pair. Theorem 65 of [Suppes] p. 39. (Contributed by NM, 17-Aug-2004.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V       𝐴, 𝐵⟩ = {𝐴, 𝐵}

Theoremuniopel 4019 Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008.) (Revised by Mario Carneiro, 26-Apr-2015.)
𝐴 ∈ V    &   𝐵 ∈ V       (⟨𝐴, 𝐵⟩ ∈ 𝐶𝐴, 𝐵⟩ ∈ 𝐶)

2.3.4  Ordered-pair class abstractions (cont.)

Theoremopabid 4020 The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)

Theoremelopab 4021* Membership in a class abstraction of pairs. (Contributed by NM, 24-Mar-1998.)
(𝐴 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦(𝐴 = ⟨𝑥, 𝑦⟩ ∧ 𝜑))

TheoremopelopabsbALT 4022* The law of concretion in terms of substitutions. Less general than opelopabsb 4023, but having a much shorter proof. (Contributed by NM, 30-Sep-2002.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
(⟨𝑧, 𝑤⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝑤 / 𝑦][𝑧 / 𝑥]𝜑)

Theoremopelopabsb 4023* The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.)
(⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)

Theorembrabsb 4024* The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008.)
𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}       (𝐴𝑅𝐵[𝐴 / 𝑥][𝐵 / 𝑦]𝜑)

Theoremopelopabt 4025* Closed theorem form of opelopab 4034. (Contributed by NM, 19-Feb-2013.)
((∀𝑥𝑦(𝑥 = 𝐴 → (𝜑𝜓)) ∧ ∀𝑥𝑦(𝑦 = 𝐵 → (𝜓𝜒)) ∧ (𝐴𝑉𝐵𝑊)) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒))

Theoremopelopabga 4026* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))       ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓))

Theorembrabga 4027* The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.)
((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))    &   𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}       ((𝐴𝑉𝐵𝑊) → (𝐴𝑅𝐵𝜓))

Theoremopelopab2a 4028* Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013.)
((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))       ((𝐴𝐶𝐵𝐷) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝜑)} ↔ 𝜓))

Theoremopelopaba 4029* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by Mario Carneiro, 19-Dec-2013.)
𝐴 ∈ V    &   𝐵 ∈ V    &   ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))       (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓)

Theorembraba 4030* The law of concretion for a binary relation. (Contributed by NM, 19-Dec-2013.)
𝐴 ∈ V    &   𝐵 ∈ V    &   ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))    &   𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}       (𝐴𝑅𝐵𝜓)

Theoremopelopabg 4031* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 28-May-1995.) (Revised by Mario Carneiro, 19-Dec-2013.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑦 = 𝐵 → (𝜓𝜒))       ((𝐴𝑉𝐵𝑊) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒))

Theorembrabg 4032* The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑦 = 𝐵 → (𝜓𝜒))    &   𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}       ((𝐴𝐶𝐵𝐷) → (𝐴𝑅𝐵𝜒))

Theoremopelopab2 4033* Ordered pair membership in an ordered pair class abstraction. (Contributed by NM, 14-Oct-2007.) (Revised by Mario Carneiro, 19-Dec-2013.)
(𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑦 = 𝐵 → (𝜓𝜒))       ((𝐴𝐶𝐵𝐷) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ ((𝑥𝐶𝑦𝐷) ∧ 𝜑)} ↔ 𝜒))

Theoremopelopab 4034* The law of concretion. Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 16-May-1995.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑦 = 𝐵 → (𝜓𝜒))       (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒)

Theorembrab 4035* The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.)
𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑦 = 𝐵 → (𝜓𝜒))    &   𝑅 = {⟨𝑥, 𝑦⟩ ∣ 𝜑}       (𝐴𝑅𝐵𝜒)

Theoremopelopabaf 4036* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4034 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Mario Carneiro, 19-Dec-2013.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
𝑥𝜓    &   𝑦𝜓    &   𝐴 ∈ V    &   𝐵 ∈ V    &   ((𝑥 = 𝐴𝑦 = 𝐵) → (𝜑𝜓))       (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜓)

Theoremopelopabf 4037* The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopab 4034 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by NM, 19-Dec-2008.)
𝑥𝜓    &   𝑦𝜒    &   𝐴 ∈ V    &   𝐵 ∈ V    &   (𝑥 = 𝐴 → (𝜑𝜓))    &   (𝑦 = 𝐵 → (𝜓𝜒))       (⟨𝐴, 𝐵⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜒)

Theoremssopab2 4038 Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Revised by Mario Carneiro, 19-May-2013.)
(∀𝑥𝑦(𝜑𝜓) → {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓})

Theoremssopab2b 4039 Equivalence of ordered pair abstraction subclass and implication. (Contributed by NM, 27-Dec-1996.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
({⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ∀𝑥𝑦(𝜑𝜓))

Theoremssopab2i 4040 Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 5-Apr-1995.)
(𝜑𝜓)       {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜓}

Theoremssopab2dv 4041* Inference of ordered pair abstraction subclass from implication. (Contributed by NM, 19-Jan-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)
(𝜑 → (𝜓𝜒))       (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜓} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝜒})

Theoremeqopab2b 4042 Equivalence of ordered pair abstraction equality and biconditional. (Contributed by Mario Carneiro, 4-Jan-2017.)
({⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ 𝜓} ↔ ∀𝑥𝑦(𝜑𝜓))

Theoremopabm 4043* Inhabited ordered pair class abstraction. (Contributed by Jim Kingdon, 29-Sep-2018.)
(∃𝑧 𝑧 ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ ∃𝑥𝑦𝜑)

Theoremiunopab 4044* Move indexed union inside an ordered-pair abstraction. (Contributed by Stefan O'Rear, 20-Feb-2015.)
𝑧𝐴 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧𝐴 𝜑}

2.3.5  Power class of union and intersection

Theorempwin 4045 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.)
𝒫 (𝐴𝐵) = (𝒫 𝐴 ∩ 𝒫 𝐵)

Theorempwunss 4046 The power class of the union of two classes includes the union of their power classes. Exercise 4.12(k) of [Mendelson] p. 235. (Contributed by NM, 23-Nov-2003.)
(𝒫 𝐴 ∪ 𝒫 𝐵) ⊆ 𝒫 (𝐴𝐵)

Theorempwssunim 4047 The power class of the union of two classes is a subset of the union of their power classes, if one class is a subclass of the other. One direction of Exercise 4.12(l) of [Mendelson] p. 235. (Contributed by Jim Kingdon, 30-Sep-2018.)
((𝐴𝐵𝐵𝐴) → 𝒫 (𝐴𝐵) ⊆ (𝒫 𝐴 ∪ 𝒫 𝐵))

Theorempwundifss 4048 Break up the power class of a union into a union of smaller classes. (Contributed by Jim Kingdon, 30-Sep-2018.)
((𝒫 (𝐴𝐵) ∖ 𝒫 𝐴) ∪ 𝒫 𝐴) ⊆ 𝒫 (𝐴𝐵)

Theorempwunim 4049 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 Jim Kingdon, 30-Sep-2018.)
((𝐴𝐵𝐵𝐴) → 𝒫 (𝐴𝐵) = (𝒫 𝐴 ∪ 𝒫 𝐵))

2.3.6  Epsilon and identity relations

Syntaxcep 4050 Extend class notation to include the epsilon relation.
class E

Syntaxcid 4051 Extend the definition of a class to include identity relation.
class I

Definitiondf-eprel 4052* Define the epsilon relation. Similar to Definition 6.22 of [TakeutiZaring] p. 30. The epsilon relation and set membership are the same, that is, (𝐴 E 𝐵𝐴𝐵) when 𝐵 is a set by epelg 4053. Thus, 5 E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.)
E = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝑦}

Theoremepelg 4053 The epsilon relation and membership are the same. General version of epel 4055. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.)
(𝐵𝑉 → (𝐴 E 𝐵𝐴𝐵))

Theoremepelc 4054 The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.)
𝐵 ∈ V       (𝐴 E 𝐵𝐴𝐵)

Theoremepel 4055 The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.)
(𝑥 E 𝑦𝑥𝑦)

Definitiondf-id 4056* Define the identity relation. Definition 9.15 of [Quine] p. 64. For example, 5 I 5 and ¬ 4 I 5. (Contributed by NM, 13-Aug-1995.)
I = {⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦}

2.3.7  Partial and complete ordering

Syntaxwpo 4057 Extend wff notation to include the strict partial ordering predicate. Read: ' 𝑅 is a partial order on 𝐴.'
wff 𝑅 Po 𝐴

Syntaxwor 4058 Extend wff notation to include the strict linear ordering predicate. Read: ' 𝑅 orders 𝐴.'
wff 𝑅 Or 𝐴

Definitiondf-po 4059* Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po 𝐴 means 𝑅 is a partial order on 𝐴. (Contributed by NM, 16-Mar-1997.)
(𝑅 Po 𝐴 ↔ ∀𝑥𝐴𝑦𝐴𝑧𝐴𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))

Definitiondf-iso 4060* Define the strict linear order predicate. The expression 𝑅 Or 𝐴 is true if relationship 𝑅 orders 𝐴. The property 𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦) is called weak linearity by Proposition 11.2.3 of [HoTT], p. (varies). If we assumed excluded middle, it would be equivalent to trichotomy, 𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥. (Contributed by NM, 21-Jan-1996.) (Revised by Jim Kingdon, 4-Oct-2018.)
(𝑅 Or 𝐴 ↔ (𝑅 Po 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦))))

Theoremposs 4061 Subset theorem for the partial ordering predicate. (Contributed by NM, 27-Mar-1997.) (Proof shortened by Mario Carneiro, 18-Nov-2016.)
(𝐴𝐵 → (𝑅 Po 𝐵𝑅 Po 𝐴))

Theorempoeq1 4062 Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
(𝑅 = 𝑆 → (𝑅 Po 𝐴𝑆 Po 𝐴))

Theorempoeq2 4063 Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
(𝐴 = 𝐵 → (𝑅 Po 𝐴𝑅 Po 𝐵))

Theoremnfpo 4064 Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
𝑥𝑅    &   𝑥𝐴       𝑥 𝑅 Po 𝐴

Theoremnfso 4065 Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
𝑥𝑅    &   𝑥𝐴       𝑥 𝑅 Or 𝐴

Theorempocl 4066 Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.)
(𝑅 Po 𝐴 → ((𝐵𝐴𝐶𝐴𝐷𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))))

Theoremispod 4067* Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.)
((𝜑𝑥𝐴) → ¬ 𝑥𝑅𝑥)    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))       (𝜑𝑅 Po 𝐴)

Theoremswopolem 4068* Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.)
((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))       ((𝜑 ∧ (𝑋𝐴𝑌𝐴𝑍𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍𝑍𝑅𝑌)))

Theoremswopo 4069* A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.)
((𝜑 ∧ (𝑦𝐴𝑧𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦))    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))       (𝜑𝑅 Po 𝐴)

Theorempoirr 4070 A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)

Theorempotr 4071 A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))

Theorempo2nr 4072 A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))

Theorempo3nr 4073 A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐷𝐷𝑅𝐵))

Theorempo0 4074 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 ∅

Theorempofun 4075* A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}    &   (𝑥 = 𝑦𝑋 = 𝑌)       ((𝑅 Po 𝐵 ∧ ∀𝑥𝐴 𝑋𝐵) → 𝑆 Po 𝐴)

Theoremsopo 4076 A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
(𝑅 Or 𝐴𝑅 Po 𝐴)

Theoremsoss 4077 Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))

Theoremsoeq1 4078 Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
(𝑅 = 𝑆 → (𝑅 Or 𝐴𝑆 Or 𝐴))

Theoremsoeq2 4079 Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
(𝐴 = 𝐵 → (𝑅 Or 𝐴𝑅 Or 𝐵))

Theoremsonr 4080 A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
((𝑅 Or 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)

Theoremsotr 4081 A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))

Theoremissod 4082* An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4060). (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
(𝜑𝑅 Po 𝐴)    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))       (𝜑𝑅 Or 𝐴)

Theoremsowlin 4083 A strict order relation satisfies weak linearity. (Contributed by Jim Kingdon, 6-Oct-2018.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → (𝐵𝑅𝐶 → (𝐵𝑅𝐷𝐷𝑅𝐶)))

Theoremso2nr 4084 A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))

Theoremso3nr 4085 A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐷𝐷𝑅𝐵))

Theoremsotricim 4086 One direction of sotritric 4087 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 → ¬ (𝐵 = 𝐶𝐶𝑅𝐵)))

Theoremsotritric 4087 A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 28-Sep-2019.)
𝑅 Or 𝐴    &   ((𝐵𝐴𝐶𝐴) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))       ((𝐵𝐴𝐶𝐴) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶𝐶𝑅𝐵)))

Theoremsotritrieq 4088 A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
𝑅 Or 𝐴    &   ((𝐵𝐴𝐶𝐴) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))       ((𝐵𝐴𝐶𝐴) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶𝐶𝑅𝐵)))

Theoremso0 4089 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 ∅

2.3.8  Founded and set-like relations

Syntaxwfrfor 4090 Extend wff notation to include the well-founded predicate.
wff FrFor 𝑅𝐴𝑆

Syntaxwfr 4091 Extend wff notation to include the well-founded predicate. Read: ' 𝑅 is a well-founded relation on 𝐴.'
wff 𝑅 Fr 𝐴

Syntaxwse 4092 Extend wff notation to include the set-like predicate. Read: ' 𝑅 is set-like on 𝐴.'
wff 𝑅 Se 𝐴

Syntaxwwe 4093 Extend wff notation to include the well-ordering predicate. Read: ' 𝑅 well-orders 𝐴.'
wff 𝑅 We 𝐴

Definitiondf-frfor 4094* Define the well-founded relation predicate where 𝐴 might be a proper class. By passing in 𝑆 we allow it potentially to be a proper class rather than a set. (Contributed by Jim Kingdon and Mario Carneiro, 22-Sep-2021.)
( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥𝐴 (∀𝑦𝐴 (𝑦𝑅𝑥𝑦𝑆) → 𝑥𝑆) → 𝐴𝑆))

Definitiondf-frind 4095* Define the well-founded relation predicate. In the presence of excluded middle, there are a variety of equivalent ways to define this. In our case, this definition, in terms of an inductive principle, works better than one along the lines of "there is an element which is minimal when A is ordered by R". Because 𝑠 is constrained to be a set (not a proper class) here, sometimes it may be necessary to use FrFor directly rather than via Fr. (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.)
(𝑅 Fr 𝐴 ↔ ∀𝑠 FrFor 𝑅𝐴𝑠)

Definitiondf-se 4096* Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
(𝑅 Se 𝐴 ↔ ∀𝑥𝐴 {𝑦𝐴𝑦𝑅𝑥} ∈ V)

Definitiondf-wetr 4097* Define the well-ordering predicate. It is unusual to define "well-ordering" in the absence of excluded middle, but we mean an ordering which is like the ordering which we have for ordinals (for example, it does not entail trichotomy because ordinals don't have that as seen at ordtriexmid 4273). Given excluded middle, well-ordering is usually defined to require trichotomy (and the defintion of Fr is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.)
(𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))

Theoremseex 4098* 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)

Theoremexse 4099 Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.)
(𝐴𝑉𝑅 Se 𝐴)

Theoremsess1 4100 Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(𝑅𝑆 → (𝑆 Se 𝐴𝑅 Se 𝐴))

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-10953
 Copyright terms: Public domain < Previous  Next >