 Home Intuitionistic Logic ExplorerTheorem List (p. 41 of 74) < 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

2.3.7  Partial and complete ordering

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

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

Definitiondf-po 4003* Define the strict partial order predicate. Definition of [Enderton] p. 168. The expression 𝑅 Po A means 𝑅 is a partial order on A. (Contributed by NM, 16-Mar-1997.)
(𝑅 Po Ax A y A z Ax𝑅x ((x𝑅y y𝑅z) → x𝑅z)))

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

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

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

Theorempoeq2 4007 Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
(A = B → (𝑅 Po A𝑅 Po B))

Theoremnfpo 4008 Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
x𝑅    &   xA       x 𝑅 Po A

Theoremnfso 4009 Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
x𝑅    &   xA       x 𝑅 Or A

Theorempocl 4010 Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.)
(𝑅 Po A → ((B A 𝐶 A 𝐷 A) → (¬ B𝑅B ((B𝑅𝐶 𝐶𝑅𝐷) → B𝑅𝐷))))

Theoremispod 4011* Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.)
((φ x A) → ¬ x𝑅x)    &   ((φ (x A y A z A)) → ((x𝑅y y𝑅z) → x𝑅z))       (φ𝑅 Po A)

Theoremswopolem 4012* Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.)
((φ (x A y A z A)) → (x𝑅y → (x𝑅z z𝑅y)))       ((φ (𝑋 A 𝑌 A 𝑍 A)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 𝑍𝑅𝑌)))

Theoremswopo 4013* A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.)
((φ (y A z A)) → (y𝑅z → ¬ z𝑅y))    &   ((φ (x A y A z A)) → (x𝑅y → (x𝑅z z𝑅y)))       (φ𝑅 Po A)

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

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

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

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

Theorempo0 4018 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 4019* A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
𝑆 = {⟨x, y⟩ ∣ 𝑋𝑅𝑌}    &   (x = y𝑋 = 𝑌)       ((𝑅 Po B x A 𝑋 B) → 𝑆 Po A)

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

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

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

Theoremsoeq2 4023 Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
(A = B → (𝑅 Or A𝑅 Or B))

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

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

Theoremissod 4026* An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4004). (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
(φ𝑅 Po A)    &   ((φ (x A y A)) → (x𝑅y x = y y𝑅x))       (φ𝑅 Or A)

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

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

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

Theoremsotricim 4030 One direction of sotritric 4031 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.)
((𝑅 Or A (B A 𝐶 A)) → (B𝑅𝐶 → ¬ (B = 𝐶 𝐶𝑅B)))

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

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

Theoremso0 4033 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  Set-like relations

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

Definitiondf-se 4035* Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
(𝑅 Se Ax A {y Ay𝑅x} V)

Theoremseex 4036* 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 A B A) → {x Ax𝑅B} V)

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

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

Theoremsess2 4039 Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(AB → (𝑅 Se B𝑅 Se A))

Theoremseeq1 4040 Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(𝑅 = 𝑆 → (𝑅 Se A𝑆 Se A))

Theoremseeq2 4041 Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(A = B → (𝑅 Se A𝑅 Se B))

Theoremnfse 4042 Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
x𝑅    &   xA       x 𝑅 Se A

Theoremepse 4043 The epsilon relation is set-like on any class. (This is the origin of the term "set-like": a set-like relation "acts like" the epsilon relation of sets and their elements.) (Contributed by Mario Carneiro, 22-Jun-2015.)
E Se A

2.3.9  Ordinals

Syntaxword 4044 Extend the definition of a wff to include the ordinal predicate.
wff Ord A

Syntaxcon0 4045 Extend the definition of a class to include the class of all ordinal numbers. (The 0 in the name prevents creating a file called con.html, which causes problems in Windows.)
class On

Syntaxwlim 4046 Extend the definition of a wff to include the limit ordinal predicate.
wff Lim A

Syntaxcsuc 4047 Extend class notation to include the successor function.
class suc A

Definitiondf-iord 4048* Define the ordinal predicate, which is true for a class that is transitive and whose elements are transitive. Definition of ordinal in [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic". (Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4049 instead for naming consistency with set.mm. (New usage is discouraged.)
(Ord A ↔ (Tr A x A Tr x))

Theoremdford3 4049* Alias for df-iord 4048. Use it instead of df-iord 4048 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
(Ord A ↔ (Tr A x A Tr x))

Definitiondf-on 4050 Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.)
On = {x ∣ Ord x}

Definitiondf-ilim 4051 Define the limit ordinal predicate, which is true for an ordinal that has the empty set as an element and is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42, and then changes A ≠ ∅ to A (which would be equivalent given the law of the excluded middle, but which is not for us). (Contributed by Jim Kingdon, 11-Nov-2018.) Use its alias dflim2 4052 instead for naming consistency with set.mm. (New usage is discouraged.)
(Lim A ↔ (Ord A A A = A))

Theoremdflim2 4052 Alias for df-ilim 4051. Use it instead of df-ilim 4051 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.)
(Lim A ↔ (Ord A A A = A))

Definitiondf-suc 4053 Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1". Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Our definition is a generalization to classes. Although it is not conventional to use it with proper classes, it has no effect on a proper class (sucprc 4094). Some authors denote the successor operation with a prime (apostrophe-like) symbol, such as Definition 6 of [Suppes] p. 134 and the definition of successor in [Mendelson] p. 246 (who uses the symbol "Suc" as a predicate to mean "is a successor ordinal"). The definition of successor of [Enderton] p. 68 denotes the operation with a plus-sign superscript. (Contributed by NM, 30-Aug-1993.)
suc A = (A ∪ {A})

Theoremordeq 4054 Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
(A = B → (Ord A ↔ Ord B))

Theoremelong 4055 An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
(A 𝑉 → (A On ↔ Ord A))

Theoremelon 4056 An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
A V       (A On ↔ Ord A)

Theoremeloni 4057 An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
(A On → Ord A)

Theoremelon2 4058 An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
(A On ↔ (Ord A A V))

Theoremlimeq 4059 Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(A = B → (Lim A ↔ Lim B))

Theoremordtr 4060 An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
(Ord A → Tr A)

Theoremordelss 4061 An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
((Ord A B A) → BA)

Theoremtrssord 4062 A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.)
((Tr A AB Ord B) → Ord A)

Theoremordelord 4063 An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)
((Ord A B A) → Ord B)

Theoremtron 4064 The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
Tr On

Theoremordelon 4065 An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.)
((Ord A B A) → B On)

Theoremonelon 4066 An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
((A On B A) → B On)

Theoremordin 4067 The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.)
((Ord A Ord B) → Ord (AB))

Theoremonin 4068 The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.)
((A On B On) → (AB) On)

Theoremonelss 4069 An element of an ordinal number is a subset of the number. (Contributed by NM, 5-Jun-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(A On → (B ABA))

Theoremordtr1 4070 Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
(Ord 𝐶 → ((A B B 𝐶) → A 𝐶))

Theoremontr1 4071 Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.)
(𝐶 On → ((A B B 𝐶) → A 𝐶))

Theoremonintss 4072* If a property is true for an ordinal number, then the minimum ordinal number for which it is true is smaller or equal. Theorem Schema 61 of [Suppes] p. 228. (Contributed by NM, 3-Oct-2003.)
(x = A → (φψ))       (A On → (ψ {x On ∣ φ} ⊆ A))

Theoremord0 4073 The empty set is an ordinal class. (Contributed by NM, 11-May-1994.)
Ord ∅

Theorem0elon 4074 The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)
On

Theoreminton 4075 The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.)
On = ∅

Theoremnlim0 4076 The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
¬ Lim ∅

Theoremlimord 4077 A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
(Lim A → Ord A)

Theoremlimuni 4078 A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)
(Lim AA = A)

Theoremlimuni2 4079 The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.)
(Lim A → Lim A)

Theorem0ellim 4080 A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.)
(Lim A → ∅ A)

Theoremlimelon 4081 A limit ordinal class that is also a set is an ordinal number. (Contributed by NM, 26-Apr-2004.)
((A B Lim A) → A On)

Theoremonn0 4082 The class of all ordinal numbers is not empty. (Contributed by NM, 17-Sep-1995.)
On ≠ ∅

Theoremonm 4083 The class of all ordinal numbers is inhabited. (Contributed by Jim Kingdon, 6-Mar-2019.)
x x On

Theoremsuceq 4084 Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(A = B → suc A = suc B)

Theoremelsuci 4085 Membership in a successor. This one-way implication does not require that either A or B be sets. (Contributed by NM, 6-Jun-1994.)
(A suc B → (A B A = B))

Theoremelsucg 4086 Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-1995.)
(A 𝑉 → (A suc B ↔ (A B A = B)))

Theoremelsuc2g 4087 Variant of membership in a successor, requiring that B rather than A be a set. (Contributed by NM, 28-Oct-2003.)
(B 𝑉 → (A suc B ↔ (A B A = B)))

Theoremelsuc 4088 Membership in a successor. Exercise 5 of [TakeutiZaring] p. 17. (Contributed by NM, 15-Sep-2003.)
A V       (A suc B ↔ (A B A = B))

Theoremelsuc2 4089 Membership in a successor. (Contributed by NM, 15-Sep-2003.)
A V       (B suc A ↔ (B A B = A))

Theoremnfsuc 4090 Bound-variable hypothesis builder for successor. (Contributed by NM, 15-Sep-2003.)
xA       x suc A

Theoremelelsuc 4091 Membership in a successor. (Contributed by NM, 20-Jun-1998.)
(A BA suc B)

Theoremsucel 4092* Membership of a successor in another class. (Contributed by NM, 29-Jun-2004.)
(suc A Bx B y(y x ↔ (y A y = A)))

Theoremsuc0 4093 The successor of the empty set. (Contributed by NM, 1-Feb-2005.)
suc ∅ = {∅}

Theoremsucprc 4094 A proper class is its own successor. (Contributed by NM, 3-Apr-1995.)
A V → suc A = A)

Theoremunisuc 4095 A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by NM, 30-Aug-1993.)
A V       (Tr A suc A = A)

Theoremunisucg 4096 A transitive class is equal to the union of its successor. Combines Theorem 4E of [Enderton] p. 72 and Exercise 6 of [Enderton] p. 73. (Contributed by Jim Kingdon, 18-Aug-2019.)
(A 𝑉 → (Tr A suc A = A))

Theoremsssucid 4097 A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.)
A ⊆ suc A

Theoremsucidg 4098 Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized). (Contributed by NM, 25-Mar-1995.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
(A 𝑉A suc A)

Theoremsucid 4099 A set belongs to its successor. (Contributed by NM, 22-Jun-1994.) (Proof shortened by Alan Sare, 18-Feb-2012.) (Proof shortened by Scott Fenton, 20-Feb-2012.)
A V       A suc A

Theoremnsuceq0g 4100 No successor is empty. (Contributed by Jim Kingdon, 14-Oct-2018.)
(A 𝑉 → suc A ≠ ∅)

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-7354
 Copyright terms: Public domain < Previous  Next >