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