![]() |
Metamath
Proof Explorer Theorem List (p. 83 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mpoxopynvov0g 8201* | 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 | mpoxopxnop0 8202* | If 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, is not an ordered pair, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (¬ 𝑉 ∈ (V × V) → (𝑉𝐹𝐾) = ∅) | ||
Theorem | mpoxopx0ov0 8203* | If 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, is the empty set, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017.) |
⊢ 𝐹 = (𝑥 ∈ V, 𝑦 ∈ (1st ‘𝑥) ↦ 𝐶) ⇒ ⊢ (∅𝐹𝐾) = ∅ | ||
Theorem | mpoxopxprcov0 8204* | 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 8205* | 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 8206* | 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 8207* | 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 8208* | 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 8209* | 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 8210* | 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 8211* | 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 8212 | The transposition of a function. |
class tpos 𝐹 | ||
Definition | df-tpos 8213* | Define the transposition of a function, which is a function 𝐺 = tpos 𝐹 satisfying 𝐺(𝑥, 𝑦) = 𝐹(𝑦, 𝑥). (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) | ||
Theorem | tposss 8214 | Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺) | ||
Theorem | tposeq 8215 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺) | ||
Theorem | tposeqd 8216 | Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → tpos 𝐹 = tpos 𝐺) | ||
Theorem | tposssxp 8217 | The transposition is a subset of a Cartesian product. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ tpos 𝐹 ⊆ ((◡dom 𝐹 ∪ {∅}) × ran 𝐹) | ||
Theorem | reltpos 8218 | The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ Rel tpos 𝐹 | ||
Theorem | brtpos2 8219 | Value of the transposition at an ordered pair ⟨𝐴, 𝐵⟩. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴tpos 𝐹𝐵 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵))) | ||
Theorem | brtpos0 8220 | 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 8222. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ ∅𝐹𝐴)) | ||
Theorem | reldmtpos 8221 | Necessary and sufficient condition for dom tpos 𝐹 to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹) | ||
Theorem | brtpos 8222 | The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐶 ∈ 𝑉 → (⟨𝐴, 𝐵⟩tpos 𝐹𝐶 ↔ ⟨𝐵, 𝐴⟩𝐹𝐶)) | ||
Theorem | ottpos 8223 | The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ (𝐶 ∈ 𝑉 → (⟨𝐴, 𝐵, 𝐶⟩ ∈ tpos 𝐹 ↔ ⟨𝐵, 𝐴, 𝐶⟩ ∈ 𝐹)) | ||
Theorem | relbrtpos 8224 | The transposition swaps arguments of a three-parameter relation. (Contributed by Mario Carneiro, 3-Nov-2015.) |
⊢ (Rel 𝐹 → (⟨𝐴, 𝐵⟩tpos 𝐹𝐶 ↔ ⟨𝐵, 𝐴⟩𝐹𝐶)) | ||
Theorem | dmtpos 8225 | The domain of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → dom tpos 𝐹 = ◡dom 𝐹) | ||
Theorem | rntpos 8226 | The range of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹) | ||
Theorem | tposexg 8227 | The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V) | ||
Theorem | ovtpos 8228 | 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 8229 | The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Fun 𝐹 → Fun tpos 𝐹) | ||
Theorem | dftpos2 8230* | Alternate definition of tpos when 𝐹 has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}))) | ||
Theorem | dftpos3 8231* | Alternate definition of tpos when 𝐹 has relational domain. Compare df-cnv 5684. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → tpos 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ⟨𝑦, 𝑥⟩𝐹𝑧}) | ||
Theorem | dftpos4 8232* | Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) | ||
Theorem | tpostpos 8233 | Value of the double transposition for a general class 𝐹. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V)) | ||
Theorem | tpostpos2 8234 | Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ ((Rel 𝐹 ∧ Rel dom 𝐹) → tpos tpos 𝐹 = 𝐹) | ||
Theorem | tposfn2 8235 | The domain of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹 Fn 𝐴 → tpos 𝐹 Fn ◡𝐴)) | ||
Theorem | tposfo2 8236 | Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–onto→𝐵 → tpos 𝐹:◡𝐴–onto→𝐵)) | ||
Theorem | tposf2 8237 | The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴⟶𝐵 → tpos 𝐹:◡𝐴⟶𝐵)) | ||
Theorem | tposf12 8238 | Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1→𝐵 → tpos 𝐹:◡𝐴–1-1→𝐵)) | ||
Theorem | tposf1o2 8239 | Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 → tpos 𝐹:◡𝐴–1-1-onto→𝐵)) | ||
Theorem | tposfo 8240 | The domain and codomain/range of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 → tpos 𝐹:(𝐵 × 𝐴)–onto→𝐶) | ||
Theorem | tposf 8241 | The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → tpos 𝐹:(𝐵 × 𝐴)⟶𝐶) | ||
Theorem | tposfn 8242 | Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝐹 Fn (𝐴 × 𝐵) → tpos 𝐹 Fn (𝐵 × 𝐴)) | ||
Theorem | tpos0 8243 | Transposition of the empty set. (Contributed by NM, 10-Sep-2015.) |
⊢ tpos ∅ = ∅ | ||
Theorem | tposco 8244 | Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ tpos (𝐹 ∘ 𝐺) = (𝐹 ∘ tpos 𝐺) | ||
Theorem | tpossym 8245* | Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝐹 Fn (𝐴 × 𝐴) → (tpos 𝐹 = 𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝐹𝑦) = (𝑦𝐹𝑥))) | ||
Theorem | tposeqi 8246 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = 𝐺 ⇒ ⊢ tpos 𝐹 = tpos 𝐺 | ||
Theorem | tposex 8247 | A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 ∈ V ⇒ ⊢ tpos 𝐹 ∈ V | ||
Theorem | nftpos 8248 | Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥tpos 𝐹 | ||
Theorem | tposoprab 8249* | Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ 𝜑} ⇒ ⊢ tpos 𝐹 = {⟨⟨𝑦, 𝑥⟩, 𝑧⟩ ∣ 𝜑} | ||
Theorem | tposmpo 8250* | Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ tpos 𝐹 = (𝑦 ∈ 𝐵, 𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | tposconst 8251 | The transposition of a constant operation using the relation representation. (Contributed by SO, 11-Jul-2018.) |
⊢ tpos ((𝐴 × 𝐵) × {𝐶}) = ((𝐵 × 𝐴) × {𝐶}) | ||
Syntax | ccur 8252 | Extend class notation to include the currying function. |
class curry 𝐴 | ||
Syntax | cunc 8253 | Extend class notation to include the uncurrying function. |
class uncurry 𝐴 | ||
Definition | df-cur 8254* | 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 8255* | 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 8256* | 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 8257* | 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 8258* | 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 8259 | Extend class notation with undefined value function. |
class Undef | ||
Definition | df-undef 8260 | Define the undefined value function, whose value at set 𝑠 is guaranteed not to be a member of 𝑠 (see pwuninel 8262). (Contributed by NM, 15-Sep-2011.) |
⊢ Undef = (𝑠 ∈ V ↦ 𝒫 ∪ 𝑠) | ||
Theorem | pwuninel2 8261 | Direct proof of pwuninel 8262 avoiding functions and thus several ZF axioms. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (∪ 𝐴 ∈ 𝑉 → ¬ 𝒫 ∪ 𝐴 ∈ 𝐴) | ||
Theorem | pwuninel 8262 | 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 8261. (Contributed by NM, 27-Jun-2008.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
⊢ ¬ 𝒫 ∪ 𝐴 ∈ 𝐴 | ||
Theorem | undefval 8263 | Value of the undefined value function. Normally we will not reference the explicit value but will use undefnel 8265 instead. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 24-Dec-2016.) |
⊢ (𝑆 ∈ 𝑉 → (Undef‘𝑆) = 𝒫 ∪ 𝑆) | ||
Theorem | undefnel2 8264 | The undefined value generated from a set is not a member of the set. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝑆 ∈ 𝑉 → ¬ (Undef‘𝑆) ∈ 𝑆) | ||
Theorem | undefnel 8265 | The undefined value generated from a set is not a member of the set. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝑆 ∈ 𝑉 → (Undef‘𝑆) ∉ 𝑆) | ||
Theorem | undefne0 8266 | The undefined value generated from a set is not empty. (Contributed by NM, 3-Sep-2018.) |
⊢ (𝑆 ∈ 𝑉 → (Undef‘𝑆) ≠ ∅) | ||
Syntax | cfrecs 8267 | Declare the syntax for the well-founded recursion generator. See df-frecs 8268. |
class frecs(𝑅, 𝐴, 𝐹) | ||
Definition | df-frecs 8268* | This is the definition for the well-founded recursion generator. Similar to df-wrecs 8299 and df-recs 8373, 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 9635 has been introduced. (Contributed by Scott Fenton, 23-Dec-2021.) |
⊢ frecs(𝑅, 𝐴, 𝐹) = ∪ {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐹(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} | ||
Theorem | frecseq123 8269 | Equality theorem for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021.) |
⊢ ((𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝐹 = 𝐺) → frecs(𝑅, 𝐴, 𝐹) = frecs(𝑆, 𝐵, 𝐺)) | ||
Theorem | nffrecs 8270 | Bound-variable hypothesis builder for the well-founded recursion generator. (Contributed by Scott Fenton, 23-Dec-2021.) |
⊢ Ⅎ𝑥𝑅 & ⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥frecs(𝑅, 𝐴, 𝐹) | ||
Theorem | csbfrecsg 8271 | Move class substitution in and out of the well-founded recursive function generator. (Contributed by Scott Fenton, 18-Nov-2024.) |
⊢ (𝐴 ∈ 𝑉 → ⦋𝐴 / 𝑥⦌frecs(𝑅, 𝐷, 𝐹) = frecs(⦋𝐴 / 𝑥⦌𝑅, ⦋𝐴 / 𝑥⦌𝐷, ⦋𝐴 / 𝑥⦌𝐹)) | ||
Theorem | fpr3g 8272* | Functions defined by well-founded recursion over a partial order are identical up to relation, domain, and characteristic function. This version of frr3g 9753 does not require infinity. (Contributed by Scott Fenton, 24-Aug-2022.) |
⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐹 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) = (𝑦𝐻(𝐹 ↾ Pred(𝑅, 𝐴, 𝑦)))) ∧ (𝐺 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝐺‘𝑦) = (𝑦𝐻(𝐺 ↾ Pred(𝑅, 𝐴, 𝑦))))) → 𝐹 = 𝐺) | ||
Theorem | frrlem1 8273* | 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 8274* | Lemma for well-founded recursion. An acceptable function is a function. (Contributed by Paul Chapman, 21-Apr-2012.) |
⊢ 𝐵 = {𝑓 ∣ ∃𝑥(𝑓 Fn 𝑥 ∧ (𝑥 ⊆ 𝐴 ∧ ∀𝑦 ∈ 𝑥 Pred(𝑅, 𝐴, 𝑦) ⊆ 𝑥) ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑦𝐺(𝑓 ↾ Pred(𝑅, 𝐴, 𝑦))))} ⇒ ⊢ (𝑔 ∈ 𝐵 → Fun 𝑔) | ||
Theorem | frrlem3 8275* | 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 8276* | 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 8277* | 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 8278* | 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 8279* | 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 8280* | 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 8281* | 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 8282* | 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 8283* | 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 8284* | 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 8285* | 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 8286* | 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 8287* | 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 8288* | 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 8289 | Weak version of fpr2 8291 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 8290 | 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 8291 | 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 8292* | 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 8290 and fpr2 8291 is identical to 𝐹. (Contributed by Scott Fenton, 11-Sep-2023.) |
⊢ 𝐹 = frecs(𝑅, 𝐴, 𝐺) ⇒ ⊢ (((𝑅 Fr 𝐴 ∧ 𝑅 Po 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐻 Fn 𝐴 ∧ ∀𝑧 ∈ 𝐴 (𝐻‘𝑧) = (𝑧𝐺(𝐻 ↾ Pred(𝑅, 𝐴, 𝑧))))) → 𝐹 = 𝐻) | ||
Theorem | frrrel 8293 | 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 8294 | 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 8295 | 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 8296 | 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 8297 | 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 8298 | Declare syntax for the well-ordered recursive function generator. |
class wrecs(𝑅, 𝐴, 𝐹) | ||
Definition | df-wrecs 8299 | 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 8337, wfr2 8338, and wfr3 8339. (Contributed by Scott Fenton, 7-Jun-2018.) (Revised by BJ, 27-Oct-2024.) |
⊢ wrecs(𝑅, 𝐴, 𝐹) = frecs(𝑅, 𝐴, (𝐹 ∘ 2nd )) | ||
Theorem | dfwrecsOLD 8300* | 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(𝑅, 𝐴, 𝑦))))} |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |