Home | Metamath
Proof Explorer Theorem List (p. 330 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 | sotrine 32901 | Trichotomy law for strict orderings. (Contributed by Scott Fenton, 8-Dec-2021.) |
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴)) → (𝐵 ≠ 𝐶 ↔ (𝐵𝑅𝐶 ∨ 𝐶𝑅𝐵))) | ||
Theorem | eqfunresadj 32902 | Law for adjoining an element to restrictions of functions. (Contributed by Scott Fenton, 6-Dec-2021.) |
⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐹 ↾ 𝑋) = (𝐺 ↾ 𝑋) ∧ (𝑌 ∈ dom 𝐹 ∧ 𝑌 ∈ dom 𝐺 ∧ (𝐹‘𝑌) = (𝐺‘𝑌))) → (𝐹 ↾ (𝑋 ∪ {𝑌})) = (𝐺 ↾ (𝑋 ∪ {𝑌}))) | ||
Theorem | eqfunressuc 32903 | 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 32904 | 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 32905* | Membership in an intersection of function values. (Contributed by Scott Fenton, 9-Dec-2021.) |
⊢ 𝑋 ∈ V ⇒ ⊢ ((𝐹 Fn 𝐴 ∧ 𝐵 ⊆ 𝐴) → (𝑋 ∈ ∩ (𝐹 “ 𝐵) ↔ ∀𝑦 ∈ 𝐵 𝑋 ∈ (𝐹‘𝑦))) | ||
Theorem | funpsstri 32906 | A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.) |
⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹)) | ||
Theorem | fundmpss 32907 | 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 32908 | 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 32909 | 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 32910 | The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶)) | ||
Theorem | funbreq 32911 | An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶)) | ||
Theorem | br1steq 32912 | 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 32913 | 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 32914 | 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 32915 | 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 32916 | Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.) |
⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) | ||
Theorem | elima4 32917 | Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.) |
⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅) | ||
Theorem | fv1stcnv 32918 | The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = 〈𝑋, 𝑌〉) | ||
Theorem | fv2ndcnv 32919 | The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉) | ||
Theorem | imaindm 32920 | The image is unaffected by intersection with the domain. (Contributed by Scott Fenton, 17-Dec-2021.) |
⊢ (𝑅 “ 𝐴) = (𝑅 “ (𝐴 ∩ dom 𝑅)) | ||
Theorem | setinds 32921* | 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 32922* | E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | setinds2 32923* | E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | elpotr 32924* | A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.) |
⊢ (∀𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴) | ||
Theorem | dford5reg 32925 | Given ax-reg 9045, 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 32926 | Lemma for dfon2 32935. (Contributed by Scott Fenton, 28-Feb-2011.) |
⊢ Tr ∪ {𝑥 ∣ (𝜑 ∧ Tr 𝑥 ∧ 𝜓)} | ||
Theorem | dfon2lem2 32927* | Lemma for dfon2 32935. (Contributed by Scott Fenton, 28-Feb-2011.) |
⊢ ∪ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓)} ⊆ 𝐴 | ||
Theorem | dfon2lem3 32928* | Lemma for dfon2 32935. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧))) | ||
Theorem | dfon2lem4 32929* | Lemma for dfon2 32935. 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 32930* | Lemma for dfon2 32935. 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 32931* | Lemma for dfon2 32935. 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 32932* | Lemma for dfon2 32935. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵))) | ||
Theorem | dfon2lem8 32933* | Lemma for dfon2 32935. 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 32934* | Lemma for dfon2 32935. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E Fr 𝐴) | ||
Theorem | dfon2 32935* | 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 32936 | 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 32937 | 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 32938* | 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 32939* | Generalization of dfrdg2 32938 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 32940 | A version of ax-ext 2793 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ((𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤))) | ||
Theorem | ax8dfeq 32941 | A version of ax-8 2107 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑦)) | ||
Theorem | axextdist 32942 | ax-ext 2793 with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)) | ||
Theorem | axextbdist 32943 | axextb 2796 with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))) | ||
Theorem | 19.12b 32944* | Version of 19.12vv 2360 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 32945 | There is always a set not in 𝑦. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ∃𝑥 ¬ 𝑥 ∈ 𝑦 | ||
Theorem | distel 32946 | Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 5262 and elirrv 9049.) (Contributed by Scott Fenton, 15-Dec-2010.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑥 ↔ ¬ ∀𝑦 ¬ 𝑥 ∈ 𝑦) | ||
Theorem | axextndbi 32947 | axextnd 10002 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.) |
⊢ ∃𝑧(𝑥 = 𝑦 ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | ||
Theorem | hbntg 32948 | A more general form of hbnt 2294. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | hbimtg 32949 | A more general and closed form of hbim 2299. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ((∀𝑥(𝜑 → ∀𝑥𝜒) ∧ (𝜓 → ∀𝑥𝜃)) → ((𝜒 → 𝜓) → ∀𝑥(𝜑 → 𝜃))) | ||
Theorem | hbaltg 32950 | A more general and closed form of hbal 2164. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓)) | ||
Theorem | hbng 32951 | A more general form of hbn 2295. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (𝜑 → ∀𝑥𝜓) ⇒ ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜑) | ||
Theorem | hbimg 32952 | A more general form of hbim 2299. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜃) ⇒ ⊢ ((𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜃)) | ||
Theorem | tfisg 32953* | A closed form of tfis 7557. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥 ∈ On 𝜑) | ||
Syntax | ctrpred 32954 | Define the transitive predecessor class as a class. |
class TrPred(𝑅, 𝐴, 𝑋) | ||
Definition | df-trpred 32955* | 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 32967 and trpredmintr 32968). 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 32968 (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 32956* | 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 32957 | Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑅 = 𝑆 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑆, 𝐴, 𝑋)) | ||
Theorem | trpredeq2 32958 | Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 = 𝐵 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐵, 𝑋)) | ||
Theorem | trpredeq3 32959 | Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑋 = 𝑌 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐴, 𝑌)) | ||
Theorem | trpredeq1d 32960 | Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑆, 𝐴, 𝑋)) | ||
Theorem | trpredeq2d 32961 | Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐵, 𝑋)) | ||
Theorem | trpredeq3d 32962 | Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝜑 → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐴, 𝑌)) | ||
Theorem | eltrpred 32963* | 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 32965 and trpredmintr 32968. (Contributed by Scott Fenton, 28-Apr-2012.) |
⊢ (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) ↔ ∃𝑖 ∈ ω 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) | ||
Theorem | trpredlem1 32964* | 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 32965 | 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 32966 | The transitive predecessors form a subset of the base class. (Contributed by Scott Fenton, 20-Feb-2011.) |
⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐴) | ||
Theorem | trpredtr 32967 | 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 32968* | 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 32969 | 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 32970* | 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 32971* | 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 32972 | 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 32973 | The class of transitive predecessors is empty when 𝐴 is empty. (Contributed by Scott Fenton, 30-Apr-2012.) |
⊢ TrPred(𝑅, ∅, 𝑋) = ∅ | ||
Theorem | trpredex 32974 | 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 32975* | 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 32976* | 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 32982 enables avoiding infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑦𝑅𝑥) | ||
Theorem | frpomin2 32977* | 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 32982 enables avoiding infinity. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑥 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑥) = ∅) | ||
Theorem | frpoind 32978* | The principle of founded induction over a partial ordering. This theorem is a version of frind 32983 that does not require infinity, and can be used to prove wfi 6175 and tfi 7556. (Contributed by Scott Fenton, 11-Feb-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝐴 (Pred(𝑅, 𝐴, 𝑦) ⊆ 𝐵 → 𝑦 ∈ 𝐵))) → 𝐴 = 𝐵) | ||
Theorem | frpoinsg 32979* | 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 32980* | Founded Partial Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ Ⅎ𝑦𝜓 & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frpoins2g 32981* | Founded Partial Induction schema, using implicit substitution. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (𝑦 ∈ 𝐴 → (∀𝑧 ∈ Pred (𝑅, 𝐴, 𝑦)𝜓 → 𝜑)) & ⊢ (𝑦 = 𝑧 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → ∀𝑦 ∈ 𝐴 𝜑) | ||
Theorem | frmin 32982* | 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 6173 and tz7.5 6206. (Contributed by Scott Fenton, 4-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) | ||
Theorem | frind 32983* | The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 32982). 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 6175 and tfi 7556, 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 32984* | The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 32982). 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 32985* | 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 32986* | 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 32987* | 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 32988* | 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 32989* | 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 32990* | 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 32991* | 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 32992* | Lemma for poseq 32993 and soseq 32994. The function value of a sequene is either in 𝐴 or null. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} ⇒ ⊢ (𝐺 ∈ 𝐹 → (𝐺‘𝑋) ∈ (𝐴 ∪ {∅})) | ||
Theorem | poseq 32993* | A partial ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝑅 Po (𝐴 ∪ {∅}) & ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} & ⊢ 𝑆 = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))} ⇒ ⊢ 𝑆 Po 𝐹 | ||
Theorem | soseq 32994* | A linear ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝑅 Or (𝐴 ∪ {∅}) & ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} & ⊢ 𝑆 = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))} & ⊢ ¬ ∅ ∈ 𝐴 ⇒ ⊢ 𝑆 Or 𝐹 | ||
Syntax | cwsuc 32995 | Declare the syntax for well-founded successor. |
class wsuc(𝑅, 𝐴, 𝑋) | ||
Syntax | cwlim 32996 | Declare the syntax for well-founded limit class. |
class WLim(𝑅, 𝐴) | ||
Definition | df-wsuc 32997 | Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
⊢ wsuc(𝑅, 𝐴, 𝑋) = inf(Pred(◡𝑅, 𝐴, 𝑋), 𝐴, 𝑅) | ||
Definition | df-wlim 32998* | Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) (Revised by AV, 10-Oct-2021.) |
⊢ WLim(𝑅, 𝐴) = {𝑥 ∈ 𝐴 ∣ (𝑥 ≠ inf(𝐴, 𝐴, 𝑅) ∧ 𝑥 = sup(Pred(𝑅, 𝐴, 𝑥), 𝐴, 𝑅))} | ||
Theorem | wsuceq123 32999 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) (Proof shortened by AV, 10-Oct-2021.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌) → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐵, 𝑌)) | ||
Theorem | wsuceq1 33000 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 = 𝑆 → wsuc(𝑅, 𝐴, 𝑋) = wsuc(𝑆, 𝐴, 𝑋)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |