| Metamath
Proof Explorer Theorem List (p. 64 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dfdm2 6301 | Alternate definition of domain df-dm 5695 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.) |
| ⊢ dom 𝐴 = ∪ ∪ (◡𝐴 ∘ 𝐴) | ||
| Theorem | unixp 6302 | The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006.) |
| ⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) | ||
| Theorem | unixp0 6303 | A Cartesian product is empty iff its union is empty. (Contributed by NM, 20-Sep-2006.) |
| ⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (𝐴 × 𝐵) = ∅) | ||
| Theorem | unixpid 6304 | Field of a Cartesian square. (Contributed by FL, 10-Oct-2009.) |
| ⊢ ∪ ∪ (𝐴 × 𝐴) = 𝐴 | ||
| Theorem | ressn 6305 | Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ (𝐴 ↾ {𝐵}) = ({𝐵} × (𝐴 “ {𝐵})) | ||
| Theorem | cnviin 6306* | The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012.) |
| ⊢ (𝐴 ≠ ∅ → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) | ||
| Theorem | cnvpo 6307 | The converse of a partial order is a partial order. (Contributed by NM, 15-Jun-2005.) |
| ⊢ (𝑅 Po 𝐴 ↔ ◡𝑅 Po 𝐴) | ||
| Theorem | cnvso 6308 | The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005.) |
| ⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴) | ||
| Theorem | xpco 6309 | Composition of two Cartesian products. (Contributed by Thierry Arnoux, 17-Nov-2017.) |
| ⊢ (𝐵 ≠ ∅ → ((𝐵 × 𝐶) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐶)) | ||
| Theorem | xpcoid 6310 | Composition of two Cartesian squares. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
| ⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) = (𝐴 × 𝐴) | ||
| Theorem | elsnxp 6311* | Membership in a Cartesian product with a singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.) (Proof shortened by JJ, 14-Jul-2021.) |
| ⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉)) | ||
| Theorem | reu3op 6312* | There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 1-Jul-2023.) |
| ⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜓 ↔ 𝜒)) ⇒ ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ (∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 𝜒 ∧ ∃𝑥 ∈ 𝑋 ∃𝑦 ∈ 𝑌 ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑌 (𝜒 → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉))) | ||
| Theorem | reuop 6313* | There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 23-Jun-2023.) |
| ⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜓 ↔ 𝜒)) & ⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝜓 ↔ 𝜃)) ⇒ ⊢ (∃!𝑝 ∈ (𝑋 × 𝑌)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑌 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝜃 → 〈𝑥, 𝑦〉 = 〈𝑎, 𝑏〉))) | ||
| Theorem | opreu2reurex 6314* | There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 24-Jun-2023.) (Revised by AV, 1-Jul-2023.) |
| ⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∃!𝑝 ∈ (𝐴 × 𝐵)𝜑 ↔ (∃!𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝜒 ∧ ∃!𝑏 ∈ 𝐵 ∃𝑎 ∈ 𝐴 𝜒)) | ||
| Theorem | opreu2reu 6315* | If there is a unique ordered pair fulfilling a wff, then there is a double restricted unique existential qualification fulfilling a corresponding wff. (Contributed by AV, 25-Jun-2023.) (Revised by AV, 2-Jul-2023.) |
| ⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∃!𝑝 ∈ (𝐴 × 𝐵)𝜑 → ∃!𝑎 ∈ 𝐴 ∃!𝑏 ∈ 𝐵 𝜒) | ||
| Theorem | dfpo2 6316 | Quantifier-free definition of a partial ordering. (Contributed by Scott Fenton, 22-Feb-2013.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
| ⊢ (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) | ||
| Theorem | csbcog 6317 | Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.) |
| ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∘ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∘ ⦋𝐴 / 𝑥⦌𝐶)) | ||
| Theorem | snres0 6318 | Condition for restriction of a singleton to be empty. (Contributed by Scott Fenton, 9-Aug-2024.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (({〈𝐴, 𝐵〉} ↾ 𝐶) = ∅ ↔ ¬ 𝐴 ∈ 𝐶) | ||
| Theorem | imaindm 6319 | The image is unaffected by intersection with the domain. (Contributed by Scott Fenton, 17-Dec-2021.) |
| ⊢ (𝑅 “ 𝐴) = (𝑅 “ (𝐴 ∩ dom 𝑅)) | ||
| Syntax | cpred 6320 | The predecessors symbol. |
| class Pred(𝑅, 𝐴, 𝑋) | ||
| Definition | df-pred 6321 | Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6338). (Contributed by Scott Fenton, 29-Jan-2011.) |
| ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) | ||
| Theorem | predeq123 6322 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐵, 𝑌)) | ||
| Theorem | predeq1 6323 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
| ⊢ (𝑅 = 𝑆 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐴, 𝑋)) | ||
| Theorem | predeq2 6324 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
| ⊢ (𝐴 = 𝐵 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋)) | ||
| Theorem | predeq3 6325 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
| ⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) | ||
| Theorem | nfpred 6326 | Bound-variable hypothesis builder for the predecessor class. (Contributed by Scott Fenton, 9-Jun-2018.) |
| ⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑋 ⇒ ⊢ Ⅎ𝑥Pred(𝑅, 𝐴, 𝑋) | ||
| Theorem | csbpredg 6327 | Move class substitution in and out of the predecessor class of a relation. (Contributed by ML, 25-Oct-2020.) |
| ⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑋) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑋)) | ||
| Theorem | predpredss 6328 | If 𝐴 is a subset of 𝐵, then their predecessor classes are also subsets. (Contributed by Scott Fenton, 2-Feb-2011.) |
| ⊢ (𝐴 ⊆ 𝐵 → Pred(𝑅, 𝐴, 𝑋) ⊆ Pred(𝑅, 𝐵, 𝑋)) | ||
| Theorem | predss 6329 | The predecessor class of 𝐴 is a subset of 𝐴. (Contributed by Scott Fenton, 2-Feb-2011.) |
| ⊢ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴 | ||
| Theorem | sspred 6330 | Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011.) |
| ⊢ ((𝐵 ⊆ 𝐴 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋)) | ||
| Theorem | dfpred2 6331* | An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 8-Feb-2011.) |
| ⊢ 𝑋 ∈ V ⇒ ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ {𝑦 ∣ 𝑦𝑅𝑋}) | ||
| Theorem | dfpred3 6332* | An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ 𝑋 ∈ V ⇒ ⊢ Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋} | ||
| Theorem | dfpred3g 6333* | An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.) |
| ⊢ (𝑋 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}) | ||
| Theorem | elpredgg 6334 | Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) Generalize to closed form. (Revised by BJ, 16-Oct-2024.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌𝑅𝑋))) | ||
| Theorem | elpredg 6335 | Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) (Proof shortened by BJ, 16-Oct-2024.) |
| ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ 𝑌𝑅𝑋)) | ||
| Theorem | elpredimg 6336 | Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 13-Apr-2011.) (Revised by NM, 5-Apr-2016.) (Proof shortened by BJ, 16-Oct-2024.) |
| ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)) → 𝑌𝑅𝑋) | ||
| Theorem | elpredim 6337 | Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012.) (Proof shortened by BJ, 16-Oct-2024.) |
| ⊢ 𝑋 ∈ V ⇒ ⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌𝑅𝑋) | ||
| Theorem | elpred 6338 | Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011.) (Proof shortened by BJ, 16-Oct-2024.) |
| ⊢ 𝑌 ∈ V ⇒ ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌𝑅𝑋))) | ||
| Theorem | predexg 6339 | The predecessor class exists when 𝐴 does. (Contributed by Scott Fenton, 8-Feb-2011.) Generalize to closed form. (Revised by BJ, 27-Oct-2024.) |
| ⊢ (𝐴 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑋) ∈ V) | ||
| Theorem | predasetexOLD 6340 | Obsolete form of predexg 6339 as of 27-Oct-2024. (Contributed by Scott Fenton, 8-Feb-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ Pred(𝑅, 𝐴, 𝑋) ∈ V | ||
| Theorem | dffr4 6341* | Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011.) |
| ⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 Pred(𝑅, 𝑥, 𝑦) = ∅)) | ||
| Theorem | predel 6342 | Membership in the predecessor class implies membership in the base class. (Contributed by Scott Fenton, 11-Feb-2011.) |
| ⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌 ∈ 𝐴) | ||
| Theorem | predtrss 6343 | If 𝑅 is transitive over 𝐴 and 𝑌𝑅𝑋, then Pred(𝑅, 𝐴, 𝑌) is a subclass of Pred(𝑅, 𝐴, 𝑋). (Contributed by Scott Fenton, 28-Oct-2024.) |
| ⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)) | ||
| Theorem | predpo 6344 | Property of the predecessor class for partial orders. (Contributed by Scott Fenton, 28-Apr-2012.) (Proof shortened by Scott Fenton, 28-Oct-2024.) |
| ⊢ ((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋))) | ||
| Theorem | predso 6345 | Property of the predecessor class for strict total orders. (Contributed by Scott Fenton, 11-Feb-2011.) |
| ⊢ ((𝑅 Or 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋))) | ||
| Theorem | setlikespec 6346 | If 𝑅 is set-like in 𝐴, then all predecessor classes of elements of 𝐴 exist. (Contributed by Scott Fenton, 20-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V) | ||
| Theorem | predidm 6347 | Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011.) |
| ⊢ Pred(𝑅, Pred(𝑅, 𝐴, 𝑋), 𝑋) = Pred(𝑅, 𝐴, 𝑋) | ||
| Theorem | predin 6348 | Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.) |
| ⊢ Pred(𝑅, (𝐴 ∩ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∩ Pred(𝑅, 𝐵, 𝑋)) | ||
| Theorem | predun 6349 | Union law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.) |
| ⊢ Pred(𝑅, (𝐴 ∪ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∪ Pred(𝑅, 𝐵, 𝑋)) | ||
| Theorem | preddif 6350 | Difference law for predecessor classes. (Contributed by Scott Fenton, 14-Apr-2011.) |
| ⊢ Pred(𝑅, (𝐴 ∖ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∖ Pred(𝑅, 𝐵, 𝑋)) | ||
| Theorem | predep 6351 | The predecessor under the membership relation is equivalent to an intersection. (Contributed by Scott Fenton, 27-Mar-2011.) (Proof shortened by Andrew Salmon, 27-Aug-2011.) |
| ⊢ (𝑋 ∈ 𝐵 → Pred( E , 𝐴, 𝑋) = (𝐴 ∩ 𝑋)) | ||
| Theorem | trpred 6352 | The class of predecessors of an element of a transitive class for the membership relation is that element. (Contributed by BJ, 12-Oct-2024.) |
| ⊢ ((Tr 𝐴 ∧ 𝑋 ∈ 𝐴) → Pred( E , 𝐴, 𝑋) = 𝑋) | ||
| Theorem | preddowncl 6353* | A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011.) |
| ⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋))) | ||
| Theorem | predpoirr 6354 | Given a partial ordering, a class is not a member of its predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) |
| ⊢ (𝑅 Po 𝐴 → ¬ 𝑋 ∈ Pred(𝑅, 𝐴, 𝑋)) | ||
| Theorem | predfrirr 6355 | Given a well-founded relation, a class is not a member of its predecessor class. (Contributed by Scott Fenton, 22-Apr-2011.) |
| ⊢ (𝑅 Fr 𝐴 → ¬ 𝑋 ∈ Pred(𝑅, 𝐴, 𝑋)) | ||
| Theorem | pred0 6356 | The predecessor class over ∅ is always ∅. (Contributed by Scott Fenton, 16-Apr-2011.) (Proof shortened by AV, 11-Jun-2021.) |
| ⊢ Pred(𝑅, ∅, 𝑋) = ∅ | ||
| Theorem | dfse3 6357* | Alternate definition of set-like relationships. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑥) ∈ V) | ||
| Theorem | predrelss 6358 | Subset carries from relation to predecessor class. (Contributed by Scott Fenton, 25-Nov-2024.) |
| ⊢ (𝑅 ⊆ 𝑆 → Pred(𝑅, 𝐴, 𝑋) ⊆ Pred(𝑆, 𝐴, 𝑋)) | ||
| Theorem | predprc 6359 | The predecessor of a proper class is empty. (Contributed by Scott Fenton, 25-Nov-2024.) |
| ⊢ (¬ 𝑋 ∈ V → Pred(𝑅, 𝐴, 𝑋) = ∅) | ||
| Theorem | predres 6360 | Predecessor class is unaffected by restriction to the base class. (Contributed by Scott Fenton, 25-Nov-2024.) |
| ⊢ Pred(𝑅, 𝐴, 𝑋) = Pred((𝑅 ↾ 𝐴), 𝐴, 𝑋) | ||
| Theorem | frpomin 6361* | Every nonempty (possibly proper) subclass of a class 𝐴 with a well-founded set-like partial order 𝑅 has a minimal element. The additional condition of partial order over frmin 9789 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
| ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
| Theorem | frpomin2 6362* | Every nonempty (possibly proper) subclass of a class 𝐴 with a well-founded set-like partial order 𝑅 has a minimal element. The additional condition of partial order over frmin 9789 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
| ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑥) = ∅) | ||
| Theorem | frpoind 6363* | The principle of well-founded induction over a partial order. This theorem is a version of frind 9790 that does not require the axiom of infinity and can be used to prove wfi 6371 and tfi 7874. (Contributed by Scott Fenton, 11-Feb-2022.) |
| ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵) | ||
| Theorem | frpoinsg 6364* | Well-Founded Induction Schema (variant). If a property passes from all elements less than 𝑦 of a well-founded set-like partial order class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 11-Feb-2022.) |
| ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑦 ∈ 𝐴) → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
| Theorem | frpoins2fg 6365* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.) |
| ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
| Theorem | frpoins2g 6366* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.) |
| ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
| Theorem | frpoins3g 6367* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 19-Aug-2024.) |
| ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ Pred (𝑅, 𝐴, 𝑥)𝜓 → 𝜑)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝐵 ∈ 𝐴) → 𝜒) | ||
| Theorem | tz6.26 6368* | All nonempty subclasses of a class having a well-ordered set-like relation have minimal elements for that relation. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
| ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) | ||
| Theorem | tz6.26OLD 6369* | Obsolete version of tz6.26 6368 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) | ||
| Theorem | tz6.26i 6370* | All nonempty subclasses of a class having a well-ordered set-like relation 𝑅 have 𝑅-minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31. (Contributed by Scott Fenton, 14-Apr-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) | ||
| Theorem | wfi 6371* | The Principle of Well-Ordered Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if 𝐵 is a subclass of a well-ordered class 𝐴 with the property that every element of 𝐵 whose inital segment is included in 𝐴 is itself equal to 𝐴. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
| ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵) | ||
| Theorem | wfiOLD 6372* | Obsolete version of wfi 6371 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵) | ||
| Theorem | wfii 6373* | The Principle of Well-Ordered Induction. Theorem 6.27 of [TakeutiZaring] p. 32. This principle states that if 𝐵 is a subclass of a well-ordered class 𝐴 with the property that every element of 𝐵 whose inital segment is included in 𝐴 is itself equal to 𝐴. (Contributed by Scott Fenton, 29-Jan-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵)) → 𝐴 = 𝐵) | ||
| Theorem | wfisg 6374* | Well-Ordered Induction Schema. If a property passes from all elements less than 𝑦 of a well-ordered class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 11-Feb-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
| ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
| Theorem | wfisgOLD 6375* | Obsolete version of wfisg 6374 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 11-Feb-2011.) |
| ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
| Theorem | wfis 6376* | Well-Ordered Induction Schema. If all elements less than a given set 𝑥 of the well-ordered class 𝐴 have a property (induction hypothesis), then all elements of 𝐴 have that property. (Contributed by Scott Fenton, 29-Jan-2011.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
| Theorem | wfis2fg 6377* | Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
| ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
| Theorem | wfis2fgOLD 6378* | Obsolete version of wfis2fg 6377 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 11-Feb-2011.) |
| ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
| Theorem | wfis2f 6379* | Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
| Theorem | wfis2g 6380* | Well-Ordered Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) |
| ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
| Theorem | wfis2 6381* | Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
| Theorem | wfis3 6382* | Well-Ordered Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
| ⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝜒) | ||
| Syntax | word 6383 | Extend the definition of a wff to include the ordinal predicate. |
| wff Ord 𝐴 | ||
| Syntax | con0 6384 | 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 6385 | Extend the definition of a wff to include the limit ordinal predicate. |
| wff Lim 𝐴 | ||
| Syntax | csuc 6386 | Extend class notation to include the successor function. |
| class suc 𝐴 | ||
| Definition | df-ord 6387 |
Define the ordinal predicate, which is true for a class that is transitive
and is well-ordered by the membership relation. Variant of definition of
[BellMachover] p. 468.
Some sources will define a notation for ordinal order corresponding to < and ≤ but we just use ∈ and ⊆ respectively. (Contributed by NM, 17-Sep-1993.) |
| ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | ||
| Definition | df-on 6388 | Define the class of all ordinal numbers. Definition 7.11 of [TakeutiZaring] p. 38. (Contributed by NM, 5-Jun-1994.) |
| ⊢ On = {𝑥 ∣ Ord 𝑥} | ||
| Definition | df-lim 6389 | Define the limit ordinal predicate, which is true for a nonempty ordinal that 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. See dflim2 6441, dflim3 7868, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.) |
| ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | ||
| Definition | df-suc 6390 | Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8569). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. Definition 1.4 of [Schloeder] p. 1, similarly. Ordinal natural numbers defined using this successor function and 0 as the empty set are also called von Neumann ordinals; 0 is the empty set {}, 1 is {0, {0}}, 2 is {1, {1}}, and so on. 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 6460), so that the successor of any ordinal class is still an ordinal class (ordsuc 7833), simplifying certain proofs. 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 6391 | Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.) |
| ⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) | ||
| Theorem | elong 6392 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) | ||
| Theorem | elon 6393 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
| ⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ On ↔ Ord 𝐴) | ||
| Theorem | eloni 6394 | An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.) |
| ⊢ (𝐴 ∈ On → Ord 𝐴) | ||
| Theorem | elon2 6395 | An ordinal number is an ordinal set. Part of Definition 1.2 of [Schloeder] p. 1. (Contributed by NM, 8-Feb-2004.) |
| ⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V)) | ||
| Theorem | limeq 6396 | Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
| ⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵)) | ||
| Theorem | ordwe 6397 | Membership well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.) |
| ⊢ (Ord 𝐴 → E We 𝐴) | ||
| Theorem | ordtr 6398 | An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.) |
| ⊢ (Ord 𝐴 → Tr 𝐴) | ||
| Theorem | ordfr 6399 | Membership is well-founded on an ordinal class. In other words, an ordinal class is well-founded. (Contributed by NM, 22-Apr-1994.) |
| ⊢ (Ord 𝐴 → E Fr 𝐴) | ||
| Theorem | ordelss 6400 | An element of an ordinal class is a subset of it. (Contributed by NM, 30-May-1994.) |
| ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ⊆ 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |