![]() |
Intuitionistic Logic Explorer Theorem List (p. 44 of 152) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-eprel 4301* | 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 4302. Thus, 5 E { 1 , 5 }. (Contributed by NM, 13-Aug-1995.) |
⊢ E = {〈𝑥, 𝑦〉 ∣ 𝑥 ∈ 𝑦} | ||
Theorem | epelg 4302 | The epsilon relation and membership are the same. General version of epel 4304. (Contributed by Scott Fenton, 27-Mar-2011.) (Revised by Mario Carneiro, 28-Apr-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵)) | ||
Theorem | epelc 4303 | The epsilon relationship and the membership relation are the same. (Contributed by Scott Fenton, 11-Apr-2012.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 E 𝐵 ↔ 𝐴 ∈ 𝐵) | ||
Theorem | epel 4304 | The epsilon relation and the membership relation are the same. (Contributed by NM, 13-Aug-1995.) |
⊢ (𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦) | ||
Definition | df-id 4305* | 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 = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} | ||
We have not yet defined relations (df-rel 4645), 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 4306 | Extend wff notation to include the strict partial ordering predicate. Read: ' 𝑅 is a partial order on 𝐴.' |
wff 𝑅 Po 𝐴 | ||
Syntax | wor 4307 | Extend wff notation to include the strict linear ordering predicate. Read: ' 𝑅 orders 𝐴.' |
wff 𝑅 Or 𝐴 | ||
Definition | df-po 4308* | 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 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) | ||
Definition | df-iso 4309* | 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 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦)))) | ||
Theorem | poss 4310 | 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 4311 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Po 𝐴 ↔ 𝑆 Po 𝐴)) | ||
Theorem | poeq2 4312 | Equality theorem for partial ordering predicate. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝐴 = 𝐵 → (𝑅 Po 𝐴 ↔ 𝑅 Po 𝐵)) | ||
Theorem | nfpo 4313 | Bound-variable hypothesis builder for partial orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Po 𝐴 | ||
Theorem | nfso 4314 | Bound-variable hypothesis builder for total orders. (Contributed by Stefan O'Rear, 20-Jan-2015.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Or 𝐴 | ||
Theorem | pocl 4315 | Properties of partial order relation in class notation. (Contributed by NM, 27-Mar-1997.) |
⊢ (𝑅 Po 𝐴 → ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴) → (¬ 𝐵𝑅𝐵 ∧ ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)))) | ||
Theorem | ispod 4316* | Sufficient conditions for a partial order. (Contributed by NM, 9-Jul-2014.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝑥𝑅𝑥) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
Theorem | swopolem 4317* | Perform the substitutions into the strict weak ordering law. (Contributed by Mario Carneiro, 31-Dec-2014.) |
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → (𝑋𝑅𝑌 → (𝑋𝑅𝑍 ∨ 𝑍𝑅𝑌))) | ||
Theorem | swopo 4318* | A strict weak order is a partial order. (Contributed by Mario Carneiro, 9-Jul-2014.) |
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑦𝑅𝑧 → ¬ 𝑧𝑅𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (𝑥𝑅𝑦 → (𝑥𝑅𝑧 ∨ 𝑧𝑅𝑦))) ⇒ ⊢ (𝜑 → 𝑅 Po 𝐴) | ||
Theorem | poirr 4319 | A partial order relation is irreflexive. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | potr 4320 | A partial order relation is a transitive relation. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | po2nr 4321 | A partial order relation has no 2-cycle loops. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
Theorem | po3nr 4322 | A partial order relation has no 3-cycle loops. (Contributed by NM, 27-Mar-1997.) |
⊢ ((𝑅 Po 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
Theorem | po0 4323 | 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 4324* | A function preserves a partial order relation. (Contributed by Jeff Madsen, 18-Jun-2011.) |
⊢ 𝑆 = {〈𝑥, 𝑦〉 ∣ 𝑋𝑅𝑌} & ⊢ (𝑥 = 𝑦 → 𝑋 = 𝑌) ⇒ ⊢ ((𝑅 Po 𝐵 ∧ ∀𝑥 ∈ 𝐴 𝑋 ∈ 𝐵) → 𝑆 Po 𝐴) | ||
Theorem | sopo 4325 | A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997.) |
⊢ (𝑅 Or 𝐴 → 𝑅 Po 𝐴) | ||
Theorem | soss 4326 | 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 4327 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Or 𝐴 ↔ 𝑆 Or 𝐴)) | ||
Theorem | soeq2 4328 | Equality theorem for the strict ordering predicate. (Contributed by NM, 16-Mar-1997.) |
⊢ (𝐴 = 𝐵 → (𝑅 Or 𝐴 ↔ 𝑅 Or 𝐵)) | ||
Theorem | sonr 4329 | A strict order relation is irreflexive. (Contributed by NM, 24-Nov-1995.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | sotr 4330 | A strict order relation is a transitive relation. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷) → 𝐵𝑅𝐷)) | ||
Theorem | issod 4331* | An irreflexive, transitive, trichotomous relation is a linear ordering (in the sense of df-iso 4309). (Contributed by NM, 21-Jan-1996.) (Revised by Mario Carneiro, 9-Jul-2014.) |
⊢ (𝜑 → 𝑅 Po 𝐴) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑥𝑅𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦𝑅𝑥)) ⇒ ⊢ (𝜑 → 𝑅 Or 𝐴) | ||
Theorem | sowlin 4332 | A strict order relation satisfies weak linearity. (Contributed by Jim Kingdon, 6-Oct-2018.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐵𝑅𝐶 → (𝐵𝑅𝐷 ∨ 𝐷𝑅𝐶))) | ||
Theorem | so2nr 4333 | A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐵)) | ||
Theorem | so3nr 4334 | A strict order relation has no 3-cycle loops. (Contributed by NM, 21-Jan-1996.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ¬ (𝐵𝑅𝐶 ∧ 𝐶𝑅𝐷 ∧ 𝐷𝑅𝐵)) | ||
Theorem | sotricim 4335 | One direction of sotritric 4336 holds for all weakly linear orders. (Contributed by Jim Kingdon, 28-Sep-2019.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵𝑅𝐶 → ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) | ||
Theorem | sotritric 4336 | A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 28-Sep-2019.) |
⊢ 𝑅 Or 𝐴 & ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ↔ ¬ (𝐵 = 𝐶 ∨ 𝐶𝑅𝐵))) | ||
Theorem | sotritrieq 4337 | A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.) |
⊢ 𝑅 Or 𝐴 & ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵𝑅𝐶 ∨ 𝐵 = 𝐶 ∨ 𝐶𝑅𝐵)) ⇒ ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐵 = 𝐶 ↔ ¬ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) | ||
Theorem | so0 4338 | 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 ∅ | ||
Syntax | wfrfor 4339 | Extend wff notation to include the well-founded predicate. |
wff FrFor 𝑅𝐴𝑆 | ||
Syntax | wfr 4340 | Extend wff notation to include the well-founded predicate. Read: ' 𝑅 is a well-founded relation on 𝐴.' |
wff 𝑅 Fr 𝐴 | ||
Syntax | wse 4341 | Extend wff notation to include the set-like predicate. Read: ' 𝑅 is set-like on 𝐴.' |
wff 𝑅 Se 𝐴 | ||
Syntax | wwe 4342 | Extend wff notation to include the well-ordering predicate. Read: ' 𝑅 well-orders 𝐴.' |
wff 𝑅 We 𝐴 | ||
Definition | df-frfor 4343* | 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 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆)) | ||
Definition | df-frind 4344* | 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 𝑅𝐴𝑠) | ||
Definition | df-se 4345* | Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014.) |
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑥} ∈ V) | ||
Definition | df-wetr 4346* | 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 4532). 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 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) | ||
Theorem | seex 4347* | 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 4348 | Any relation on a set is set-like on it. (Contributed by Mario Carneiro, 22-Jun-2015.) |
⊢ (𝐴 ∈ 𝑉 → 𝑅 Se 𝐴) | ||
Theorem | sess1 4349 | Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝑅 ⊆ 𝑆 → (𝑆 Se 𝐴 → 𝑅 Se 𝐴)) | ||
Theorem | sess2 4350 | Subset theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝐴 ⊆ 𝐵 → (𝑅 Se 𝐵 → 𝑅 Se 𝐴)) | ||
Theorem | seeq1 4351 | Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝑅 = 𝑆 → (𝑅 Se 𝐴 ↔ 𝑆 Se 𝐴)) | ||
Theorem | seeq2 4352 | Equality theorem for the set-like predicate. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ (𝐴 = 𝐵 → (𝑅 Se 𝐴 ↔ 𝑅 Se 𝐵)) | ||
Theorem | nfse 4353 | Bound-variable hypothesis builder for set-like relations. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 Se 𝐴 | ||
Theorem | epse 4354 | 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 𝐴 | ||
Theorem | frforeq1 4355 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
⊢ (𝑅 = 𝑆 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑆𝐴𝑇)) | ||
Theorem | freq1 4356 | Equality theorem for the well-founded predicate. (Contributed by NM, 9-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 Fr 𝐴 ↔ 𝑆 Fr 𝐴)) | ||
Theorem | frforeq2 4357 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
⊢ (𝐴 = 𝐵 → ( FrFor 𝑅𝐴𝑇 ↔ FrFor 𝑅𝐵𝑇)) | ||
Theorem | freq2 4358 | Equality theorem for the well-founded predicate. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝐴 = 𝐵 → (𝑅 Fr 𝐴 ↔ 𝑅 Fr 𝐵)) | ||
Theorem | frforeq3 4359 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
⊢ (𝑆 = 𝑇 → ( FrFor 𝑅𝐴𝑆 ↔ FrFor 𝑅𝐴𝑇)) | ||
Theorem | nffrfor 4360 | Bound-variable hypothesis builder for well-founded relations. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑆 ⇒ ⊢ Ⅎ𝑥 FrFor 𝑅𝐴𝑆 | ||
Theorem | nffr 4361 | 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 | frirrg 4362 | A well-founded relation is irreflexive. This is the case where 𝐴 exists. (Contributed by Jim Kingdon, 21-Sep-2021.) |
⊢ ((𝑅 Fr 𝐴 ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴) → ¬ 𝐵𝑅𝐵) | ||
Theorem | fr0 4363 | Any relation is well-founded on the empty set. (Contributed by NM, 17-Sep-1993.) |
⊢ 𝑅 Fr ∅ | ||
Theorem | frind 4364* | Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝜓) → 𝜑)) & ⊢ (𝜒 → 𝑅 Fr 𝐴) & ⊢ (𝜒 → 𝐴 ∈ 𝑉) ⇒ ⊢ ((𝜒 ∧ 𝑥 ∈ 𝐴) → 𝜑) | ||
Theorem | efrirr 4365 | 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 𝐴 → ¬ 𝐴 ∈ 𝐴) | ||
Theorem | tz7.2 4366 | 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 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ 𝐴)) | ||
Theorem | nfwe 4367 | Bound-variable hypothesis builder for well-orderings. (Contributed by Stefan O'Rear, 20-Jan-2015.) (Revised by Mario Carneiro, 14-Oct-2016.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 ⇒ ⊢ Ⅎ𝑥 𝑅 We 𝐴 | ||
Theorem | weeq1 4368 | Equality theorem for the well-ordering predicate. (Contributed by NM, 9-Mar-1997.) |
⊢ (𝑅 = 𝑆 → (𝑅 We 𝐴 ↔ 𝑆 We 𝐴)) | ||
Theorem | weeq2 4369 | Equality theorem for the well-ordering predicate. (Contributed by NM, 3-Apr-1994.) |
⊢ (𝐴 = 𝐵 → (𝑅 We 𝐴 ↔ 𝑅 We 𝐵)) | ||
Theorem | wefr 4370 | A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.) |
⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴) | ||
Theorem | wepo 4371 | A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.) |
⊢ ((𝑅 We 𝐴 ∧ 𝐴 ∈ 𝑉) → 𝑅 Po 𝐴) | ||
Theorem | wetrep 4372* | An epsilon well-ordering is a transitive relation. (Contributed by NM, 22-Apr-1994.) |
⊢ (( E We 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → ((𝑥 ∈ 𝑦 ∧ 𝑦 ∈ 𝑧) → 𝑥 ∈ 𝑧)) | ||
Theorem | we0 4373 | Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997.) |
⊢ 𝑅 We ∅ | ||
Syntax | word 4374 | Extend the definition of a wff to include the ordinal predicate. |
wff Ord 𝐴 | ||
Syntax | con0 4375 | 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 | ||
Syntax | wlim 4376 | Extend the definition of a wff to include the limit ordinal predicate. |
wff Lim 𝐴 | ||
Syntax | csuc 4377 | Extend class notation to include the successor function. |
class suc 𝐴 | ||
Definition | df-iord 4378* |
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 4379 instead for naming consistency with set.mm. (New usage is discouraged.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) | ||
Theorem | dford3 4379* | Alias for df-iord 4378. Use it instead of df-iord 4378 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 Tr 𝑥)) | ||
Definition | df-on 4380 | Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.) |
⊢ On = {𝑥 ∣ Ord 𝑥} | ||
Definition | df-ilim 4381 | 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 4382 instead for naming consistency with set.mm. (New usage is discouraged.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) | ||
Theorem | dflim2 4382 | Alias for df-ilim 4381. Use it instead of df-ilim 4381 for naming consistency with set.mm. (Contributed by NM, 4-Nov-2004.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) | ||
Definition | df-suc 4383 | 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 4424). 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 𝐴 = (𝐴 ∪ {𝐴}) | ||
Theorem | ordeq 4384 | Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.) |
⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) | ||
Theorem | elong 4385 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) | ||
Theorem | elon 4386 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ On ↔ Ord 𝐴) | ||
Theorem | eloni 4387 | An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ On → Ord 𝐴) | ||
Theorem | elon2 4388 | An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.) |
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V)) | ||
Theorem | limeq 4389 | Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵)) | ||
Theorem | ordtr 4390 | An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.) |
⊢ (Ord 𝐴 → Tr 𝐴) | ||
Theorem | ordelss 4391 | An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) | ||
Theorem | trssord 4392 | A transitive subclass of an ordinal class is ordinal. (Contributed by NM, 29-May-1994.) |
⊢ ((Tr 𝐴 ∧ 𝐴 ⊆ 𝐵 ∧ Ord 𝐵) → Ord 𝐴) | ||
Theorem | ordelord 4393 | An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵) | ||
Theorem | tron 4394 | The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009.) |
⊢ Tr On | ||
Theorem | ordelon 4395 | An element of an ordinal class is an ordinal number. (Contributed by NM, 26-Oct-2003.) |
⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ On) | ||
Theorem | onelon 4396 | 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) | ||
Theorem | ordin 4397 | The intersection of two ordinal classes is ordinal. Proposition 7.9 of [TakeutiZaring] p. 37. (Contributed by NM, 9-May-1994.) |
⊢ ((Ord 𝐴 ∧ Ord 𝐵) → Ord (𝐴 ∩ 𝐵)) | ||
Theorem | onin 4398 | The intersection of two ordinal numbers is an ordinal number. (Contributed by NM, 7-Apr-1995.) |
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ∩ 𝐵) ∈ On) | ||
Theorem | onelss 4399 | 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 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴)) | ||
Theorem | ordtr1 4400 | Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
⊢ (Ord 𝐶 → ((𝐴 ∈ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ 𝐶)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |