Home | Metamath
Proof Explorer Theorem List (p. 310 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | br4 30901* | Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013.) (Revised by Mario Carneiro, 14-Oct-2013.) |
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) & ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) & ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) & ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) & ⊢ 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = 〈𝑎, 𝑏〉 ∧ 𝑞 = 〈𝑐, 𝑑〉 ∧ 𝜑)} ⇒ ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (〈𝐴, 𝐵〉𝑅〈𝐶, 𝐷〉 ↔ 𝜏)) | ||
Theorem | dfres3 30902 | Alternate definition of restriction. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝐴 ↾ 𝐵) = (𝐴 ∩ (𝐵 × ran 𝐴)) | ||
Theorem | cnvco1 30903 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ ◡(◡𝐴 ∘ 𝐵) = (◡𝐵 ∘ 𝐴) | ||
Theorem | cnvco2 30904 | Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014.) |
⊢ ◡(𝐴 ∘ ◡𝐵) = (𝐵 ∘ ◡𝐴) | ||
Theorem | eldm3 30905 | Quantifier-free definition of membership in a domain. (Contributed by Scott Fenton, 21-Jan-2017.) |
⊢ (𝐴 ∈ dom 𝐵 ↔ (𝐵 ↾ {𝐴}) ≠ ∅) | ||
Theorem | elrn3 30906 | Quantifier-free definition of membership in a range. (Contributed by Scott Fenton, 21-Jan-2017.) |
⊢ (𝐴 ∈ ran 𝐵 ↔ (𝐵 ∩ (V × {𝐴})) ≠ ∅) | ||
Theorem | pocnv 30907 | The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 Po 𝐴 → ◡𝑅 Po 𝐴) | ||
Theorem | socnv 30908 | The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴) | ||
Theorem | funpsstri 30909 | A condition for subset trichotomy for functions. (Contributed by Scott Fenton, 19-Apr-2011.) |
⊢ ((Fun 𝐻 ∧ (𝐹 ⊆ 𝐻 ∧ 𝐺 ⊆ 𝐻) ∧ (dom 𝐹 ⊆ dom 𝐺 ∨ dom 𝐺 ⊆ dom 𝐹)) → (𝐹 ⊊ 𝐺 ∨ 𝐹 = 𝐺 ∨ 𝐺 ⊊ 𝐹)) | ||
Theorem | fundmpss 30910 | 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 30911 | 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 30912 | 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 30913 | The uniqueness condition of functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (Fun 𝐹 → ((𝐴𝐹𝐵 ∧ 𝐴𝐹𝐶) → 𝐵 = 𝐶)) | ||
Theorem | funbreq 30914 | An equality condition for functions. (Contributed by Scott Fenton, 18-Feb-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ ((Fun 𝐹 ∧ 𝐴𝐹𝐵) → (𝐴𝐹𝐶 ↔ 𝐵 = 𝐶)) | ||
Theorem | mpteq12d 30915 | An equality inference for the maps to notation. Compare mpteq12dv 4663. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝜑 & ⊢ (𝜑 → 𝐴 = 𝐶) & ⊢ (𝜑 → 𝐵 = 𝐷) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷)) | ||
Theorem | fprb 30916* | A condition for functionhood over a pair. (Contributed by Scott Fenton, 16-Sep-2013.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ≠ 𝐵 → (𝐹:{𝐴, 𝐵}⟶𝑅 ↔ ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑅 𝐹 = {〈𝐴, 𝑥〉, 〈𝐵, 𝑦〉})) | ||
Theorem | br1steq 30917 | Uniqueness condition for binary relationship over the 1st relationship. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉1st 𝐶 ↔ 𝐶 = 𝐴) | ||
Theorem | br2ndeq 30918 | Uniqueness condition for binary relationship over the 2nd relationship. (Contributed by Scott Fenton, 11-Apr-2014.) (Proof shortened by Mario Carneiro, 3-May-2015.) |
⊢ 𝐴 ∈ V & ⊢ 𝐵 ∈ V & ⊢ 𝐶 ∈ V ⇒ ⊢ (〈𝐴, 𝐵〉2nd 𝐶 ↔ 𝐶 = 𝐵) | ||
Theorem | br1steqg 30919 | Uniqueness condition for binary relationship over the 1st relationship. (Contributed by Scott Fenton, 2-Jul-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉1st 𝐶 ↔ 𝐶 = 𝐴)) | ||
Theorem | br2ndeqg 30920 | Uniqueness condition for binary relationship over the 2nd relationship. (Contributed by Scott Fenton, 2-Jul-2020.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉2nd 𝐶 ↔ 𝐶 = 𝐵)) | ||
Theorem | dfdm5 30921 | Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ dom 𝐴 = ((1st ↾ (V × V)) “ 𝐴) | ||
Theorem | dfrn5 30922 | Definition of range in terms of 2nd and image. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ran 𝐴 = ((2nd ↾ (V × V)) “ 𝐴) | ||
Theorem | opelco3 30923 | Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.) |
⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 ∘ 𝐷) ↔ 𝐵 ∈ (𝐶 “ (𝐷 “ {𝐴}))) | ||
Theorem | elima4 30924 | Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.) |
⊢ (𝐴 ∈ (𝑅 “ 𝐵) ↔ (𝑅 ∩ (𝐵 × {𝐴})) ≠ ∅) | ||
Theorem | fv1stcnv 30925 | The value of the converse of 1st restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = 〈𝑋, 𝑌〉) | ||
Theorem | fv2ndcnv 30926 | The value of the converse of 2nd restricted to a singleton. (Contributed by Scott Fenton, 2-Jul-2020.) |
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉) | ||
Theorem | setinds 30927* | Principle of E induction (set 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 30928* | E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) (Revised by Mario Carneiro, 11-Dec-2016.) |
⊢ Ⅎ𝑥𝜓 & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | setinds2 30929* | E induction schema, using implicit substitution. (Contributed by Scott Fenton, 10-Mar-2011.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) & ⊢ (∀𝑦 ∈ 𝑥 𝜓 → 𝜑) ⇒ ⊢ 𝜑 | ||
Theorem | elpotr 30930* | A class of transitive sets is partially ordered by E. (Contributed by Scott Fenton, 15-Oct-2010.) |
⊢ (∀𝑧 ∈ 𝐴 Tr 𝑧 → E Po 𝐴) | ||
Theorem | dford5reg 30931 | Given ax-reg 8380, an ordinal is a transitive class totally ordered by epsilon. (Contributed by Scott Fenton, 28-Jan-2011.) |
⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E Or 𝐴)) | ||
Theorem | dfon2lem1 30932 | Lemma for dfon2 30941. (Contributed by Scott Fenton, 28-Feb-2011.) |
⊢ Tr ∪ {𝑥 ∣ (𝜑 ∧ Tr 𝑥 ∧ 𝜓)} | ||
Theorem | dfon2lem2 30933* | Lemma for dfon2 30941. (Contributed by Scott Fenton, 28-Feb-2011.) |
⊢ ∪ {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ 𝜑 ∧ 𝜓)} ⊆ 𝐴 | ||
Theorem | dfon2lem3 30934* | Lemma for dfon2 30941. All sets satisfying the new definition are transitive and untangled. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ (𝐴 ∈ 𝑉 → (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (Tr 𝐴 ∧ ∀𝑧 ∈ 𝐴 ¬ 𝑧 ∈ 𝑧))) | ||
Theorem | dfon2lem4 30935* | Lemma for dfon2 30941. 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 30936* | Lemma for dfon2 30941. 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 30937* | Lemma for dfon2 30941. 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 30938* | Lemma for dfon2 30941. All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011.) |
⊢ 𝐴 ∈ V ⇒ ⊢ (∀𝑥((𝑥 ⊊ 𝐴 ∧ Tr 𝑥) → 𝑥 ∈ 𝐴) → (𝐵 ∈ 𝐴 → ∀𝑦((𝑦 ⊊ 𝐵 ∧ Tr 𝑦) → 𝑦 ∈ 𝐵))) | ||
Theorem | dfon2lem8 30939* | Lemma for dfon2 30941. 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 30940* | Lemma for dfon2 30941. A class of new ordinals is well-founded by E. (Contributed by Scott Fenton, 3-Mar-2011.) |
⊢ (∀𝑥 ∈ 𝐴 ∀𝑦((𝑦 ⊊ 𝑥 ∧ Tr 𝑦) → 𝑦 ∈ 𝑥) → E Fr 𝐴) | ||
Theorem | dfon2 30941* | 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 | domep 30942 | The domain of the epsilon relation is the universe. (Contributed by Scott Fenton, 27-Oct-2010.) |
⊢ dom E = V | ||
Theorem | rdgprc0 30943 | 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 30944 | 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 30945* | 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 30946* | Generalization of dfrdg2 30945 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 30947 | A version of ax-ext 2590 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → ((𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥) → (𝑥 ∈ 𝑤 → 𝑦 ∈ 𝑤))) | ||
Theorem | ax8dfeq 30948 | A version of ax-8 1979 for use with defined equality. (Contributed by Scott Fenton, 12-Dec-2010.) |
⊢ ∃𝑧((𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑦)) | ||
Theorem | axextdist 30949 | ax-ext 2590 with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)) | ||
Theorem | axext4dist 30950 | axext4 2594 with distinctors instead of distinct variable restrictions. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦) → (𝑥 = 𝑦 ↔ ∀𝑧(𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))) | ||
Theorem | 19.12b 30951* | Version of 19.12vv 2168 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 30952 | There is always a set not in 𝑦. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ∃𝑥 ¬ 𝑥 ∈ 𝑦 | ||
Theorem | distel 30953 | Distinctors in terms of membership. (NOTE: this only works with relations where we can prove el 4773 and elirrv 8387.) (Contributed by Scott Fenton, 15-Dec-2010.) |
⊢ (¬ ∀𝑦 𝑦 = 𝑥 ↔ ¬ ∀𝑦 ¬ 𝑥 ∈ 𝑦) | ||
Theorem | axextndbi 30954 | axextnd 9292 as a biconditional. (Contributed by Scott Fenton, 14-Dec-2010.) |
⊢ ∃𝑧(𝑥 = 𝑦 ↔ (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦)) | ||
Theorem | hbntg 30955 | A more general form of hbnt 2129. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (∀𝑥(𝜑 → ∀𝑥𝜓) → (¬ 𝜓 → ∀𝑥 ¬ 𝜑)) | ||
Theorem | hbimtg 30956 | A more general and closed form of hbim 2112. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ ((∀𝑥(𝜑 → ∀𝑥𝜒) ∧ (𝜓 → ∀𝑥𝜃)) → ((𝜒 → 𝜓) → ∀𝑥(𝜑 → 𝜃))) | ||
Theorem | hbaltg 30957 | A more general and closed form of hbal 2023. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (∀𝑥(𝜑 → ∀𝑦𝜓) → (∀𝑥𝜑 → ∀𝑦∀𝑥𝜓)) | ||
Theorem | hbng 30958 | A more general form of hbn 2131. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (𝜑 → ∀𝑥𝜓) ⇒ ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜑) | ||
Theorem | hbimg 30959 | A more general form of hbim 2112. (Contributed by Scott Fenton, 13-Dec-2010.) |
⊢ (𝜑 → ∀𝑥𝜓) & ⊢ (𝜒 → ∀𝑥𝜃) ⇒ ⊢ ((𝜓 → 𝜒) → ∀𝑥(𝜑 → 𝜃)) | ||
Theorem | tfisg 30960* | A closed form of tfis 6946. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ (∀𝑥 ∈ On (∀𝑦 ∈ 𝑥 [𝑦 / 𝑥]𝜑 → 𝜑) → ∀𝑥 ∈ On 𝜑) | ||
Syntax | ctrpred 30961 | Define the transitive predecessor class as a class. |
class TrPred(𝑅, 𝐴, 𝑋) | ||
Definition | df-trpred 30962* | 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 30974 and trpredmintr 30975). 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 (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 30963* | 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 30964 | Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑅 = 𝑆 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑆, 𝐴, 𝑋)) | ||
Theorem | trpredeq2 30965 | Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝐴 = 𝐵 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐵, 𝑋)) | ||
Theorem | trpredeq3 30966 | Equality theorem for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝑋 = 𝑌 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐴, 𝑌)) | ||
Theorem | trpredeq1d 30967 | Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝜑 → 𝑅 = 𝑆) ⇒ ⊢ (𝜑 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑆, 𝐴, 𝑋)) | ||
Theorem | trpredeq2d 30968 | Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐵, 𝑋)) | ||
Theorem | trpredeq3d 30969 | Equality deduction for transitive predecessors. (Contributed by Scott Fenton, 2-Feb-2011.) |
⊢ (𝜑 → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → TrPred(𝑅, 𝐴, 𝑋) = TrPred(𝑅, 𝐴, 𝑌)) | ||
Theorem | eltrpred 30970* | 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 30972 and trpredmintr 30975. (Contributed by Scott Fenton, 28-Apr-2012.) |
⊢ (𝑌 ∈ TrPred(𝑅, 𝐴, 𝑋) ↔ ∃𝑖 ∈ ω 𝑌 ∈ ((rec((𝑎 ∈ V ↦ ∪ 𝑦 ∈ 𝑎 Pred(𝑅, 𝐴, 𝑦)), Pred(𝑅, 𝐴, 𝑋)) ↾ ω)‘𝑖)) | ||
Theorem | trpredlem1 30971* | 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 30972 | 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 30973 | The transitive predecessors form a subset of the base class. (Contributed by Scott Fenton, 20-Feb-2011.) |
⊢ (Pred(𝑅, 𝐴, 𝑋) ∈ 𝐵 → TrPred(𝑅, 𝐴, 𝑋) ⊆ 𝐴) | ||
Theorem | trpredtr 30974 | 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 30975* | 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 30976 | 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 30977* | 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 30978* | 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 30979 | 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 30980 | The class of transitive predecessors is empty when 𝐴 is empty. (Contributed by Scott Fenton, 30-Apr-2012.) |
⊢ TrPred(𝑅, ∅, 𝑋) = ∅ | ||
Theorem | trpredex 30981 | 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 30982* | 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 | frmin 30983* | 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 5628 and tz7.5 5661. (Contributed by Scott Fenton, 4-Feb-2011.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐵 ⊆ 𝐴 ∧ 𝐵 ≠ ∅)) → ∃𝑦 ∈ 𝐵 Pred(𝑅, 𝐵, 𝑦) = ∅) | ||
Theorem | frind 30984* | The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 30983). 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 5630 and tfi 6945, 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 30985* | The principle of founded induction. Theorem 4.4 of Don Monk's notes (see frmin 30983). 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 30986* | 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 30987* | 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 30988* | 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 30989* | 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 30990* | 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 30991* | 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 30992* | 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 30993* | Lemma for poseq 30994 and soseq 30995. The function value of a sequene is either in 𝐴 or null. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} ⇒ ⊢ (𝐺 ∈ 𝐹 → (𝐺‘𝑋) ∈ (𝐴 ∪ {∅})) | ||
Theorem | poseq 30994* | A partial ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝑅 Po (𝐴 ∪ {∅}) & ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} & ⊢ 𝑆 = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))} ⇒ ⊢ 𝑆 Po 𝐹 | ||
Theorem | soseq 30995* | A linear ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.) |
⊢ 𝑅 Or (𝐴 ∪ {∅}) & ⊢ 𝐹 = {𝑓 ∣ ∃𝑥 ∈ On 𝑓:𝑥⟶𝐴} & ⊢ 𝑆 = {〈𝑓, 𝑔〉 ∣ ((𝑓 ∈ 𝐹 ∧ 𝑔 ∈ 𝐹) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥)𝑅(𝑔‘𝑥)))} & ⊢ ¬ ∅ ∈ 𝐴 ⇒ ⊢ 𝑆 Or 𝐹 | ||
Syntax | cwsuc 30996 | Declare the syntax for well-founded successor. |
class wsuc(𝑅, 𝐴, 𝑋) | ||
Syntax | cwsucOLD 30997 | Declare the syntax for well-founded successor. (New usage is discouraged.) |
class wsucOLD(𝑅, 𝐴, 𝑋) | ||
Syntax | cwlim 30998 | Declare the syntax for well-founded limit class. |
class WLim(𝑅, 𝐴) | ||
Syntax | cwlimOLD 30999 | Declare the syntax for well-founded limit class. (New usage is discouraged.) |
class WLimOLD(𝑅, 𝐴) | ||
Definition | df-wsuc 31000 | 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(◡𝑅, 𝐴, 𝑋), 𝐴, 𝑅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |