![]() |
Metamath
Proof Explorer Theorem List (p. 83 of 479) | < 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: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mpoxopxprcov0 8201* | If the components of the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, are not sets, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (¬ (𝑉 ∈ V ∧ 𝑊 ∈ V) → (⟨𝑉, 𝑊⟩𝐹𝐾) = ∅) | ||
Theorem | mpoxopynvov0 8202* | If the second argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument is not element of the first component of the first argument, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (𝐾 ∉ 𝑉 → (⟨𝑉, 𝑊⟩𝐹𝐾) = ∅) | ||
Theorem | mpoxopoveq 8203* | Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑}) ⇒ ⊢ (((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) ∧ 𝐾 ∈ 𝑉) → (⟨𝑉, 𝑊⟩𝐹𝐾) = {𝑛 ∈ 𝑉 ∣ [⟨𝑉, 𝑊⟩ / 𝑥][𝐾 / 𝑦]𝜑}) | ||
Theorem | mpoxopovel 8204* | Element of the value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument. (Contributed by Alexander van der Vekens and Mario Carneiro, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑}) ⇒ ⊢ ((𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌) → (𝑁 ∈ (⟨𝑉, 𝑊⟩𝐹𝐾) ↔ (𝐾 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ∧ [⟨𝑉, 𝑊⟩ / 𝑥][𝐾 / 𝑦][𝑁 / 𝑛]𝜑))) | ||
Theorem | mpoxopoveqd 8205* | Value of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, deduction version. (Contributed by Alexander van der Vekens, 11-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ {𝑛 ∈ (1st ‘𝑥) ∣ 𝜑}) & ⊢ (𝜓 → (𝑉 ∈ 𝑋 ∧ 𝑊 ∈ 𝑌)) & ⊢ ((𝜓 ∧ ¬ 𝐾 ∈ 𝑉) → {𝑛 ∈ 𝑉 ∣ [⟨𝑉, 𝑊⟩ / 𝑥][𝐾 / 𝑦]𝜑} = ∅) ⇒ ⊢ (𝜓 → (⟨𝑉, 𝑊⟩𝐹𝐾) = {𝑛 ∈ 𝑉 ∣ [⟨𝑉, 𝑊⟩ / 𝑥][𝐾 / 𝑦]𝜑}) | ||
Theorem | brovex 8206* | A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ 𝐶) & ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → Rel (𝑉𝑂𝐸)) ⇒ ⊢ (𝐹(𝑉𝑂𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | ||
Theorem | brovmpoex 8207* | A binary relation of the value of an operation given by the maps-to notation. (Contributed by Alexander van der Vekens, 21-Oct-2017.) |
⊢ 𝑂 = (𝑥 ∈ V, 𝑦 ∈ V ↦ {⟨𝑧, 𝑤⟩ ∣ 𝜑}) ⇒ ⊢ (𝐹(𝑉𝑂𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) | ||
Theorem | sprmpod 8208* | The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) (Revised by AV, 20-Jun-2019.) |
⊢ 𝑀 = (𝑣 ∈ V, 𝑒 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝑣𝑅𝑒)𝑦 ∧ 𝜒)}) & ⊢ ((𝜑 ∧ 𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝜒 ↔ 𝜓)) & ⊢ (𝜑 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) & ⊢ (𝜑 → ∀𝑥∀𝑦(𝑥(𝑉𝑅𝐸)𝑦 → 𝜃)) & ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ 𝜃} ∈ V) ⇒ ⊢ (𝜑 → (𝑉𝑀𝐸) = {⟨𝑥, 𝑦⟩ ∣ (𝑥(𝑉𝑅𝐸)𝑦 ∧ 𝜓)}) | ||
Syntax | ctpos 8209 | The transposition of a function. |
class tpos 𝐹 | ||
Definition | df-tpos 8210* | Define the transposition of a function, which is a function 𝐺 = tpos 𝐹 satisfying 𝐺(𝑥, 𝑦) = 𝐹(𝑦, 𝑥). (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) | ||
Theorem | tposss 8211 | Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺) | ||
Theorem | tposeq 8212 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺) | ||
Theorem | tposeqd 8213 | Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → tpos 𝐹 = tpos 𝐺) | ||
Theorem | tposssxp 8214 | The transposition is a subset of a Cartesian product. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ tpos 𝐹 ⊆ ((◡dom 𝐹 ∪ {∅}) × ran 𝐹) | ||
Theorem | reltpos 8215 | The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ Rel tpos 𝐹 | ||
Theorem | brtpos2 8216 | Value of the transposition at an ordered pair ⟨𝐴, 𝐵⟩. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴tpos 𝐹𝐵 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵))) | ||
Theorem | brtpos0 8217 | The behavior of tpos when the left argument is the empty set (which is not an ordered pair but is the "default" value of an ordered pair when the arguments are proper classes). This allows to eliminate sethood hypotheses on 𝐴, 𝐵 in brtpos 8219. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ ∅𝐹𝐴)) | ||
Theorem | reldmtpos 8218 | Necessary and sufficient condition for dom tpos 𝐹 to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹) | ||
Theorem | brtpos 8219 | The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐶 ∈ 𝑉 → (⟨𝐴, 𝐵⟩tpos 𝐹𝐶 ↔ ⟨𝐵, 𝐴⟩𝐹𝐶)) | ||
Theorem | ottpos 8220 | The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ (𝐶 ∈ 𝑉 → (⟨𝐴, 𝐵, 𝐶⟩ ∈ tpos 𝐹 ↔ ⟨𝐵, 𝐴, 𝐶⟩ ∈ 𝐹)) | ||
Theorem | relbrtpos 8221 | The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ (Rel 𝐹 → (⟨𝐴, 𝐵⟩tpos 𝐹𝐶 ↔ ⟨𝐵, 𝐴⟩𝐹𝐶)) | ||
Theorem | dmtpos 8222 | The domain of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → dom tpos 𝐹 = ◡dom 𝐹) | ||
Theorem | rntpos 8223 | The range of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹) | ||
Theorem | tposexg 8224 | The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V) | ||
Theorem | ovtpos 8225 | The transposition swaps the arguments in a two-argument function. When 𝐹 is a matrix, which is to say a function from (1...𝑚) × (1...𝑛) to ℝ or some ring, tpos 𝐹 is the transposition of 𝐹, which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐴tpos 𝐹𝐵) = (𝐵𝐹𝐴) | ||
Theorem | tposfun 8226 | The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Fun 𝐹 → Fun tpos 𝐹) | ||
Theorem | dftpos2 8227* | Alternate definition of tpos when 𝐹 has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}))) | ||
Theorem | dftpos3 8228* | Alternate definition of tpos when 𝐹 has relational domain. Compare df-cnv 5684. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → tpos 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨𝑦, 𝑥⟩𝐹𝑧}) | ||
Theorem | dftpos4 8229* | Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) | ||
Theorem | tpostpos 8230 | Value of the double transposition for a general class 𝐹. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V)) | ||
Theorem | tpostpos2 8231 | Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ ((Rel 𝐹 ∧ Rel dom 𝐹) → tpos tpos 𝐹 = 𝐹) | ||
Theorem | tposfn2 8232 | The domain of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹 Fn 𝐴 → tpos 𝐹 Fn ◡𝐴)) | ||
Theorem | tposfo2 8233 | Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–onto→𝐵 → tpos 𝐹:◡𝐴–onto→𝐵)) | ||
Theorem | tposf2 8234 | The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴⟶𝐵 → tpos 𝐹:◡𝐴⟶𝐵)) | ||
Theorem | tposf12 8235 | Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1→𝐵 → tpos 𝐹:◡𝐴–1-1→𝐵)) | ||
Theorem | tposf1o2 8236 | Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 → tpos 𝐹:◡𝐴–1-1-onto→𝐵)) | ||
Theorem | tposfo 8237 | The domain and codomain/range of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 → tpos 𝐹:(𝐵 × 𝐴)–onto→𝐶) | ||
Theorem | tposf 8238 | The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → tpos 𝐹:(𝐵 × 𝐴)⟶𝐶) | ||
Theorem | tposfn 8239 | Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝐹 Fn (𝐴 × 𝐵) → tpos 𝐹 Fn (𝐵 × 𝐴)) | ||
Theorem | tpos0 8240 | Transposition of the empty set. (Contributed by NM, 10-Sep-2015.) |
⊢ tpos ∅ = ∅ | ||
Theorem | tposco 8241 | Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ tpos (𝐹 ∘ 𝐺) = (𝐹 ∘ tpos 𝐺) | ||
Theorem | tpossym 8242* | Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝐹 Fn (𝐴 × 𝐴) → (tpos 𝐹 = 𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝐹𝑦) = (𝑦𝐹𝑥))) | ||
Theorem | tposeqi 8243 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = 𝐺 ⇒ ⊢ tpos 𝐹 = tpos 𝐺 | ||
Theorem | tposex 8244 | A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 ∈ V ⇒ ⊢ tpos 𝐹 ∈ V | ||
Theorem | nftpos 8245 | Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥tpos 𝐹 | ||
Theorem | tposoprab 8246* | Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⇒ ⊢ tpos 𝐹 = {⟨⟨𝑦, 𝑥⟩, 𝑧⟩ ∣ 𝜑} | ||
Theorem | tposmpo 8247* | Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ tpos 𝐹 = (𝑦 ∈ 𝐵, 𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | tposconst 8248 | The transposition of a constant operation using the relation representation. (Contributed by SO, 11-Jul-2018.) |
⊢ tpos ((𝐴 × 𝐵) × {𝐶}) = ((𝐵 × 𝐴) × {𝐶}) | ||
Syntax | ccur 8249 | Extend class notation to include the currying function. |
class curry 𝐴 | ||
Syntax | cunc 8250 | Extend class notation to include the uncurrying function. |
class uncurry 𝐴 | ||
Definition | df-cur 8251* | Define the currying of 𝐹, which splits a function of two arguments into a function of the first argument, producing a function over the second argument. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ curry 𝐹 = (𝑥 ∈ dom dom 𝐹 ↦ {⟨𝑦, 𝑧⟩ ∣ ⟨𝑥, 𝑦⟩𝐹𝑧}) | ||
Definition | df-unc 8252* | Define the uncurrying of 𝐹, which takes a function producing functions, and transforms it into a two-argument function. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ uncurry 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝑦(𝐹‘𝑥)𝑧} | ||
Theorem | mpocurryd 8253* | The currying of an operation given in maps-to notation, splitting the operation (function of two arguments) into a function of the first argument, producing a function over the second argument. (Contributed by AV, 27-Oct-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ≠ ∅) ⇒ ⊢ (𝜑 → curry 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝑦 ∈ 𝑌 ↦ 𝐶))) | ||
Theorem | mpocurryvald 8254* | The value of a curried operation given in maps-to notation is a function over the second argument of the original operation. (Contributed by AV, 27-Oct-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ≠ ∅) & ⊢ (𝜑 → 𝑌 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → (curry 𝐹‘𝐴) = (𝑦 ∈ 𝑌 ↦ ⦋𝐴 / 𝑥⦌𝐶)) | ||
Theorem | fvmpocurryd 8255* | The value of the value of a curried operation given in maps-to notation is the operation value of the original operation. (Contributed by AV, 27-Oct-2019.) |
⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐶) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑊) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐵 ∈ 𝑌) ⇒ ⊢ (𝜑 → ((curry 𝐹‘𝐴)‘𝐵) = (𝐴𝐹𝐵)) | ||
Syntax | cund 8256 | Extend class notation with undefined value function. |
class Undef | ||
Definition | df-undef 8257 | Define the undefined value function, whose value at set 𝑠 is guaranteed not to be a member of 𝑠 (see pwuninel 8259). (Contributed by NM, 15-Sep-2011.) |
⊢ Undef = (𝑠 ∈ V ↦ 𝒫 ∪ 𝑠) | ||
Theorem | pwuninel2 8258 | Direct proof of pwuninel 8259 avoiding functions and thus several ZF axioms. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (∪ 𝐴 ∈ 𝑉 → ¬ 𝒫 ∪ 𝐴 ∈ 𝐴) | ||
Theorem | pwuninel 8259 | The power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. See also pwuninel2 8258. (Contributed by NM, 27-Jun-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ ¬ 𝒫 ∪ 𝐴 ∈ 𝐴 | ||
Theorem | undefval 8260 | Value of the undefined value function. Normally we will not reference the explicit value but will use undefnel 8262 instead. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝑆 ∈ 𝑉 → (Undef‘𝑆) = 𝒫 ∪ 𝑆) | ||
Theorem | undefnel2 8261 | The undefined value generated from a set is not a member of the set. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝑆 ∈ 𝑉 → ¬ (Undef‘𝑆) ∈ 𝑆) | ||
Theorem | undefnel 8262 | The undefined value generated from a set is not a member of the set. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝑆 ∈ 𝑉 → (Undef‘𝑆) ∉ 𝑆) | ||
Theorem | undefne0 8263 | The undefined value generated from a set is not empty. (Contributed by NM, 3-Sep-2018.) |
⊢ (𝑆 ∈ 𝑉 → (Undef‘𝑆) ≠ ∅) | ||
Syntax | cfrecs 8264 | Declare the syntax for the well-founded recursion generator. See df-frecs 8265. |
class frecs(𝑅, 𝐴, 𝐹) | ||
Definition | df-frecs 8265* | This is the definition for the well-founded recursion generator. Similar to df-wrecs 8296 and df-recs 8370, it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a well-founded set-like relationship for its properties, not a well-ordered relationship. This proof requires either a partial order or the axiom of infinity. We develop the theorems twice, once with a partial order and once without. The second development occurs later in the database, after ax-inf 9632 has been introduced. (Contributed by Scott Fenton, 23-Dec-2021.) |
⊢ frecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} | ||
Theorem | frecseq123 8266 | Equality theorem for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺) → frecs(𝑅, 𝐴, 𝐹) = frecs(𝑆, 𝐵, 𝐺)) | ||
Theorem | nffrecs 8267 | Bound-variable hypothesis builder for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥frecs(𝑅, 𝐴, 𝐹) | ||
Theorem | csbfrecsg 8268 | Move class substitution in and out of the well-founded recursive function generator. (Contributed by Scott Fenton, 18-Nov-2024.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌frecs(𝑅, 𝐷, 𝐹) = frecs(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝐹)) | ||
Theorem | fpr3g 8269* | Functions defined by well-founded recursion over a partial order are identical up to relation, domain, and characteristic function. This version of frr3g 9750 does not require infinity. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝑦𝐻(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) = (𝑦𝐻(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺) | ||
Theorem | frrlem1 8270* | Lemma for well-founded recursion. The final item we are interested in is the union of acceptable functions 𝐵. This lemma just changes bound variables for later use. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ 𝐵 = {𝑔 ∣ ∃𝑧(𝑔 Fn 𝑧 ∧ (𝑧 ⊆ 𝐴 ∧ ∀𝑤 ∈ 𝑧 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑧) ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝑤𝐺(𝑔 ↾ Pred(𝑅, 𝐴, 𝑤))))} | ||
Theorem | frrlem2 8271* | Lemma for well-founded recursion. An acceptable function is a function. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔) | ||
Theorem | frrlem3 8272* | Lemma for well-founded recursion. An acceptable function's domain is a subset of 𝐴. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → dom 𝑔 ⊆ 𝐴) | ||
Theorem | frrlem4 8273* | Lemma for well-founded recursion. Properties of the restriction of an acceptable function to the domain of another acceptable function. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ ((𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → ((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) Fn (dom 𝑔 ∩ dom ℎ) ∧ ∀𝑎 ∈ (dom 𝑔 ∩ dom ℎ)((𝑔 ↾ (dom 𝑔 ∩ dom ℎ))‘𝑎) = (𝑎𝐺((𝑔 ↾ (dom 𝑔 ∩ dom ℎ)) ↾ Pred(𝑅, (dom 𝑔 ∩ dom ℎ), 𝑎))))) | ||
Theorem | frrlem5 8274* | Lemma for well-founded recursion. State the well-founded recursion generator in terms of the acceptable functions. (Contributed by Scott Fenton, 27-Aug-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ 𝐹 = ∪ 𝐵 | ||
Theorem | frrlem6 8275* | Lemma for well-founded recursion. The well-founded recursion generator is a relation. (Contributed by Scott Fenton, 27-Aug-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Rel 𝐹 | ||
Theorem | frrlem7 8276* | Lemma for well-founded recursion. The well-founded recursion generator's domain is a subclass of 𝐴. (Contributed by Scott Fenton, 27-Aug-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | frrlem8 8277* | Lemma for well-founded recursion. dom 𝐹 is closed under predecessor classes. (Contributed by Scott Fenton, 6-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑧 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑧) ⊆ dom 𝐹) | ||
Theorem | frrlem9 8278* | Lemma for well-founded recursion. Show that the well-founded recursive generator produces a function. Hypothesis three will be eliminated using different induction rules depending on if we use partial orders or the axiom of infinity. (Contributed by Scott Fenton, 27-Aug-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) ⇒ ⊢ (𝜑 → Fun 𝐹) | ||
Theorem | frrlem10 8279* | Lemma for well-founded recursion. Under the compatibility hypothesis, compute the value of 𝐹 within its domain. (Contributed by Scott Fenton, 6-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) ⇒ ⊢ ((𝜑 ∧ 𝑦 ∈ dom 𝐹) → (𝐹‘𝑦) = (𝑦𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) | ||
Theorem | frrlem11 8280* | Lemma for well-founded recursion. For the next several theorems we will be aiming to prove that dom 𝐹 = 𝐴. To do this, we set up a function 𝐶 that supposedly contains an element of 𝐴 that is not in dom 𝐹 and we show that the element must be in dom 𝐹. Our choice of what to restrict 𝐹 to depends on if we assume partial orders or the axiom of infinity. To begin with, we establish the functionality of 𝐶. (Contributed by Scott Fenton, 7-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) & ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹)) → 𝐶 Fn ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) | ||
Theorem | frrlem12 8281* | Lemma for well-founded recursion. Next, we calculate the value of 𝐶. (Contributed by Scott Fenton, 7-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) & ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) & ⊢ (𝜑 → 𝑅 Fr 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ 𝑤 ∈ ((𝑆 ∩ dom 𝐹) ∪ {𝑧})) → (𝐶‘𝑤) = (𝑤𝐺(𝐶 ↾ Pred(𝑅, 𝐴, 𝑤)))) | ||
Theorem | frrlem13 8282* | Lemma for well-founded recursion. Assuming that 𝑆 is a subset of 𝐴 and that 𝑧 is 𝑅-minimal, then 𝐶 is an acceptable function. (Contributed by Scott Fenton, 7-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) & ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) & ⊢ (𝜑 → 𝑅 Fr 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ∈ V) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ⊆ 𝐴) ⇒ ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐴 ∖ dom 𝐹) ∧ Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅)) → 𝐶 ∈ 𝐵) | ||
Theorem | frrlem14 8283* | Lemma for well-founded recursion. Finally, we tie all these threads together and show that dom 𝐹 = 𝐴 when given the right 𝑆. Specifically, we prove that there can be no 𝑅-minimal element of (𝐴 ∖ dom 𝐹). (Contributed by Scott Fenton, 7-Dec-2022.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) & ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) & ⊢ 𝐶 = ((𝐹 ↾ 𝑆) ∪ {⟨𝑧, (𝑧𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑧)))⟩}) & ⊢ (𝜑 → 𝑅 Fr 𝐴) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → Pred(𝑅, 𝐴, 𝑧) ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ 𝑆 Pred(𝑅, 𝐴, 𝑤) ⊆ 𝑆) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ∈ V) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝐴) → 𝑆 ⊆ 𝐴) & ⊢ ((𝜑 ∧ (𝐴 ∖ dom 𝐹) ≠ ∅) → ∃𝑧 ∈ (𝐴 ∖ dom 𝐹)Pred(𝑅, (𝐴 ∖ dom 𝐹), 𝑧) = ∅) ⇒ ⊢ (𝜑 → dom 𝐹 = 𝐴) | ||
Theorem | fprlem1 8284* | Lemma for well-founded recursion with a partial order. Two acceptable functions are compatible. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} & ⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝑔 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
Theorem | fprlem2 8285* | Lemma for well-founded recursion with a partial order. Establish a subset relation. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑧 ∈ 𝐴) → ∀𝑤 ∈ Pred (𝑅, 𝐴, 𝑧)Pred(𝑅, 𝐴, 𝑤) ⊆ Pred(𝑅, 𝐴, 𝑧)) | ||
Theorem | fpr2a 8286 | Weak version of fpr2 8288 which is useful for proofs that avoid the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ dom 𝐹) → (𝐹‘𝑋) = (𝑋𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
Theorem | fpr1 8287 | Law of well-founded recursion over a partial order, part one. Establish the functionality and domain of the recursive function generator. Note that by requiring a partial order we can avoid using the axiom of infinity. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → 𝐹 Fn 𝐴) | ||
Theorem | fpr2 8288 | Law of well-founded recursion over a partial order, part two. Now we establish the value of 𝐹 within 𝐴. (Contributed by Scott Fenton, 11-Sep-2023.) (Proof shortened by Scott Fenton, 18-Nov-2024.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) = (𝑋𝐺(𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)))) | ||
Theorem | fpr3 8289* | Law of well-founded recursion over a partial order, part three. Finally, we show that 𝐹 is unique. We do this by showing that any function 𝐻 with the same properties we proved of 𝐹 in fpr1 8287 and fpr2 8288 is identical to 𝐹. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝑧𝐺(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝐹 = 𝐻) | ||
Theorem | frrrel 8290 | Show without using the axiom of replacement that the well-founded recursion generator gives a relation. (Contributed by Scott Fenton, 18-Nov-2024.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ Rel 𝐹 | ||
Theorem | frrdmss 8291 | Show without using the axiom of replacement that the domain of the well-founded recursion generator is a subclass of 𝐴. (Contributed by Scott Fenton, 18-Nov-2024.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ dom 𝐹 ⊆ 𝐴 | ||
Theorem | frrdmcl 8292 | Show without using the axiom of replacement that for a "function" defined by well-founded recursion, the predecessor class of an element of its domain is a subclass of its domain. (Contributed by Scott Fenton, 21-Apr-2011.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (𝑋 ∈ dom 𝐹 → Pred(𝑅, 𝐴, 𝑋) ⊆ dom 𝐹) | ||
Theorem | fprfung 8293 | A "function" defined by well-founded recursion is indeed a function when the relation is a partial order. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ ((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) → Fun 𝐹) | ||
Theorem | fprresex 8294 | The restriction of a function defined by well-founded recursion to the predecessor of an element of its domain is a set. Avoids the axiom of replacement. (Contributed by Scott Fenton, 18-Nov-2024.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ 𝑋 ∈ dom 𝐹) → (𝐹 ↾ Pred(𝑅, 𝐴, 𝑋)) ∈ V) | ||
Syntax | cwrecs 8295 | Declare syntax for the well-ordered recursive function generator. |
class wrecs(𝑅, 𝐴, 𝐹) | ||
Definition | df-wrecs 8296 | Define the well-ordered recursive function generator. This function takes the usual expressions from recursion theorems and forms a unified definition. Specifically, given a function 𝐹, a relation 𝑅, and a base set 𝐴, this definition generates a function 𝐺 = wrecs(𝑅, 𝐴, 𝐹) that has property that, at any point 𝑥 ∈ 𝐴, (𝐺‘𝑥) = (𝐹‘(𝐺 ↾ Pred(𝑅, 𝐴, 𝑥))). See wfr1 8334, wfr2 8335, and wfr3 8336. (Contributed by Scott Fenton, 7-Jun-2018.) (Revised by BJ, 27-Oct-2024.) |
⊢ wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd )) | ||
Theorem | dfwrecsOLD 8297* | Obsolete definition of the well-ordered recursive function generator as of 18-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 7-Jun-2018.) |
⊢ wrecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} | ||
Theorem | wrecseq123 8298 | General equality theorem for the well-ordered recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺) → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑆, 𝐵, 𝐺)) | ||
Theorem | wrecseq123OLD 8299 | Obsolete proof of wrecseq123 8298 as of 17-Nov-2024. (New usage is discouraged.) (Proof modification is discouraged.) (Contributed by Scott Fenton, 7-Jun-2018.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺) → wrecs(𝑅, 𝐴, 𝐹) = wrecs(𝑆, 𝐵, 𝐺)) | ||
Theorem | nfwrecs 8300 | Bound-variable hypothesis builder for the well-ordered recursive function generator. (Contributed by Scott Fenton, 9-Jun-2018.) (Proof shortened by Scott Fenton, 17-Nov-2024.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥wrecs(𝑅, 𝐴, 𝐹) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |