Home | Metamath
Proof Explorer Theorem List (p. 331 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pocnv 33001 | The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴) | ||
Theorem | socnv 33002 | The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴) | ||
Theorem | sotrd 33003 | Transitivity law for strict orderings, deduction form. (Contributed by Scott Fenton, 24-Nov-2021.) |
⊢ (𝜑 → 𝑅 Or 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ (𝜑 → 𝑍 ∈ 𝐴) & ⊢ (𝜑 → 𝑋𝑅𝑌) & ⊢ (𝜑 → 𝑌𝑅𝑍) ⇒ ⊢ (𝜑 → 𝑋𝑅𝑍) | ||
Theorem | sotr3 33004 | Transitivity law for strict orderings. (Contributed by Scott Fenton, 24-Nov-2021.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴)) → ((𝑋𝑅𝑌 ∧ ¬ 𝑍𝑅𝑌) → 𝑋𝑅𝑍)) | ||
Theorem | sotrine 33005 | Trichotomy law for strict orderings. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ≠ 𝐶 ↔ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) | ||
Theorem | eqfunresadj 33006 | Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021.) |
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ (𝐹‘𝑌) = (𝐺‘𝑌))) → (𝐹 ↾ (𝑋 ∪ {𝑌})) = (𝐺 ↾ (𝑋 ∪ {𝑌}))) | ||
Theorem | eqfunressuc 33007 | Law for equality of restriction to successors. This is primarily useful when 𝑋 is an ordinal, but it does not require that. (Contributed by Scott Fenton, 6-Dec-2021.) |
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑋 ∈ dom 𝐹 ∧ 𝑋 ∈ dom 𝐺 ∧ (𝐹‘𝑋) = (𝐺‘𝑋))) → (𝐹 ↾ suc 𝑋) = (𝐺 ↾ suc 𝑋)) | ||
Theorem | funeldmb 33008 | If ∅ is not part of the range of a function 𝐹, then 𝐴 is in the domain of 𝐹 iff (𝐹‘𝐴) ≠ ∅. (Contributed by Scott Fenton, 7-Dec-2021.) |
⊢ ((Fun 𝐹 ∧ ¬ ∅ ∈ ran 𝐹) → (𝐴 ∈ dom 𝐹 ↔ (𝐹‘𝐴) ≠ ∅)) | ||
Theorem | elintfv 33009* | Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ 𝑋 ∈ V ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑋 ∈ ∩ (𝐹 “ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ (𝐹‘𝑦))) | ||
Theorem | funpsstri 33010 | A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.) |
⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹)) | ||
Theorem | fundmpss 33011 | If a class 𝐹 is a proper subset of a function 𝐺, then dom 𝐹 ⊊ dom 𝐺. (Contributed by Scott Fenton, 20-Apr-2011.) |
⊢ (Fun 𝐺 → (𝐹 ⊊ 𝐺 → dom 𝐹 ⊊ dom 𝐺)) | ||
Theorem | fvresval 33012 | The value of a function at a restriction is either null or the same as the function itself. (Contributed by Scott Fenton, 4-Sep-2011.) |
⊢ (((𝐹 ↾ 𝐵)‘𝐴) = (𝐹‘𝐴) ∨ ((𝐹 ↾ 𝐵)‘𝐴) = ∅) | ||
Theorem | funsseq 33013 | Given two functions with equal domains, equality only requires one direction of the subset relationship. (Contributed by Scott Fenton, 24-Apr-2012.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
⊢ ((Fun 𝐹 ∧ Fun 𝐺 ∧ dom 𝐹 = dom 𝐺) → (𝐹 = 𝐺 ↔ 𝐹 ⊆ 𝐺)) | ||
Theorem | fununiq 33014 | The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶)) | ||
Theorem | funbreq 33015 | An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶)) | ||
Theorem | br1steq 33016 | Uniqueness condition for the binary relation 1st. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉1st 𝐶 ↔ 𝐶 = 𝐴) | ||
Theorem | br2ndeq 33017 | Uniqueness condition for the binary relation 2nd. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉2nd 𝐶 ↔ 𝐶 = 𝐵) | ||
Theorem | dfdm5 33018 | Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ dom 𝐴 = ((1st ↾ (V × V)) “ 𝐴) | ||
Theorem | dfrn5 33019 | Definition of range in terms of 2nd and image. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
⊢ ran 𝐴 = ((2nd ↾ (V × V)) “ 𝐴) | ||
Theorem | opelco3 33020 | Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.) |
⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) | ||
Theorem | elima4 33021 | Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.) |
⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅) | ||
Theorem | fv1stcnv 33022 | The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = 〈𝑋, 𝑌〉) | ||
Theorem | fv2ndcnv 33023 | The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉) | ||
Theorem | imaindm 33024 | The image is unaffected by intersection with the domain. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ (𝑅 “ 𝐴) = (𝑅 “ (𝐴 ∩ dom 𝑅)) | ||
Theorem | setinds 33025* | Principle of set induction (or E-induction). If a property passes from all elements of 𝑥 to 𝑥 itself, then it holds for all 𝑥. (Contributed by Scott Fenton, 10-Mar-2011.) |
⊢ (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | setinds2f 33026* | E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | setinds2 33027* | E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | elpotr 33028* | A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.) |
⊢ (∀𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴) | ||
Theorem | dford5reg 33029 | Given ax-reg 9058, an ordinal is a transitive class totally ordered by the membership relation. (Contributed by Scott Fenton, 28-Jan-2011.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E Or 𝐴)) | ||
Theorem | dfon2lem1 33030 | Lemma for dfon2 33039. (Contributed by Scott Fenton, 28-Feb-2011.) |
⊢ Tr ∪ {𝑥 ∣ (𝜑 ∧ Tr 𝑥 ∧ 𝜓)} | ||
Theorem | dfon2lem2 33031* | Lemma for dfon2 33039. (Contributed by Scott Fenton, 28-Feb-2011.) |
⊢ ∪ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓)} ⊆ 𝐴 | ||
Theorem | dfon2lem3 33032* | Lemma for dfon2 33039. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧))) | ||
Theorem | dfon2lem4 33033* | Lemma for dfon2 33039. If two sets satisfy the new definition, then one is a subset of the other. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ 𝐴)) | ||
Theorem | dfon2lem5 33034* | Lemma for dfon2 33039. Two sets satisfying the new definition also satisfy trichotomy with respect to ∈. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ ((∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) ∧ ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵)) → (𝐴 ∈ 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 ∈ 𝐴)) | ||
Theorem | dfon2lem6 33035* | Lemma for dfon2 33039. A transitive class of sets satisfying the new definition satisfies the new definition. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ ((Tr 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑧((𝑧 ⊊ 𝑥 ∧ Tr 𝑧) → 𝑧 ∈ 𝑥)) → ∀𝑦((𝑦 ⊊ 𝑆 ∧ Tr 𝑦) → 𝑦 ∈ 𝑆)) | ||
Theorem | dfon2lem7 33036* | Lemma for dfon2 33039. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵))) | ||
Theorem | dfon2lem8 33037* | Lemma for dfon2 33039. The intersection of a nonempty class 𝐴 of new ordinals is itself a new ordinal and is contained within 𝐴 (Contributed by Scott Fenton, 26-Feb-2011.) |
⊢ ((𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)) → (∀𝑧((𝑧 ⊊ ∩ 𝐴 ∧ Tr 𝑧) → 𝑧 ∈ ∩ 𝐴) ∧ ∩ 𝐴 ∈ 𝐴)) | ||
Theorem | dfon2lem9 33038* | Lemma for dfon2 33039. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E Fr 𝐴) | ||
Theorem | dfon2 33039* | On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers", American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011.) |
⊢ On = {𝑥 ∣ ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥)} | ||
Theorem | rdgprc0 33040 | The value of the recursive definition generator at ∅ when the base value is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (¬ 𝐼 ∈ V → (rec(𝐹, 𝐼)‘∅) = ∅) | ||
Theorem | rdgprc 33041 | The value of the recursive definition generator when 𝐼 is a proper class. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (¬ 𝐼 ∈ V → rec(𝐹, 𝐼) = rec(𝐹, ∅)) | ||
Theorem | dfrdg2 33042* | Alternate definition of the recursive function generator when 𝐼 is a set. (Contributed by Scott Fenton, 26-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝐼 ∈ 𝑉 → rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, 𝐼, if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))}) | ||
Theorem | dfrdg3 33043* | Generalization of dfrdg2 33042 to remove sethood requirement. (Contributed by Scott Fenton, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ rec(𝐹, 𝐼) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = if(𝑦 = ∅, if(𝐼 ∈ V, 𝐼, ∅), if(Lim 𝑦, ∪ (𝑓 “ 𝑦), (𝐹‘(𝑓‘∪ 𝑦)))))} | ||
Theorem | axextdfeq 33044 | A version of ax-ext 2795 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ((𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤))) | ||
Theorem | ax8dfeq 33045 | A version of ax-8 2116 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑦)) | ||
Theorem | axextdist 33046 | ax-ext 2795 with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)) | ||
Theorem | axextbdist 33047 | axextb 2798 with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))) | ||
Theorem | 19.12b 33048* | Version of 19.12vv 2368 with not-free hypotheses, instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑦𝜑 & ⊢ Ⅎ𝑥𝜓 ⇒ ⊢ (∃𝑥∀𝑦(𝜑 → 𝜓) ↔ ∀𝑦∃𝑥(𝜑 → 𝜓)) | ||
Theorem | exnel 33049 | There is always a set not in 𝑦. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ∃𝑥 ¬ 𝑥 ∈ 𝑦 | ||
Theorem | distel 33050 | Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5272 and elirrv 9062.) (Contributed by Scott Fenton, 15-Dec-2010.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑥 ↔ ¬ ∀𝑦 ¬ 𝑥 ∈ 𝑦) | ||
Theorem | axextndbi 33051 | axextnd 10015 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.) |
⊢ ∃𝑧(𝑥 = 𝑦 ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | ||
Theorem | hbntg 33052 | A more general form of hbnt 2302. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | hbimtg 33053 | A more general and closed form of hbim 2307. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ((∀𝑥(𝜑 → ∀𝑥𝜒) ∧ (𝜓 → ∀𝑥𝜃)) → ((𝜒 → 𝜓) → ∀𝑥(𝜑 → 𝜃))) | ||
Theorem | hbaltg 33054 | A more general and closed form of hbal 2174. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓)) | ||
Theorem | hbng 33055 | A more general form of hbn 2303. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (𝜑 → ∀𝑥𝜓) ⇒ ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜑) | ||
Theorem | hbimg 33056 | A more general form of hbim 2307. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜃) ⇒ ⊢ ((𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜃)) | ||
Theorem | tfisg 33057* | A closed form of tfis 7571. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥 ∈ On 𝜑) | ||
Syntax | ctrpred 33058 | Define the transitive predecessor class as a class. |
class TrPred(𝑅, 𝐴, 𝑋) | ||
Definition | df-trpred 33059* | Define the transitive predecessors of a class 𝑋 under a relationship 𝑅 and a class 𝐴. This class can be thought of as the "smallest" class containing all elements of 𝐴 that are linked to 𝑋 by a chain of 𝑅 relationships (see trpredtr 33071 and trpredmintr 33072). Definition based off of Lemma 4.2 of Don Monk's notes for Advanced Set Theory, which can be found at http://euclid.colorado.edu/~monkd/settheory 33072 (check The Internet Archive for it now as Prof. Monk appears to have rewritten his website). (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ TrPred(𝑅, 𝐴, 𝑋) = ∪ ran (rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω) | ||
Theorem | dftrpred2 33060* | A definition of the transitive predecessors of a class in terms of indexed union. (Contributed by Scott Fenton, 28-Apr-2012.) |
⊢ TrPred(𝑅, 𝐴, 𝑋) = ∪ 𝑖 ∈ ω ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) | ||
Theorem | trpredeq1 33061 | Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑅 = 𝑆 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑆, 𝐴, 𝑋)) | ||
Theorem | trpredeq2 33062 | Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 = 𝐵 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐵, 𝑋)) | ||
Theorem | trpredeq3 33063 | Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑋 = 𝑌 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐴, 𝑌)) | ||
Theorem | trpredeq1d 33064 | Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑆, 𝐴, 𝑋)) | ||
Theorem | trpredeq2d 33065 | Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐵, 𝑋)) | ||
Theorem | trpredeq3d 33066 | Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝜑 → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐴, 𝑌)) | ||
Theorem | eltrpred 33067* | A class is a transitive predecessor iff it is in some value of the underlying function. This theorem is not really meant to be used directly: instead refer to trpredpred 33069 and trpredmintr 33072. (Contributed by Scott Fenton, 28-Apr-2012.) |
⊢ (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) ↔ ∃𝑖 ∈ ω 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) | ||
Theorem | trpredlem1 33068* | Technical lemma for transitive predecessors properties. All values of the transitive predecessors' underlying function are subsets of the base set. (Contributed by Scott Fenton, 28-Apr-2012.) |
⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖) ⊆ 𝐴) | ||
Theorem | trpredpred 33069 | Assuming it exists, the predecessor class is a subset of the transitive predecessors. (Contributed by Scott Fenton, 18-Feb-2011.) |
⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → Pred(𝑅, 𝐴, 𝑋) ⊆ TrPred(𝑅, 𝐴, 𝑋)) | ||
Theorem | trpredss 33070 | The transitive predecessors form a subset of the base class. (Contributed by Scott Fenton, 20-Feb-2011.) |
⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐴) | ||
Theorem | trpredtr 33071 | The transitive predecessors are transitive in 𝑅 and 𝐴 (Contributed by Scott Fenton, 20-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) → Pred(𝑅, 𝐴, 𝑌) ⊆ TrPred(𝑅, 𝐴, 𝑋))) | ||
Theorem | trpredmintr 33072* | The transitive predecessors form the smallest class transitive in 𝑅 and 𝐴. That is, if 𝐵 is another 𝑅, 𝐴 transitive class containing Pred(𝑅, 𝐴, 𝑋), then TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐵 (Contributed by Scott Fenton, 25-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) ∧ (∀𝑦 ∈ 𝐵 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 ∧ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐵)) → TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐵) | ||
Theorem | trpredelss 33073 | Given a transitive predecessor 𝑌 of 𝑋, the transitive predecessors of 𝑌 are a subset of the transitive predecessors of 𝑋. (Contributed by Scott Fenton, 25-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) → TrPred(𝑅, 𝐴, 𝑌) ⊆ TrPred(𝑅, 𝐴, 𝑋))) | ||
Theorem | dftrpred3g 33074* | The transitive predecessors of 𝑋 are equal to the predecessors of 𝑋 together with their transitive predecessors. (Contributed by Scott Fenton, 26-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → TrPred(𝑅, 𝐴, 𝑋) = (Pred(𝑅, 𝐴, 𝑋) ∪ ∪ 𝑦 ∈ Pred (𝑅, 𝐴, 𝑋)TrPred(𝑅, 𝐴, 𝑦))) | ||
Theorem | dftrpred4g 33075* | Another recursive expression for the transitive predecessors. (Contributed by Scott Fenton, 27-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → TrPred(𝑅, 𝐴, 𝑋) = ∪ 𝑦 ∈ Pred (𝑅, 𝐴, 𝑋)({𝑦} ∪ TrPred(𝑅, 𝐴, 𝑦))) | ||
Theorem | trpredpo 33076 | If 𝑅 partially orders 𝐴, then the transitive predecessors are the same as the immediate predecessors . (Contributed by Scott Fenton, 28-Apr-2012.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ ((𝑅 Po 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → TrPred(𝑅, 𝐴, 𝑋) = Pred(𝑅, 𝐴, 𝑋)) | ||
Theorem | trpred0 33077 | The class of transitive predecessors is empty when 𝐴 is empty. (Contributed by Scott Fenton, 30-Apr-2012.) |
⊢ TrPred(𝑅, ∅, 𝑋) = ∅ | ||
Theorem | trpredex 33078 | The transitive predecessors of a relation form a set (NOTE: this is the first theorem in the transitive predecessor series that requires infinity). (Contributed by Scott Fenton, 18-Feb-2011.) |
⊢ TrPred(𝑅, 𝐴, 𝑋) ∈ V | ||
Theorem | trpredrec 33079* | If 𝑌 is an 𝑅, 𝐴 transitive predecessor, then it is either an immediate predecessor or there is a transitive predecessor between 𝑌 and 𝑋. (Contributed by Scott Fenton, 9-May-2012.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑅 Se 𝐴) → (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) → (𝑌 ∈ Pred(𝑅, 𝐴, 𝑋) ∨ ∃𝑧 ∈ TrPred (𝑅, 𝐴, 𝑋)𝑌𝑅𝑧))) | ||
Theorem | frpomin 33080* | Every (possibly proper) subclass of a class 𝐴 with a founded, partial-ordering, set-like relation 𝑅 has a minimal element. The additional condition of partial ordering over frmin 33086 enables avoiding infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | frpomin2 33081* | Every (possibly proper) subclass of a class 𝐴 with a founded, partial-ordering, set-like relation 𝑅 has a minimal element. The additional condition of partial ordering over frmin 33086 enables avoiding infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑥) = ∅) | ||
Theorem | frpoind 33082* | The principle of founded induction over a partial ordering. This theorem is a version of frind 33087 that does not require infinity, and can be used to prove wfi 6183 and tfi 7570. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵) | ||
Theorem | frpoinsg 33083* | Founded, Partial-Ordering Induction Schema. If a property passes from all elements less than 𝑦 of a founded, partially-ordered 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 33084* | Founded Partial Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frpoins2g 33085* | Founded Partial Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frmin 33086* | Every (possibly proper) subclass of a class 𝐴 with a founded, set-like relation 𝑅 has a minimal element. Lemma 4.3 of Don Monk's notes for Advanced Set Theory, which can be found at http://euclid.colorado.edu/~monkd/settheory. This is a very strong generalization of tz6.26 6181 and tz7.5 6214. (Contributed by Scott Fenton, 4-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) | ||
Theorem | frind 33087* | The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 33086). This principle states that if 𝐵 is a subclass of a founded class 𝐴 with the property that every element of 𝐵 whose initial segment is included in 𝐴 is itself equal to 𝐴. Compare wfi 6183 and tfi 7570, which are special cases of this theorem that do not require the axiom of infinity to prove. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵) | ||
Theorem | frindi 33088* | The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 33086). This principle states that if 𝐵 is a subclass of a founded class 𝐴 with the property that every element of 𝐵 whose initial segment is included in 𝐴 is itself equal to 𝐴. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 ⇒ ⊢ ((𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵)) → 𝐴 = 𝐵) | ||
Theorem | frinsg 33089* | Founded Induction Schema. If a property passes from all elements less than 𝑦 of a founded class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 7-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frins 33090* | Founded Induction Schema. If a property passes from all elements less than 𝑦 of a founded class 𝐴 to 𝑦 itself (induction hypothesis), then the property holds for all elements of 𝐴. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)[𝑧 / 𝑦]𝜑 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
Theorem | frins2fg 33091* | Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 7-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frins2f 33092* | Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
Theorem | frins2g 33093* | Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 8-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frins2 33094* | Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝑦 ∈ 𝐴 → 𝜑) | ||
Theorem | frins3 33095* | Founded Induction schema, using implicit substitution. (Contributed by Scott Fenton, 6-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ 𝑅 Fr 𝐴 & ⊢ 𝑅 Se 𝐴 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) & ⊢ (𝑦 = 𝐵 → (𝜑 ↔ 𝜒)) & ⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) ⇒ ⊢ (𝐵 ∈ 𝐴 → 𝜒) | ||
Theorem | orderseqlem 33096* | Lemma for poseq 33097 and soseq 33098. The function value of a sequene is either in 𝐴 or null. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} ⇒ ⊢ (𝐺 ∈ 𝐹 → (𝐺‘𝑋) ∈ (𝐴 ∪ {∅})) | ||
Theorem | poseq 33097* | A partial ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝑅 Po (𝐴 ∪ {∅}) & ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} & ⊢ 𝑆 = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))} ⇒ ⊢ 𝑆 Po 𝐹 | ||
Theorem | soseq 33098* | A linear ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝑅 Or (𝐴 ∪ {∅}) & ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} & ⊢ 𝑆 = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))} & ⊢ ¬ ∅ ∈ 𝐴 ⇒ ⊢ 𝑆 Or 𝐹 | ||
Syntax | cwsuc 33099 | Declare the syntax for well-founded successor. |
class wsuc(𝑅, 𝐴, 𝑋) | ||
Syntax | cwlim 33100 | Declare the syntax for well-founded limit class. |
class WLim(𝑅, 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |