Home | Intuitionistic Logic Explorer Theorem List (p. 63 of 138) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rbropapd 6201* | Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
⊢ (𝜑 → 𝑀 = {〈𝑓, 𝑝〉 ∣ (𝑓𝑊𝑝 ∧ 𝜓)}) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒)) ⇒ ⊢ (𝜑 → ((𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒)))) | ||
Theorem | rbropap 6202* | Properties of a pair in a restricted binary relation 𝑀 expressed as an ordered-pair class abstraction: 𝑀 is the binary relation 𝑊 restricted by the condition 𝜓. (Contributed by AV, 31-Jan-2021.) |
⊢ (𝜑 → 𝑀 = {〈𝑓, 𝑝〉 ∣ (𝑓𝑊𝑝 ∧ 𝜓)}) & ⊢ ((𝑓 = 𝐹 ∧ 𝑝 = 𝑃) → (𝜓 ↔ 𝜒)) ⇒ ⊢ ((𝜑 ∧ 𝐹 ∈ 𝑋 ∧ 𝑃 ∈ 𝑌) → (𝐹𝑀𝑃 ↔ (𝐹𝑊𝑃 ∧ 𝜒))) | ||
Syntax | ctpos 6203 | The transposition of a function. |
class tpos 𝐹 | ||
Definition | df-tpos 6204* | Define the transposition of a function, which is a function 𝐺 = tpos 𝐹 satisfying 𝐺(𝑥, 𝑦) = 𝐹(𝑦, 𝑥). (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ (◡dom 𝐹 ∪ {∅}) ↦ ∪ ◡{𝑥})) | ||
Theorem | tposss 6205 | Subset theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 ⊆ 𝐺 → tpos 𝐹 ⊆ tpos 𝐺) | ||
Theorem | tposeq 6206 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 = 𝐺 → tpos 𝐹 = tpos 𝐺) | ||
Theorem | tposeqd 6207 | Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.) |
⊢ (𝜑 → 𝐹 = 𝐺) ⇒ ⊢ (𝜑 → tpos 𝐹 = tpos 𝐺) | ||
Theorem | tposssxp 6208 | The transposition is a subset of a cross product. (Contributed by Mario Carneiro, 12-Jan-2017.) |
⊢ tpos 𝐹 ⊆ ((◡dom 𝐹 ∪ {∅}) × ran 𝐹) | ||
Theorem | reltpos 6209 | The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ Rel tpos 𝐹 | ||
Theorem | brtpos2 6210 | Value of the transposition at a pair 〈𝐴, 𝐵〉. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐵 ∈ 𝑉 → (𝐴tpos 𝐹𝐵 ↔ (𝐴 ∈ (◡dom 𝐹 ∪ {∅}) ∧ ∪ ◡{𝐴}𝐹𝐵))) | ||
Theorem | brtpos0 6211 | 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). (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐴 ∈ 𝑉 → (∅tpos 𝐹𝐴 ↔ ∅𝐹𝐴)) | ||
Theorem | reldmtpos 6212 | Necessary and sufficient condition for dom tpos 𝐹 to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹) | ||
Theorem | brtposg 6213 | The transposition swaps arguments of a three-parameter relation. (Contributed by Jim Kingdon, 31-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) | ||
Theorem | ottposg 6214 | The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵, 𝐶〉 ∈ tpos 𝐹 ↔ 〈𝐵, 𝐴, 𝐶〉 ∈ 𝐹)) | ||
Theorem | dmtpos 6215 | The domain of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → dom tpos 𝐹 = ◡dom 𝐹) | ||
Theorem | rntpos 6216 | The range of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹) | ||
Theorem | tposexg 6217 | The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V) | ||
Theorem | ovtposg 6218 | The transposition swaps the arguments in a two-argument function. When 𝐹 is a matrix, which is to say a function from ( 1 ... m ) × ( 1 ... n ) to the reals 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 6219 | The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Fun 𝐹 → Fun tpos 𝐹) | ||
Theorem | dftpos2 6220* | Alternate definition of tpos when 𝐹 has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}))) | ||
Theorem | dftpos3 6221* | Alternate definition of tpos when 𝐹 has relational domain. Compare df-cnv 4606. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → tpos 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 〈𝑦, 𝑥〉𝐹𝑧}) | ||
Theorem | dftpos4 6222* | Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) | ||
Theorem | tpostpos 6223 | Value of the double transposition for a general class 𝐹. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V)) | ||
Theorem | tpostpos2 6224 | Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ ((Rel 𝐹 ∧ Rel dom 𝐹) → tpos tpos 𝐹 = 𝐹) | ||
Theorem | tposfn2 6225 | The domain of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹 Fn 𝐴 → tpos 𝐹 Fn ◡𝐴)) | ||
Theorem | tposfo2 6226 | Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–onto→𝐵 → tpos 𝐹:◡𝐴–onto→𝐵)) | ||
Theorem | tposf2 6227 | The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴⟶𝐵 → tpos 𝐹:◡𝐴⟶𝐵)) | ||
Theorem | tposf12 6228 | Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1→𝐵 → tpos 𝐹:◡𝐴–1-1→𝐵)) | ||
Theorem | tposf1o2 6229 | Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 → tpos 𝐹:◡𝐴–1-1-onto→𝐵)) | ||
Theorem | tposfo 6230 | The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 → tpos 𝐹:(𝐵 × 𝐴)–onto→𝐶) | ||
Theorem | tposf 6231 | The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → tpos 𝐹:(𝐵 × 𝐴)⟶𝐶) | ||
Theorem | tposfn 6232 | Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝐹 Fn (𝐴 × 𝐵) → tpos 𝐹 Fn (𝐵 × 𝐴)) | ||
Theorem | tpos0 6233 | Transposition of the empty set. (Contributed by NM, 10-Sep-2015.) |
⊢ tpos ∅ = ∅ | ||
Theorem | tposco 6234 | Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ tpos (𝐹 ∘ 𝐺) = (𝐹 ∘ tpos 𝐺) | ||
Theorem | tpossym 6235* | Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝐹 Fn (𝐴 × 𝐴) → (tpos 𝐹 = 𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝐹𝑦) = (𝑦𝐹𝑥))) | ||
Theorem | tposeqi 6236 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = 𝐺 ⇒ ⊢ tpos 𝐹 = tpos 𝐺 | ||
Theorem | tposex 6237 | A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 ∈ V ⇒ ⊢ tpos 𝐹 ∈ V | ||
Theorem | nftpos 6238 | Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥tpos 𝐹 | ||
Theorem | tposoprab 6239* | Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ tpos 𝐹 = {〈〈𝑦, 𝑥〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | tposmpo 6240* | Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ tpos 𝐹 = (𝑦 ∈ 𝐵, 𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | pwuninel2 6241 | 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. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
⊢ (∪ 𝐴 ∈ 𝑉 → ¬ 𝒫 ∪ 𝐴 ∈ 𝐴) | ||
Theorem | 2pwuninelg 6242 | The power set of 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. (Contributed by Jim Kingdon, 14-Jan-2020.) |
⊢ (𝐴 ∈ 𝑉 → ¬ 𝒫 𝒫 ∪ 𝐴 ∈ 𝐴) | ||
Theorem | iunon 6243* | The indexed union of a set of ordinal numbers 𝐵(𝑥) is an ordinal number. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 5-Dec-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ On) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ On) | ||
Syntax | wsmo 6244 | Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals. |
wff Smo 𝐴 | ||
Definition | df-smo 6245* | Definition of a strictly monotone ordinal function. Definition 7.46 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 15-Nov-2011.) |
⊢ (Smo 𝐴 ↔ (𝐴:dom 𝐴⟶On ∧ Ord dom 𝐴 ∧ ∀𝑥 ∈ dom 𝐴∀𝑦 ∈ dom 𝐴(𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦)))) | ||
Theorem | dfsmo2 6246* | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.) |
⊢ (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) | ||
Theorem | issmo 6247* | Conditions for which 𝐴 is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.) |
⊢ 𝐴:𝐵⟶On & ⊢ Ord 𝐵 & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) & ⊢ dom 𝐴 = 𝐵 ⇒ ⊢ Smo 𝐴 | ||
Theorem | issmo2 6248* | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ (𝐹:𝐴⟶𝐵 → ((𝐵 ⊆ On ∧ Ord 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) → Smo 𝐹)) | ||
Theorem | smoeq 6249 | Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ (𝐴 = 𝐵 → (Smo 𝐴 ↔ Smo 𝐵)) | ||
Theorem | smodm 6250 | The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ (Smo 𝐴 → Ord dom 𝐴) | ||
Theorem | smores 6251 | A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 16-Nov-2011.) (Proof shortened by Mario Carneiro, 5-Dec-2016.) |
⊢ ((Smo 𝐴 ∧ 𝐵 ∈ dom 𝐴) → Smo (𝐴 ↾ 𝐵)) | ||
Theorem | smores3 6252 | A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.) |
⊢ ((Smo (𝐴 ↾ 𝐵) ∧ 𝐶 ∈ (dom 𝐴 ∩ 𝐵) ∧ Ord 𝐵) → Smo (𝐴 ↾ 𝐶)) | ||
Theorem | smores2 6253 | A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.) |
⊢ ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴)) | ||
Theorem | smodm2 6254 | The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → Ord 𝐴) | ||
Theorem | smofvon2dm 6255 | The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ ((Smo 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐹‘𝐵) ∈ On) | ||
Theorem | iordsmo 6256 | The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ Ord 𝐴 ⇒ ⊢ Smo ( I ↾ 𝐴) | ||
Theorem | smo0 6257 | The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.) |
⊢ Smo ∅ | ||
Theorem | smofvon 6258 | If 𝐵 is a strictly monotone ordinal function, and 𝐴 is in the domain of 𝐵, then the value of the function at 𝐴 is an ordinal. (Contributed by Andrew Salmon, 20-Nov-2011.) |
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵) → (𝐵‘𝐴) ∈ On) | ||
Theorem | smoel 6259 | If 𝑥 is less than 𝑦 then a strictly monotone function's value will be strictly less at 𝑥 than at 𝑦. (Contributed by Andrew Salmon, 22-Nov-2011.) |
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐵‘𝐶) ∈ (𝐵‘𝐴)) | ||
Theorem | smoiun 6260* | The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.) |
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵) → ∪ 𝑥 ∈ 𝐴 (𝐵‘𝑥) ⊆ (𝐵‘𝐴)) | ||
Theorem | smoiso 6261 | If 𝐹 is an isomorphism from an ordinal 𝐴 onto 𝐵, which is a subset of the ordinals, then 𝐹 is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.) |
⊢ ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On) → Smo 𝐹) | ||
Theorem | smoel2 6262 | A strictly monotone ordinal function preserves the epsilon relation. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)) → (𝐹‘𝐶) ∈ (𝐹‘𝐵)) | ||
Syntax | crecs 6263 | Notation for a function defined by strong transfinite recursion. |
class recs(𝐹) | ||
Definition | df-recs 6264* |
Define a function recs(𝐹) on On, the
class of ordinal
numbers, by transfinite recursion given a rule 𝐹 which sets the next
value given all values so far. See df-irdg 6329 for more details on why
this definition is desirable. Unlike df-irdg 6329 which restricts the
update rule to use only the previous value, this version allows the
update rule to use all previous values, which is why it is
described
as "strong", although it is actually more primitive. See tfri1d 6294 and
tfri2d 6295 for the primary contract of this definition.
(Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} | ||
Theorem | recseq 6265 | Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺)) | ||
Theorem | nfrecs 6266 | Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥recs(𝐹) | ||
Theorem | tfrlem1 6267* | A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by Mario Carneiro, 24-May-2019.) |
⊢ (𝜑 → 𝐴 ∈ On) & ⊢ (𝜑 → (Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹)) & ⊢ (𝜑 → (Fun 𝐺 ∧ 𝐴 ⊆ dom 𝐺)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐵‘(𝐹 ↾ 𝑥))) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) = (𝐵‘(𝐺 ↾ 𝑥))) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)) | ||
Theorem | tfrlem3ag 6268* | Lemma for transfinite recursion. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by Jim Kingdon, 5-Jul-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝐺 ∈ V → (𝐺 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝐺 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝐺‘𝑤) = (𝐹‘(𝐺 ↾ 𝑤))))) | ||
Theorem | tfrlem3a 6269* | Lemma for transfinite recursion. Let 𝐴 be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by NM, 9-Apr-1995.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐺 ∈ V ⇒ ⊢ (𝐺 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝐺 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝐺‘𝑤) = (𝐹‘(𝐺 ↾ 𝑤)))) | ||
Theorem | tfrlem3 6270* | Lemma for transfinite recursion. Let 𝐴 be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in 𝐴 for later use. (Contributed by NM, 9-Apr-1995.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))} | ||
Theorem | tfrlem3-2d 6271* | Lemma for transfinite recursion which changes a bound variable (Contributed by Jim Kingdon, 2-Jul-2019.) |
⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) ⇒ ⊢ (𝜑 → (Fun 𝐹 ∧ (𝐹‘𝑔) ∈ V)) | ||
Theorem | tfrlem4 6272* | Lemma for transfinite recursion. 𝐴 is the class of all "acceptable" functions, and 𝐹 is their union. First we show that an acceptable function is in fact a function. (Contributed by NM, 9-Apr-1995.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝑔 ∈ 𝐴 → Fun 𝑔) | ||
Theorem | tfrlem5 6273* | Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) | ||
Theorem | recsfval 6274* | Lemma for transfinite recursion. The definition recs is the union of all acceptable functions. (Contributed by Mario Carneiro, 9-May-2015.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ recs(𝐹) = ∪ 𝐴 | ||
Theorem | tfrlem6 6275* | Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994.) (Revised by Mario Carneiro, 9-May-2015.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ Rel recs(𝐹) | ||
Theorem | tfrlem7 6276* | Lemma for transfinite recursion. The union of all acceptable functions is a function. (Contributed by NM, 9-Aug-1994.) (Revised by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ Fun recs(𝐹) | ||
Theorem | tfrlem8 6277* | Lemma for transfinite recursion. The domain of recs is ordinal. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Alan Sare, 11-Mar-2008.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ Ord dom recs(𝐹) | ||
Theorem | tfrlem9 6278* | Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝐵 ∈ dom recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))) | ||
Theorem | tfrfun 6279 | Transfinite recursion produces a function. (Contributed by Jim Kingdon, 20-Aug-2021.) |
⊢ Fun recs(𝐹) | ||
Theorem | tfr2a 6280 | A weak version of transfinite recursion. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴))) | ||
Theorem | tfr0dm 6281 | Transfinite recursion is defined at the empty set. (Contributed by Jim Kingdon, 8-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ ((𝐺‘∅) ∈ 𝑉 → ∅ ∈ dom 𝐹) | ||
Theorem | tfr0 6282 | Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ ((𝐺‘∅) ∈ 𝑉 → (𝐹‘∅) = (𝐺‘∅)) | ||
Theorem | tfrlemisucfn 6283* | We can extend an acceptable function by one element to produce a function. Lemma for tfrlemi1 6291. (Contributed by Jim Kingdon, 2-Jul-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ (𝜑 → 𝑧 ∈ On) & ⊢ (𝜑 → 𝑔 Fn 𝑧) & ⊢ (𝜑 → 𝑔 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) Fn suc 𝑧) | ||
Theorem | tfrlemisucaccv 6284* | We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 6291. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ (𝜑 → 𝑧 ∈ On) & ⊢ (𝜑 → 𝑔 Fn 𝑧) & ⊢ (𝜑 → 𝑔 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ 𝐴) | ||
Theorem | tfrlemibacc 6285* | Each element of 𝐵 is an acceptable function. Lemma for tfrlemi1 6291. (Contributed by Jim Kingdon, 14-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))} & ⊢ (𝜑 → 𝑥 ∈ On) & ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | ||
Theorem | tfrlemibxssdm 6286* | The union of 𝐵 is defined on all ordinals. Lemma for tfrlemi1 6291. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))} & ⊢ (𝜑 → 𝑥 ∈ On) & ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → 𝑥 ⊆ dom ∪ 𝐵) | ||
Theorem | tfrlemibfn 6287* | The union of 𝐵 is a function defined on 𝑥. Lemma for tfrlemi1 6291. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))} & ⊢ (𝜑 → 𝑥 ∈ On) & ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → ∪ 𝐵 Fn 𝑥) | ||
Theorem | tfrlemibex 6288* | The set 𝐵 exists. Lemma for tfrlemi1 6291. (Contributed by Jim Kingdon, 17-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))} & ⊢ (𝜑 → 𝑥 ∈ On) & ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → 𝐵 ∈ V) | ||
Theorem | tfrlemiubacc 6289* | The union of 𝐵 satisfies the recursion rule (lemma for tfrlemi1 6291). (Contributed by Jim Kingdon, 22-Apr-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))} & ⊢ (𝜑 → 𝑥 ∈ On) & ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → ∀𝑢 ∈ 𝑥 (∪ 𝐵‘𝑢) = (𝐹‘(∪ 𝐵 ↾ 𝑢))) | ||
Theorem | tfrlemiex 6290* | Lemma for tfrlemi1 6291. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))} & ⊢ (𝜑 → 𝑥 ∈ On) & ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝑥 ∧ ∀𝑢 ∈ 𝑥 (𝑓‘𝑢) = (𝐹‘(𝑓 ↾ 𝑢)))) | ||
Theorem | tfrlemi1 6291* |
We can define an acceptable function on any ordinal.
As with many of the transfinite recursion theorems, we have a hypothesis that states that 𝐹 is a function and that it is defined for all ordinals. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ On) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐹‘(𝑔 ↾ 𝑢)))) | ||
Theorem | tfrlemi14d 6292* | The domain of recs is all ordinals (lemma for transfinite recursion). (Contributed by Jim Kingdon, 9-Jul-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) ⇒ ⊢ (𝜑 → dom recs(𝐹) = On) | ||
Theorem | tfrexlem 6293* | The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑉) → (recs(𝐹)‘𝐶) ∈ V) | ||
Theorem | tfri1d 6294* |
Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of
[TakeutiZaring] p. 47, with an
additional condition.
The condition is that 𝐺 is defined "everywhere", which is stated here as (𝐺‘𝑥) ∈ V. Alternately, ∀𝑥 ∈ On∀𝑓(𝑓 Fn 𝑥 → 𝑓 ∈ dom 𝐺) would suffice. Given a function 𝐺 satisfying that condition, we define a class 𝐴 of all "acceptable" functions. The final function we're interested in is the union 𝐹 = recs(𝐺) of them. 𝐹 is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of 𝐹. In this first part we show that 𝐹 is a function whose domain is all ordinal numbers. (Contributed by Jim Kingdon, 4-May-2019.) (Revised by Mario Carneiro, 24-May-2019.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → ∀𝑥(Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V)) ⇒ ⊢ (𝜑 → 𝐹 Fn On) | ||
Theorem | tfri2d 6295* | Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule 𝐺 ( as described at tfri1 6324). Here we show that the function 𝐹 has the property that for any function 𝐺 satisfying that condition, the "next" value of 𝐹 is 𝐺 recursively applied to all "previous" values of 𝐹. (Contributed by Jim Kingdon, 4-May-2019.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → ∀𝑥(Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V)) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ On) → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴))) | ||
Theorem | tfr1onlem3ag 6296* | Lemma for transfinite recursion. This lemma changes some bound variables in 𝐴 (version of tfrlem3ag 6268 but for tfr1on 6309 related lemmas). (Contributed by Jim Kingdon, 13-Mar-2022.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝐻 ∈ 𝑉 → (𝐻 ∈ 𝐴 ↔ ∃𝑧 ∈ 𝑋 (𝐻 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝐻‘𝑤) = (𝐺‘(𝐻 ↾ 𝑤))))) | ||
Theorem | tfr1onlem3 6297* | Lemma for transfinite recursion. This lemma changes some bound variables in 𝐴 (version of tfrlem3 6270 but for tfr1on 6309 related lemmas). (Contributed by Jim Kingdon, 14-Mar-2022.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ 𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))} | ||
Theorem | tfr1onlemssrecs 6298* | Lemma for tfr1on 6309. The union of functions acceptable for tfr1on 6309 is a subset of recs. (Contributed by Jim Kingdon, 15-Mar-2022.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → Ord 𝑋) ⇒ ⊢ (𝜑 → ∪ 𝐴 ⊆ recs(𝐺)) | ||
Theorem | tfr1onlemsucfn 6299* | We can extend an acceptable function by one element to produce a function. Lemma for tfr1on 6309. (Contributed by Jim Kingdon, 12-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → 𝑧 ∈ 𝑋) & ⊢ (𝜑 → 𝑔 Fn 𝑧) & ⊢ (𝜑 → 𝑔 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) Fn suc 𝑧) | ||
Theorem | tfr1onlemsucaccv 6300* | Lemma for tfr1on 6309. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 12-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → 𝑌 ∈ 𝑋) & ⊢ (𝜑 → 𝑧 ∈ 𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝑔 Fn 𝑧) & ⊢ (𝜑 → 𝑔 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |