Home | Metamath
Proof Explorer Theorem List (p. 63 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rnco 6201 | 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 6202 | The range of the composition of two classes. (Contributed by NM, 27-Mar-2008.) |
⊢ ran (𝐴 ∘ 𝐵) = (𝐴 “ ran 𝐵) | ||
Theorem | dmco 6203 | The domain of a composition. Exercise 27 of [Enderton] p. 53. (Contributed by NM, 4-Feb-2004.) |
⊢ dom (𝐴 ∘ 𝐵) = (◡𝐵 “ dom 𝐴) | ||
Theorem | coeq0 6204 | 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 6196 and coundir 6197 to prune meaningless terms in the result. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
⊢ ((𝐴 ∘ 𝐵) = ∅ ↔ (dom 𝐴 ∩ ran 𝐵) = ∅) | ||
Theorem | coiun 6205* | Composition with an indexed union. (Contributed by NM, 21-Dec-2008.) |
⊢ (𝐴 ∘ ∪ 𝑥 ∈ 𝐶 𝐵) = ∪ 𝑥 ∈ 𝐶 (𝐴 ∘ 𝐵) | ||
Theorem | cocnvcnv1 6206 | A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007.) |
⊢ (◡◡𝐴 ∘ 𝐵) = (𝐴 ∘ 𝐵) | ||
Theorem | cocnvcnv2 6207 | A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007.) |
⊢ (𝐴 ∘ ◡◡𝐵) = (𝐴 ∘ 𝐵) | ||
Theorem | cores2 6208 | Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006.) |
⊢ (dom 𝐴 ⊆ 𝐶 → (𝐴 ∘ ◡(◡𝐵 ↾ 𝐶)) = (𝐴 ∘ 𝐵)) | ||
Theorem | co02 6209 | Composition with the empty set. Theorem 20 of [Suppes] p. 63. (Contributed by NM, 24-Apr-2004.) |
⊢ (𝐴 ∘ ∅) = ∅ | ||
Theorem | co01 6210 | Composition with the empty set. (Contributed by NM, 24-Apr-2004.) |
⊢ (∅ ∘ 𝐴) = ∅ | ||
Theorem | coi1 6211 | 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 6212 | 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 6213 | Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.) |
⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵) | ||
Theorem | coass 6214 | 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 6215 | General form of relcnvtr 6216. (Contributed by Peter Mazsa, 17-Oct-2023.) |
⊢ ((Rel 𝑅 ∧ Rel 𝑆 ∧ Rel 𝑇) → ((𝑅 ∘ 𝑆) ⊆ 𝑇 ↔ (◡𝑆 ∘ ◡𝑅) ⊆ ◡𝑇)) | ||
Theorem | relcnvtr 6216 | 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 6217 | 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.) (Proof shortened by SN, 23-Dec-2024.) |
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴)) | ||
Theorem | relssdmrnOLD 6218 | Obsolete version of relssdmrn 6217 as of 23-Dec-2024. (Contributed by NM, 3-Aug-1994.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ (Rel 𝐴 → 𝐴 ⊆ (dom 𝐴 × ran 𝐴)) | ||
Theorem | resssxp 6219 | If the 𝑅-image of a class 𝐴 is a subclass of 𝐵, then the restriction of 𝑅 to 𝐴 is a subset of the Cartesian product of 𝐴 and 𝐵. (Contributed by RP, 24-Dec-2019.) |
⊢ ((𝑅 “ 𝐴) ⊆ 𝐵 ↔ (𝑅 ↾ 𝐴) ⊆ (𝐴 × 𝐵)) | ||
Theorem | cnvssrndm 6220 | The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017.) |
⊢ ◡𝐴 ⊆ (ran 𝐴 × dom 𝐴) | ||
Theorem | cossxp 6221 | Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ (𝐴 ∘ 𝐵) ⊆ (dom 𝐵 × ran 𝐴) | ||
Theorem | relrelss 6222 | 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 6223 | The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006.) |
⊢ ((Rel 𝑅 ∧ 𝐴 ∈ 𝑅) → ∪ 𝐴 ∈ ∪ 𝑅) | ||
Theorem | relfld 6224 | The double union of a relation is its field. (Contributed by NM, 17-Sep-2006.) |
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = (dom 𝑅 ∪ ran 𝑅)) | ||
Theorem | relresfld 6225 | Restriction of a relation to its field. (Contributed by FL, 15-Apr-2012.) |
⊢ (Rel 𝑅 → (𝑅 ↾ ∪ ∪ 𝑅) = 𝑅) | ||
Theorem | relcoi2 6226 | Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011.) |
⊢ (Rel 𝑅 → (( I ↾ ∪ ∪ 𝑅) ∘ 𝑅) = 𝑅) | ||
Theorem | relcoi1 6227 | 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 6228 | The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008.) |
⊢ ∪ ∪ ◡𝐴 = (dom 𝐴 ∪ ran 𝐴) | ||
Theorem | relcnvfld 6229 | if 𝑅 is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009.) |
⊢ (Rel 𝑅 → ∪ ∪ 𝑅 = ∪ ∪ ◡𝑅) | ||
Theorem | dfdm2 6230 | Alternate definition of domain df-dm 5641 that doesn't require dummy variables. (Contributed by NM, 2-Aug-2010.) |
⊢ dom 𝐴 = ∪ ∪ (◡𝐴 ∘ 𝐴) | ||
Theorem | unixp 6231 | The double class union of a nonempty Cartesian product is the union of it members. (Contributed by NM, 17-Sep-2006.) |
⊢ ((𝐴 × 𝐵) ≠ ∅ → ∪ ∪ (𝐴 × 𝐵) = (𝐴 ∪ 𝐵)) | ||
Theorem | unixp0 6232 | A Cartesian product is empty iff its union is empty. (Contributed by NM, 20-Sep-2006.) |
⊢ ((𝐴 × 𝐵) = ∅ ↔ ∪ (𝐴 × 𝐵) = ∅) | ||
Theorem | unixpid 6233 | Field of a Cartesian square. (Contributed by FL, 10-Oct-2009.) |
⊢ ∪ ∪ (𝐴 × 𝐴) = 𝐴 | ||
Theorem | ressn 6234 | Restriction of a class to a singleton. (Contributed by Mario Carneiro, 28-Dec-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ (𝐴 ↾ {𝐵}) = ({𝐵} × (𝐴 “ {𝐵})) | ||
Theorem | cnviin 6235* | The converse of an intersection is the intersection of the converse. (Contributed by FL, 15-Oct-2012.) |
⊢ (𝐴 ≠ ∅ → ◡∩ 𝑥 ∈ 𝐴 𝐵 = ∩ 𝑥 ∈ 𝐴 ◡𝐵) | ||
Theorem | cnvpo 6236 | The converse of a partial order is a partial order. (Contributed by NM, 15-Jun-2005.) |
⊢ (𝑅 Po 𝐴 ↔ ◡𝑅 Po 𝐴) | ||
Theorem | cnvso 6237 | The converse of a strict order relation is a strict order relation. (Contributed by NM, 15-Jun-2005.) |
⊢ (𝑅 Or 𝐴 ↔ ◡𝑅 Or 𝐴) | ||
Theorem | xpco 6238 | Composition of two Cartesian products. (Contributed by Thierry Arnoux, 17-Nov-2017.) |
⊢ (𝐵 ≠ ∅ → ((𝐵 × 𝐶) ∘ (𝐴 × 𝐵)) = (𝐴 × 𝐶)) | ||
Theorem | xpcoid 6239 | Composition of two Cartesian squares. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
⊢ ((𝐴 × 𝐴) ∘ (𝐴 × 𝐴)) = (𝐴 × 𝐴) | ||
Theorem | elsnxp 6240* | Membership in a Cartesian product with a singleton. (Contributed by Thierry Arnoux, 10-Apr-2020.) (Proof shortened by JJ, 14-Jul-2021.) |
⊢ (𝑋 ∈ 𝑉 → (𝑍 ∈ ({𝑋} × 𝐴) ↔ ∃𝑦 ∈ 𝐴 𝑍 = ⟨𝑋, 𝑦⟩)) | ||
Theorem | reu3op 6241* | 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 6242* | 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 6243* | 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 6244* | 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 6245 | 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 6246 | Distribute proper substitution through a composition of relations. (Contributed by RP, 28-Jun-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌(𝐵 ∘ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∘ ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | snres0 6247 | Condition for restriction of a singleton to be empty. (Contributed by Scott Fenton, 9-Aug-2024.) |
⊢ 𝐵 ∈ V ⇒ ⊢ (({⟨𝐴, 𝐵⟩} ↾ 𝐶) = ∅ ↔ ¬ 𝐴 ∈ 𝐶) | ||
Theorem | imaindm 6248 | The image is unaffected by intersection with the domain. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ (𝑅 “ 𝐴) = (𝑅 “ (𝐴 ∩ dom 𝑅)) | ||
Syntax | cpred 6249 | The predecessors symbol. |
class Pred(𝑅, 𝐴, 𝑋) | ||
Definition | df-pred 6250 | Define the predecessor class of a binary relation. This is the class of all elements 𝑦 of 𝐴 such that 𝑦𝑅𝑋 (see elpred 6267). (Contributed by Scott Fenton, 29-Jan-2011.) |
⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) | ||
Theorem | predeq123 6251 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐵, 𝑌)) | ||
Theorem | predeq1 6252 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑅 = 𝑆 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑆, 𝐴, 𝑋)) | ||
Theorem | predeq2 6253 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 = 𝐵 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | predeq3 6254 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑋 = 𝑌 → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑌)) | ||
Theorem | nfpred 6255 | Bound-variable hypothesis builder for the predecessor class. (Contributed by Scott Fenton, 9-Jun-2018.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝑋 ⇒ ⊢ Ⅎ𝑥Pred(𝑅, 𝐴, 𝑋) | ||
Theorem | csbpredg 6256 | Move class substitution in and out of the predecessor class of a relation. (Contributed by ML, 25-Oct-2020.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌Pred(𝑅, 𝐷, 𝑋) = Pred(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝑋)) | ||
Theorem | predpredss 6257 | If 𝐴 is a subset of 𝐵, then their predecessor classes are also subsets. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 ⊆ 𝐵 → Pred(𝑅, 𝐴, 𝑋) ⊆ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | predss 6258 | The predecessor class of 𝐴 is a subset of 𝐴. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴 | ||
Theorem | sspred 6259 | Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵) → Pred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | dfpred2 6260* | An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 8-Feb-2011.) |
⊢ 𝑋 ∈ V ⇒ ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ {𝑦 ∣ 𝑦𝑅𝑋}) | ||
Theorem | dfpred3 6261* | An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ 𝑋 ∈ V ⇒ ⊢ Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋} | ||
Theorem | dfpred3g 6262* | An alternate definition of predecessor class when 𝑋 is a set. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑋 ∈ 𝑉 → Pred(𝑅, 𝐴, 𝑋) = {𝑦 ∈ 𝐴 ∣ 𝑦𝑅𝑋}) | ||
Theorem | elpredgg 6263 | 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 6264 | Membership in a predecessor class. (Contributed by Scott Fenton, 17-Apr-2011.) (Proof shortened by BJ, 16-Oct-2024.) |
⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ 𝑌𝑅𝑋)) | ||
Theorem | elpredimg 6265 | Membership in a predecessor class - implicative version. (Contributed by Scott Fenton, 9-May-2012.) Generalize to closed form. (Revised by BJ, 16-Oct-2024.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)) → 𝑌𝑅𝑋) | ||
Theorem | elpredim 6266 | 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 6267 | Membership in a predecessor class. (Contributed by Scott Fenton, 4-Feb-2011.) (Proof shortened by BJ, 16-Oct-2024.) |
⊢ 𝑌 ∈ V ⇒ ⊢ (𝑋 ∈ 𝐷 → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ↔ (𝑌 ∈ 𝐴 ∧ 𝑌𝑅𝑋))) | ||
Theorem | predexg 6268 | 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 6269 | Obsolete form of predexg 6268 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 6270* | Alternate definition of well-founded relation. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑅 Fr 𝐴 ↔ ∀𝑥((𝑥 ⊆ 𝐴 ∧ 𝑥 ≠ ∅) → ∃𝑦 ∈ 𝑥 Pred(𝑅, 𝑥, 𝑦) = ∅)) | ||
Theorem | predel 6271 | Membership in the predecessor class implies membership in the base class. (Contributed by Scott Fenton, 11-Feb-2011.) |
⊢ (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → 𝑌 ∈ 𝐴) | ||
Theorem | predbrg 6272 | Closed form of elpredim 6266. (Contributed by Scott Fenton, 13-Apr-2011.) (Revised by NM, 5-Apr-2016.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋)) → 𝑌𝑅𝑋) | ||
Theorem | predtrss 6273 | If 𝑅 is transitive over 𝐴 and 𝑌𝑅𝑋, then Pred(𝑅, 𝐴, 𝑌) is a subclass of Pred(𝑅, 𝐴, 𝑋). (Contributed by Scott Fenton, 28-Oct-2024.) |
⊢ ((((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ∧ 𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∧ 𝑋 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋)) | ||
Theorem | predpo 6274 | 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 6275 | Property of the predecessor class for strict total orders. (Contributed by Scott Fenton, 11-Feb-2011.) |
⊢ ((𝑅 Or 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ Pred(𝑅, 𝐴, 𝑋))) | ||
Theorem | setlikespec 6276 | 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 6277 | Idempotent law for the predecessor class. (Contributed by Scott Fenton, 29-Mar-2011.) |
⊢ Pred(𝑅, Pred(𝑅, 𝐴, 𝑋), 𝑋) = Pred(𝑅, 𝐴, 𝑋) | ||
Theorem | predin 6278 | Intersection law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.) |
⊢ Pred(𝑅, (𝐴 ∩ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∩ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | predun 6279 | Union law for predecessor classes. (Contributed by Scott Fenton, 29-Mar-2011.) |
⊢ Pred(𝑅, (𝐴 ∪ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∪ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | preddif 6280 | Difference law for predecessor classes. (Contributed by Scott Fenton, 14-Apr-2011.) |
⊢ Pred(𝑅, (𝐴 ∖ 𝐵), 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∖ Pred(𝑅, 𝐵, 𝑋)) | ||
Theorem | predep 6281 | 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 6282 | 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 6283* | A property of classes that are downward closed under predecessor. (Contributed by Scott Fenton, 13-Apr-2011.) |
⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑥 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑥) ⊆ 𝐵) → (𝑋 ∈ 𝐵 → Pred(𝑅, 𝐵, 𝑋) = Pred(𝑅, 𝐴, 𝑋))) | ||
Theorem | predpoirr 6284 | 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 6285 | 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 6286 | The predecessor class over ∅ is always ∅. (Contributed by Scott Fenton, 16-Apr-2011.) (Proof shortened by AV, 11-Jun-2021.) |
⊢ Pred(𝑅, ∅, 𝑋) = ∅ | ||
Theorem | dfse3 6287* | Alternate definition of set-like relationships. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ (𝑅 Se 𝐴 ↔ ∀𝑥 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑥) ∈ V) | ||
Theorem | predrelss 6288 | Subset carries from relation to predecessor class. (Contributed by Scott Fenton, 25-Nov-2024.) |
⊢ (𝑅 ⊆ 𝑆 → Pred(𝑅, 𝐴, 𝑋) ⊆ Pred(𝑆, 𝐴, 𝑋)) | ||
Theorem | predprc 6289 | The predecessor of a proper class is empty. (Contributed by Scott Fenton, 25-Nov-2024.) |
⊢ (¬ 𝑋 ∈ V → Pred(𝑅, 𝐴, 𝑋) = ∅) | ||
Theorem | predres 6290 | Predecessor class is unaffected by restriction to the base class. (Contributed by Scott Fenton, 25-Nov-2024.) |
⊢ Pred(𝑅, 𝐴, 𝑋) = Pred((𝑅 ↾ 𝐴), 𝐴, 𝑋) | ||
Theorem | frpomin 6291* | 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 9619 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | frpomin2 6292* | 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 9619 enables avoiding the axiom of infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑥) = ∅) | ||
Theorem | frpoind 6293* | The principle of well-founded induction over a partial order. This theorem is a version of frind 9620 that does not require the axiom of infinity and can be used to prove wfi 6301 and tfi 7780. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵) | ||
Theorem | frpoinsg 6294* | 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 6295* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frpoins2g 6296* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frpoins3g 6297* | Well-Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 19-Aug-2024.) |
⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ Pred (𝑅, 𝐴, 𝑥)𝜓 → 𝜑)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜒)) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝐵 ∈ 𝐴) → 𝜒) | ||
Theorem | tz6.26 6298* | 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 6299* | Obsolete proof of tz6.26 6298 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 6300* | 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(𝑅, 𝐵, 𝑦) = ∅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |