HomeHome Intuitionistic Logic Explorer
Theorem List (p. 44 of 150)
< 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 - 4301-4400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorempoeq1 4301 Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
(𝑅 = 𝑆 → (𝑅 Po 𝐴𝑆 Po 𝐴))
 
Theorempoeq2 4302 Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.)
(𝐴 = 𝐵 → (𝑅 Po 𝐴𝑅 Po 𝐵))
 
Theoremnfpo 4303 Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
𝑥𝑅    &   𝑥𝐴       𝑥 𝑅 Po 𝐴
 
Theoremnfso 4304 Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.)
𝑥𝑅    &   𝑥𝐴       𝑥 𝑅 Or 𝐴
 
Theorempocl 4305 Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.)
(𝑅 Po 𝐴 → ((𝐵𝐴𝐶𝐴𝐷𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))))
 
Theoremispod 4306* Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.)
((𝜑𝑥𝐴) → ¬ 𝑥𝑅𝑥)    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧))       (𝜑𝑅 Po 𝐴)
 
Theoremswopolem 4307* Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.)
((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))       ((𝜑 ∧ (𝑋𝐴𝑌𝐴𝑍𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍𝑍𝑅𝑌)))
 
Theoremswopo 4308* A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.)
((𝜑 ∧ (𝑦𝐴𝑧𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦))    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧𝑧𝑅𝑦)))       (𝜑𝑅 Po 𝐴)
 
Theorempoirr 4309 A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
 
Theorempotr 4310 A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))
 
Theorempo2nr 4311 A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
 
Theorempo3nr 4312 A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.)
((𝑅 Po 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐷𝐷𝑅𝐵))
 
Theorempo0 4313 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 4314* A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.)
𝑆 = {⟨𝑥, 𝑦⟩ ∣ 𝑋𝑅𝑌}    &   (𝑥 = 𝑦𝑋 = 𝑌)       ((𝑅 Po 𝐵 ∧ ∀𝑥𝐴 𝑋𝐵) → 𝑆 Po 𝐴)
 
Theoremsopo 4315 A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.)
(𝑅 Or 𝐴𝑅 Po 𝐴)
 
Theoremsoss 4316 Subset theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(𝐴𝐵 → (𝑅 Or 𝐵𝑅 Or 𝐴))
 
Theoremsoeq1 4317 Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
(𝑅 = 𝑆 → (𝑅 Or 𝐴𝑆 Or 𝐴))
 
Theoremsoeq2 4318 Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.)
(𝐴 = 𝐵 → (𝑅 Or 𝐴𝑅 Or 𝐵))
 
Theoremsonr 4319 A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.)
((𝑅 Or 𝐴𝐵𝐴) → ¬ 𝐵𝑅𝐵)
 
Theoremsotr 4320 A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ((𝐵𝑅𝐶𝐶𝑅𝐷) → 𝐵𝑅𝐷))
 
Theoremissod 4321* An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4299). (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.)
(𝜑𝑅 Po 𝐴)    &   ((𝜑 ∧ (𝑥𝐴𝑦𝐴)) → (𝑥𝑅𝑦𝑥 = 𝑦𝑦𝑅𝑥))       (𝜑𝑅 Or 𝐴)
 
Theoremsowlin 4322 A strict order relation satisfies weak linearity. (Contributed by Jim Kingdon, 6-Oct-2018.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → (𝐵𝑅𝐶 → (𝐵𝑅𝐷𝐷𝑅𝐶)))
 
Theoremso2nr 4323 A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐵))
 
Theoremso3nr 4324 A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴𝐷𝐴)) → ¬ (𝐵𝑅𝐶𝐶𝑅𝐷𝐷𝑅𝐵))
 
Theoremsotricim 4325 One direction of sotritric 4326 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.)
((𝑅 Or 𝐴 ∧ (𝐵𝐴𝐶𝐴)) → (𝐵𝑅𝐶 → ¬ (𝐵 = 𝐶𝐶𝑅𝐵)))
 
Theoremsotritric 4326 A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 28-Sep-2019.)
𝑅 Or 𝐴    &   ((𝐵𝐴𝐶𝐴) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))       ((𝐵𝐴𝐶𝐴) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶𝐶𝑅𝐵)))
 
Theoremsotritrieq 4327 A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.)
𝑅 Or 𝐴    &   ((𝐵𝐴𝐶𝐴) → (𝐵𝑅𝐶𝐵 = 𝐶𝐶𝑅𝐵))       ((𝐵𝐴𝐶𝐴) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶𝐶𝑅𝐵)))
 
Theoremso0 4328 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.9  Founded and set-like relations
 
Syntaxwfrfor 4329 Extend wff notation to include the well-founded predicate.
wff FrFor 𝑅𝐴𝑆
 
Syntaxwfr 4330 Extend wff notation to include the well-founded predicate. Read: ' 𝑅 is a well-founded relation on 𝐴.'
wff 𝑅 Fr 𝐴
 
Syntaxwse 4331 Extend wff notation to include the set-like predicate. Read: ' 𝑅 is set-like on 𝐴.'
wff 𝑅 Se 𝐴
 
Syntaxwwe 4332 Extend wff notation to include the well-ordering predicate. Read: ' 𝑅 well-orders 𝐴.'
wff 𝑅 We 𝐴
 
Definitiondf-frfor 4333* 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 4334* 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 4335* Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.)
(𝑅 Se 𝐴 ↔ ∀𝑥𝐴 {𝑦𝐴𝑦𝑅𝑥} ∈ V)
 
Definitiondf-wetr 4336* 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 do not have that as seen at ordtriexmid 4522). Given excluded middle, well-ordering is usually defined to require trichotomy (and the definition of Fr is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.)
(𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴𝑧𝐴 ((𝑥𝑅𝑦𝑦𝑅𝑧) → 𝑥𝑅𝑧)))
 
Theoremseex 4337* 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 4338 Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.)
(𝐴𝑉𝑅 Se 𝐴)
 
Theoremsess1 4339 Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(𝑅𝑆 → (𝑆 Se 𝐴𝑅 Se 𝐴))
 
Theoremsess2 4340 Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(𝐴𝐵 → (𝑅 Se 𝐵𝑅 Se 𝐴))
 
Theoremseeq1 4341 Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(𝑅 = 𝑆 → (𝑅 Se 𝐴𝑆 Se 𝐴))
 
Theoremseeq2 4342 Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.)
(𝐴 = 𝐵 → (𝑅 Se 𝐴𝑅 Se 𝐵))
 
Theoremnfse 4343 Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑥𝑅    &   𝑥𝐴       𝑥 𝑅 Se 𝐴
 
Theoremepse 4344 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 𝐴
 
Theoremfrforeq1 4345 Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
(𝑅 = 𝑆 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑆𝐴𝑇))
 
Theoremfreq1 4346 Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.)
(𝑅 = 𝑆 → (𝑅 Fr 𝐴𝑆 Fr 𝐴))
 
Theoremfrforeq2 4347 Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
(𝐴 = 𝐵 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑅𝐵𝑇))
 
Theoremfreq2 4348 Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.)
(𝐴 = 𝐵 → (𝑅 Fr 𝐴𝑅 Fr 𝐵))
 
Theoremfrforeq3 4349 Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.)
(𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇))
 
Theoremnffrfor 4350 Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑥𝑅    &   𝑥𝐴    &   𝑥𝑆       𝑥 FrFor 𝑅𝐴𝑆
 
Theoremnffr 4351 Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑥𝑅    &   𝑥𝐴       𝑥 𝑅 Fr 𝐴
 
Theoremfrirrg 4352 A well-founded relation is irreflexive. This is the case where 𝐴 exists. (Contributed by Jim Kingdon, 21-Sep-2021.)
((𝑅 Fr 𝐴𝐴𝑉𝐵𝐴) → ¬ 𝐵𝑅𝐵)
 
Theoremfr0 4353 Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.)
𝑅 Fr ∅
 
Theoremfrind 4354* Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.)
(𝑥 = 𝑦 → (𝜑𝜓))    &   ((𝜒𝑥𝐴) → (∀𝑦𝐴 (𝑦𝑅𝑥𝜓) → 𝜑))    &   (𝜒𝑅 Fr 𝐴)    &   (𝜒𝐴𝑉)       ((𝜒𝑥𝐴) → 𝜑)
 
Theoremefrirr 4355 Irreflexivity of the epsilon relation: a class founded by epsilon is not a member of itself. (Contributed by NM, 18-Apr-1994.) (Revised by Mario Carneiro, 22-Jun-2015.)
( E Fr 𝐴 → ¬ 𝐴𝐴)
 
Theoremtz7.2 4356 Similar to Theorem 7.2 of [TakeutiZaring] p. 35, of except that the Axiom of Regularity is not required due to antecedent E Fr 𝐴. (Contributed by NM, 4-May-1994.)
((Tr 𝐴 ∧ E Fr 𝐴𝐵𝐴) → (𝐵𝐴𝐵𝐴))
 
Theoremnfwe 4357 Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.)
𝑥𝑅    &   𝑥𝐴       𝑥 𝑅 We 𝐴
 
Theoremweeq1 4358 Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.)
(𝑅 = 𝑆 → (𝑅 We 𝐴𝑆 We 𝐴))
 
Theoremweeq2 4359 Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.)
(𝐴 = 𝐵 → (𝑅 We 𝐴𝑅 We 𝐵))
 
Theoremwefr 4360 A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
(𝑅 We 𝐴𝑅 Fr 𝐴)
 
Theoremwepo 4361 A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.)
((𝑅 We 𝐴𝐴𝑉) → 𝑅 Po 𝐴)
 
Theoremwetrep 4362* An epsilon well-ordering is a transitive relation. (Contributed by NM, 22-Apr-1994.)
(( E We 𝐴 ∧ (𝑥𝐴𝑦𝐴𝑧𝐴)) → ((𝑥𝑦𝑦𝑧) → 𝑥𝑧))
 
Theoremwe0 4363 Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.)
𝑅 We ∅
 
2.3.10  Ordinals
 
Syntaxword 4364 Extend the definition of a wff to include the ordinal predicate.
wff Ord 𝐴
 
Syntaxcon0 4365 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 4366 Extend the definition of a wff to include the limit ordinal predicate.
wff Lim 𝐴
 
Syntaxcsuc 4367 Extend class notation to include the successor function.
class suc 𝐴
 
Definitiondf-iord 4368* 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".

Some sources will define a notation for ordinal order corresponding to < and but we just use and respectively.

(Contributed by Jim Kingdon, 10-Oct-2018.) Use its alias dford3 4369 instead for naming consistency with set.mm. (New usage is discouraged.)

(Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 Tr 𝑥))
 
Theoremdford3 4369* Alias for df-iord 4368. Use it instead of df-iord 4368 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
(Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴 Tr 𝑥))
 
Definitiondf-on 4370 Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.)
On = {𝑥 ∣ Ord 𝑥}
 
Definitiondf-ilim 4371 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 𝐴 ≠ ∅ to ∅ ∈ 𝐴 (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 4372 instead for naming consistency with set.mm. (New usage is discouraged.)
(Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴))
 
Theoremdflim2 4372 Alias for df-ilim 4371. Use it instead of df-ilim 4371 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.)
(Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴))
 
Definitiondf-suc 4373 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 4414). 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 𝐴 = (𝐴 ∪ {𝐴})
 
Theoremordeq 4374 Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.)
(𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵))
 
Theoremelong 4375 An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
(𝐴𝑉 → (𝐴 ∈ On ↔ Ord 𝐴))
 
Theoremelon 4376 An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.)
𝐴 ∈ V       (𝐴 ∈ On ↔ Ord 𝐴)
 
Theoremeloni 4377 An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.)
(𝐴 ∈ On → Ord 𝐴)
 
Theoremelon2 4378 An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.)
(𝐴 ∈ On ↔ (Ord 𝐴𝐴 ∈ V))
 
Theoremlimeq 4379 Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
(𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵))
 
Theoremordtr 4380 An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)
(Ord 𝐴 → Tr 𝐴)
 
Theoremordelss 4381 An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.)
((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
 
Theoremtrssord 4382 A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.)
((Tr 𝐴𝐴𝐵 ∧ Ord 𝐵) → Ord 𝐴)
 
Theoremordelord 4383 An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)
((Ord 𝐴𝐵𝐴) → Ord 𝐵)
 
Theoremtron 4384 The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.)
Tr On
 
Theoremordelon 4385 An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.)
((Ord 𝐴𝐵𝐴) → 𝐵 ∈ On)
 
Theoremonelon 4386 An element of an ordinal number is an ordinal number. Theorem 2.2(iii) of [BellMachover] p. 469. (Contributed by NM, 26-Oct-2003.)
((𝐴 ∈ On ∧ 𝐵𝐴) → 𝐵 ∈ On)
 
Theoremordin 4387 The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.)
((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴𝐵))
 
Theoremonin 4388 The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.)
((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴𝐵) ∈ On)
 
Theoremonelss 4389 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.)
(𝐴 ∈ On → (𝐵𝐴𝐵𝐴))
 
Theoremordtr1 4390 Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
(Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
 
Theoremontr1 4391 Transitive law for ordinal numbers. Theorem 7M(b) of [Enderton] p. 192. (Contributed by NM, 11-Aug-1994.)
(𝐶 ∈ On → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
 
Theoremonintss 4392* 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.)
(𝑥 = 𝐴 → (𝜑𝜓))       (𝐴 ∈ On → (𝜓 {𝑥 ∈ On ∣ 𝜑} ⊆ 𝐴))
 
Theoremord0 4393 The empty set is an ordinal class. (Contributed by NM, 11-May-1994.)
Ord ∅
 
Theorem0elon 4394 The empty set is an ordinal number. Corollary 7N(b) of [Enderton] p. 193. (Contributed by NM, 17-Sep-1993.)
∅ ∈ On
 
Theoreminton 4395 The intersection of the class of ordinal numbers is the empty set. (Contributed by NM, 20-Oct-2003.)
On = ∅
 
Theoremnlim0 4396 The empty set is not a limit ordinal. (Contributed by NM, 24-Mar-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
¬ Lim ∅
 
Theoremlimord 4397 A limit ordinal is ordinal. (Contributed by NM, 4-May-1995.)
(Lim 𝐴 → Ord 𝐴)
 
Theoremlimuni 4398 A limit ordinal is its own supremum (union). (Contributed by NM, 4-May-1995.)
(Lim 𝐴𝐴 = 𝐴)
 
Theoremlimuni2 4399 The union of a limit ordinal is a limit ordinal. (Contributed by NM, 19-Sep-2006.)
(Lim 𝐴 → Lim 𝐴)
 
Theorem0ellim 4400 A limit ordinal contains the empty set. (Contributed by NM, 15-May-1994.)
(Lim 𝐴 → ∅ ∈ 𝐴)
    < Previous  Next >

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-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-14917
  Copyright terms: Public domain < Previous  Next >