Home | Metamath
Proof Explorer Theorem List (p. 62 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmco 6101 | The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.) |
⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴) | ||
Theorem | coeq0 6102 | A composition of two relations is empty iff there is no overlap between the range of the second and the domain of the first. Useful in combination with coundi 6094 and coundir 6095 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅) | ||
Theorem | coiun 6103* | Composition with an indexed union. (Contributed by NM, 21-Dec-2008.) |
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) | ||
Theorem | cocnvcnv1 6104 | A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.) |
⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵) | ||
Theorem | cocnvcnv2 6105 | A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.) |
⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵) | ||
Theorem | cores2 6106 | Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.) |
⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵)) | ||
Theorem | co02 6107 | Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ∘ ∅) = ∅ | ||
Theorem | co01 6108 | Composition with the empty set. (Contributed by NM, 24-Apr-2004.) |
⊢ (∅ ∘ 𝐴) = ∅ | ||
Theorem | coi1 6109 | Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.) |
⊢ (Rel 𝐴 → (𝐴 ∘ I ) = 𝐴) | ||
Theorem | coi2 6110 | Composition with the identity relation. Part of Theorem 3.7(i) of [Monk1] p. 36. (Contributed by NM, 22-Apr-2004.) |
⊢ (Rel 𝐴 → ( I ∘ 𝐴) = 𝐴) | ||
Theorem | coires1 6111 | Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.) |
⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵) | ||
Theorem | coass 6112 | Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. (Contributed by NM, 27-Jan-1997.) |
⊢ ((𝐴 ∘ 𝐵) ∘ 𝐶) = (𝐴 ∘ (𝐵 ∘ 𝐶)) | ||
Theorem | relcnvtrg 6113 | General form of relcnvtr 6114. (Contributed by Peter Mazsa, 17-Oct-2023.) |
⊢ ((Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇) → ((𝑅 ∘ 𝑆) ⊆ 𝑇 ↔ (◡𝑆 ∘ ◡𝑅) ⊆ ◡𝑇)) | ||
Theorem | relcnvtr 6114 | A relation is transitive iff its converse is transitive. (Contributed by FL, 19-Sep-2011.) (Proof shortened by Peter Mazsa, 17-Oct-2023.) |
⊢ (Rel 𝑅 → ((𝑅 ∘ 𝑅) ⊆ 𝑅 ↔ (◡𝑅 ∘ ◡𝑅) ⊆ ◡𝑅)) | ||
Theorem | relssdmrn 6115 | A relation is included in the Cartesian product of its domain and range. Exercise 4.12(t) of [Mendelson] p. 235. (Contributed by NM, 3-Aug-1994.) |
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴)) | ||
Theorem | cnvssrndm 6116 | The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴) | ||
Theorem | cossxp 6117 | Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) | ||
Theorem | relrelss 6118 | Two ways to describe the structure of a two-place operation. (Contributed by NM, 17-Dec-2008.) |
⊢ ((Rel 𝐴 ∧ Rel dom 𝐴) ↔ 𝐴 ⊆ ((V × V) × V)) | ||
Theorem | unielrel 6119 | The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.) |
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∪ 𝐴 ∈ ∪ 𝑅) | ||
Theorem | relfld 6120 | The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.) |
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅)) | ||
Theorem | relresfld 6121 | Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.) |
⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) = 𝑅) | ||
Theorem | relcoi2 6122 | Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.) |
⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅) | ||
Theorem | relcoi1 6123 | Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011.) (Proof shortened by OpenAI, 3-Jul-2020.) |
⊢ (Rel 𝑅 → (𝑅 ∘ ( I ↾ ∪ ∪ 𝑅)) = 𝑅) | ||
Theorem | unidmrn 6124 | The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.) |
⊢ ∪ ∪ ◡𝐴 = (dom 𝐴 ∪ ran 𝐴) | ||
Theorem | relcnvfld 6125 | if 𝑅 is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.) |
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ◡𝑅) | ||
Theorem | dfdm2 6126 | Alternate definition of domain df-dm 5559 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.) |
⊢ dom 𝐴 = ∪ ∪ (◡𝐴 ∘ 𝐴) | ||
Theorem | unixp 6127 | The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006.) |
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) | ||
Theorem | unixp0 6128 | A Cartesian product is empty iff its union is empty. (Contributed by NM, 20-Sep-2006.) |
⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (𝐴 × 𝐵) = ∅) | ||
Theorem | unixpid 6129 | Field of a Cartesian square. (Contributed by FL, 10-Oct-2009.) |
⊢ ∪ ∪ (𝐴 × 𝐴) = 𝐴 | ||
Theorem | ressn 6130 | Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐴 ↾ {𝐵}) = ({𝐵} × (𝐴 “ {𝐵})) | ||
Theorem | cnviin 6131* | The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012.) |
⊢ (𝐴 ≠ ∅ → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) | ||
Theorem | cnvpo 6132 | The converse of a partial order relation is a partial order relation. (Contributed by NM, 15-Jun-2005.) |
⊢ (𝑅 Po 𝐴 ↔ ◡𝑅 Po 𝐴) | ||
Theorem | cnvso 6133 | The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005.) |
⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴) | ||
Theorem | xpco 6134 | Composition of two Cartesian products. (Contributed by Thierry Arnoux, 17-Nov-2017.) |
⊢ (𝐵 ≠ ∅ → ((𝐵 × 𝐶) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐶)) | ||
Theorem | xpcoid 6135 | Composition of two Cartesian squares. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) = (𝐴 × 𝐴) | ||
Theorem | elsnxp 6136* | Membership in a Cartesian product with a singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = 〈𝑋, 𝑦〉)) | ||
Theorem | reu3op 6137* | 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 6138* | 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 6139* | 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 6140* | 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.) |
⊢ (𝑝 = 〈𝑎, 𝑏〉 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (∃!𝑝 ∈ (𝐴 × 𝐵)𝜑 → ∃!𝑎 ∈ 𝐴 ∃!𝑏 ∈ 𝐵 𝜒) | ||
Syntax | cpred 6141 | The predecessors symbol. |
class Pred(𝑅, 𝐴, 𝑋) | ||
Definition | df-pred 6142 | Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6155) . (Contributed by Scott Fenton, 29-Jan-2011.) |
⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) | ||
Theorem | predeq123 6143 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐵, 𝑌)) | ||
Theorem | predeq1 6144 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑅 = 𝑆 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐴, 𝑋)) | ||
Theorem | predeq2 6145 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 = 𝐵 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | predeq3 6146 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) | ||
Theorem | nfpred 6147 | Bound-variable hypothesis builder for the predecessor class. (Contributed by Scott Fenton, 9-Jun-2018.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑋 ⇒ ⊢ Ⅎ𝑥Pred(𝑅, 𝐴, 𝑋) | ||
Theorem | predpredss 6148 | If 𝐴 is a subset of 𝐵, then their predecessor classes are also subsets. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 ⊆ 𝐵 → Pred(𝑅, 𝐴, 𝑋) ⊆ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | predss 6149 | The predecessor class of 𝐴 is a subset of 𝐴. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴 | ||
Theorem | sspred 6150 | Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | dfpred2 6151* | An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 8-Feb-2011.) |
⊢ 𝑋 ∈ V ⇒ ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ {𝑦 ∣ 𝑦𝑅𝑋}) | ||
Theorem | dfpred3 6152* | An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ 𝑋 ∈ V ⇒ ⊢ Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋} | ||
Theorem | dfpred3g 6153* | An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑋 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}) | ||
Theorem | elpredim 6154 | Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012.) |
⊢ 𝑋 ∈ V ⇒ ⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌𝑅𝑋) | ||
Theorem | elpred 6155 | Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011.) |
⊢ 𝑌 ∈ V ⇒ ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌𝑅𝑋))) | ||
Theorem | elpredg 6156 | Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) |
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ 𝑌𝑅𝑋)) | ||
Theorem | predasetex 6157 | The predecessor class exists when 𝐴 does. (Contributed by Scott Fenton, 8-Feb-2011.) |
⊢ 𝐴 ∈ V ⇒ ⊢ Pred(𝑅, 𝐴, 𝑋) ∈ V | ||
Theorem | dffr4 6158* | Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 Pred(𝑅, 𝑥, 𝑦) = ∅)) | ||
Theorem | predel 6159 | Membership in the predecessor class implies membership in the base class. (Contributed by Scott Fenton, 11-Feb-2011.) |
⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌 ∈ 𝐴) | ||
Theorem | predpo 6160 | Property of the precessor class for partial orderings. (Contributed by Scott Fenton, 28-Apr-2012.) |
⊢ ((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋))) | ||
Theorem | predso 6161 | Property of the predecessor class for strict orderings. (Contributed by Scott Fenton, 11-Feb-2011.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋))) | ||
Theorem | predbrg 6162 | Closed form of elpredim 6154. (Contributed by Scott Fenton, 13-Apr-2011.) (Revised by NM, 5-Apr-2016.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)) → 𝑌𝑅𝑋) | ||
Theorem | setlikespec 6163 | If 𝑅 is set-like in 𝐴, then all predecessors classes of elements of 𝐴 exist. (Contributed by Scott Fenton, 20-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → Pred(𝑅, 𝐴, 𝑋) ∈ V) | ||
Theorem | predidm 6164 | Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011.) |
⊢ Pred(𝑅, Pred(𝑅, 𝐴, 𝑋), 𝑋) = Pred(𝑅, 𝐴, 𝑋) | ||
Theorem | predin 6165 | Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.) |
⊢ Pred(𝑅, (𝐴 ∩ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∩ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | predun 6166 | Union law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.) |
⊢ Pred(𝑅, (𝐴 ∪ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∪ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | preddif 6167 | Difference law for predecessor classes. (Contributed by Scott Fenton, 14-Apr-2011.) |
⊢ Pred(𝑅, (𝐴 ∖ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∖ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | predep 6168 | 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 | preddowncl 6169* | A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋))) | ||
Theorem | predpoirr 6170 | 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 6171 | 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 6172 | The predecessor class over ∅ is always ∅. (Contributed by Scott Fenton, 16-Apr-2011.) (Proof shortened by AV, 11-Jun-2021.) |
⊢ Pred(𝑅, ∅, 𝑋) = ∅ | ||
Theorem | tz6.26 6173* | 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.) |
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) | ||
Theorem | tz6.26i 6174* | All nonempty subclasses of a class having a well-founded 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 6175* | The Principle of Well-Founded 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 | wfii 6176* | The Principle of Well-Founded 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 6177* | Well-Founded Induction Schema. If a property passes from all elements less than 𝑦 of a well-founded class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 11-Feb-2011.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | wfis 6178* | Well-Founded Induction Schema. If all elements less than a given set 𝑥 of the well-founded 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 6179* | Well-Founded Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) |
⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | wfis2f 6180* | Well Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
Theorem | wfis2g 6181* | Well-Founded Induction Schema, using implicit substitution. (Contributed by Scott Fenton, 11-Feb-2011.) |
⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | wfis2 6182* | Well Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
Theorem | wfis3 6183* | Well Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 29-Jan-2011.) |
⊢ 𝑅 We 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝜒) | ||
Syntax | word 6184 | Extend the definition of a wff to include the ordinal predicate. |
wff Ord 𝐴 | ||
Syntax | con0 6185 | 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 6186 | Extend the definition of a wff to include the limit ordinal predicate. |
wff Lim 𝐴 | ||
Syntax | csuc 6187 | Extend class notation to include the successor function. |
class suc 𝐴 | ||
Definition | df-ord 6188 | 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. (Contributed by NM, 17-Sep-1993.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴)) | ||
Definition | df-on 6189 | 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 6190 | 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 6241, dflim3 7550, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.) |
⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | ||
Definition | df-suc 6191 | Define the successor of a class. When applied to an ordinal number, the successor means the same thing as "plus 1" (see oa1suc 8147). Definition 7.22 of [TakeutiZaring] p. 41, who use "+ 1" to denote this function. 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 6260), so that the successor of any ordinal class is still an ordinal class (ordsuc 7517), 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 6192 | Equality theorem for the ordinal predicate. (Contributed by NM, 17-Sep-1993.) |
⊢ (𝐴 = 𝐵 → (Ord 𝐴 ↔ Ord 𝐵)) | ||
Theorem | elong 6193 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ On ↔ Ord 𝐴)) | ||
Theorem | elon 6194 | An ordinal number is an ordinal set. (Contributed by NM, 5-Jun-1994.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (𝐴 ∈ On ↔ Ord 𝐴) | ||
Theorem | eloni 6195 | An ordinal number has the ordinal property. (Contributed by NM, 5-Jun-1994.) |
⊢ (𝐴 ∈ On → Ord 𝐴) | ||
Theorem | elon2 6196 | An ordinal number is an ordinal set. (Contributed by NM, 8-Feb-2004.) |
⊢ (𝐴 ∈ On ↔ (Ord 𝐴 ∧ 𝐴 ∈ V)) | ||
Theorem | limeq 6197 | Equality theorem for the limit predicate. (Contributed by NM, 22-Apr-1994.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
⊢ (𝐴 = 𝐵 → (Lim 𝐴 ↔ Lim 𝐵)) | ||
Theorem | ordwe 6198 | Membership well-orders every ordinal. Proposition 7.4 of [TakeutiZaring] p. 36. (Contributed by NM, 3-Apr-1994.) |
⊢ (Ord 𝐴 → E We 𝐴) | ||
Theorem | ordtr 6199 | An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.) |
⊢ (Ord 𝐴 → Tr 𝐴) | ||
Theorem | ordfr 6200 | 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 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |