![]() |
Intuitionistic Logic Explorer Theorem List (p. 60 of 110) | < 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 | brtpos0 5901 | 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 5902 | Necessary and sufficient condition for dom tpos 𝐹 to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom tpos 𝐹 ↔ ¬ ∅ ∈ dom 𝐹) | ||
Theorem | brtposg 5903 | The transposition swaps arguments of a three-parameter relation. (Contributed by Jim Kingdon, 31-Jan-2019.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵〉tpos 𝐹𝐶 ↔ 〈𝐵, 𝐴〉𝐹𝐶)) | ||
Theorem | ottposg 5904 | The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋) → (〈𝐴, 𝐵, 𝐶〉 ∈ tpos 𝐹 ↔ 〈𝐵, 𝐴, 𝐶〉 ∈ 𝐹)) | ||
Theorem | dmtpos 5905 | The domain of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → dom tpos 𝐹 = ◡dom 𝐹) | ||
Theorem | rntpos 5906 | The range of tpos 𝐹 when dom 𝐹 is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → ran tpos 𝐹 = ran 𝐹) | ||
Theorem | tposexg 5907 | The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (𝐹 ∈ 𝑉 → tpos 𝐹 ∈ V) | ||
Theorem | ovtposg 5908 | 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 5909 | The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Fun 𝐹 → Fun tpos 𝐹) | ||
Theorem | dftpos2 5910* | Alternate definition of tpos when 𝐹 has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ◡dom 𝐹 ↦ ∪ ◡{𝑥}))) | ||
Theorem | dftpos3 5911* | Alternate definition of tpos when 𝐹 has relational domain. Compare df-cnv 4379. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ (Rel dom 𝐹 → tpos 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 〈𝑦, 𝑥〉𝐹𝑧}) | ||
Theorem | dftpos4 5912* | Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ tpos 𝐹 = (𝐹 ∘ (𝑥 ∈ ((V × V) ∪ {∅}) ↦ ∪ ◡{𝑥})) | ||
Theorem | tpostpos 5913 | Value of the double transposition for a general class 𝐹. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ tpos tpos 𝐹 = (𝐹 ∩ (((V × V) ∪ {∅}) × V)) | ||
Theorem | tpostpos2 5914 | Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.) |
⊢ ((Rel 𝐹 ∧ Rel dom 𝐹) → tpos tpos 𝐹 = 𝐹) | ||
Theorem | tposfn2 5915 | The domain of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹 Fn 𝐴 → tpos 𝐹 Fn ◡𝐴)) | ||
Theorem | tposfo2 5916 | Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–onto→𝐵 → tpos 𝐹:◡𝐴–onto→𝐵)) | ||
Theorem | tposf2 5917 | The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴⟶𝐵 → tpos 𝐹:◡𝐴⟶𝐵)) | ||
Theorem | tposf12 5918 | Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1→𝐵 → tpos 𝐹:◡𝐴–1-1→𝐵)) | ||
Theorem | tposf1o2 5919 | Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (Rel 𝐴 → (𝐹:𝐴–1-1-onto→𝐵 → tpos 𝐹:◡𝐴–1-1-onto→𝐵)) | ||
Theorem | tposfo 5920 | The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (𝐹:(𝐴 × 𝐵)–onto→𝐶 → tpos 𝐹:(𝐵 × 𝐴)–onto→𝐶) | ||
Theorem | tposf 5921 | The domain and range of a transposition. (Contributed by NM, 10-Sep-2015.) |
⊢ (𝐹:(𝐴 × 𝐵)⟶𝐶 → tpos 𝐹:(𝐵 × 𝐴)⟶𝐶) | ||
Theorem | tposfn 5922 | Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝐹 Fn (𝐴 × 𝐵) → tpos 𝐹 Fn (𝐵 × 𝐴)) | ||
Theorem | tpos0 5923 | Transposition of the empty set. (Contributed by NM, 10-Sep-2015.) |
⊢ tpos ∅ = ∅ | ||
Theorem | tposco 5924 | Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ tpos (𝐹 ∘ 𝐺) = (𝐹 ∘ tpos 𝐺) | ||
Theorem | tpossym 5925* | Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015.) |
⊢ (𝐹 Fn (𝐴 × 𝐴) → (tpos 𝐹 = 𝐹 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝐹𝑦) = (𝑦𝐹𝑥))) | ||
Theorem | tposeqi 5926 | Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = 𝐺 ⇒ ⊢ tpos 𝐹 = tpos 𝐺 | ||
Theorem | tposex 5927 | A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 ∈ V ⇒ ⊢ tpos 𝐹 ∈ V | ||
Theorem | nftpos 5928 | Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥tpos 𝐹 | ||
Theorem | tposoprab 5929* | Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = {〈〈𝑥, 𝑦〉, 𝑧〉 ∣ 𝜑} ⇒ ⊢ tpos 𝐹 = {〈〈𝑦, 𝑥〉, 𝑧〉 ∣ 𝜑} | ||
Theorem | tposmpt2 5930* | Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015.) |
⊢ 𝐹 = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) ⇒ ⊢ tpos 𝐹 = (𝑦 ∈ 𝐵, 𝑥 ∈ 𝐴 ↦ 𝐶) | ||
Theorem | pwuninel2 5931 | 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 5932 | 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 5933* | 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 5934 | Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals. |
wff Smo 𝐴 | ||
Definition | df-smo 5935* | 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 5936* | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.) |
⊢ (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥))) | ||
Theorem | issmo 5937* | Conditions for which 𝐴 is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.) |
⊢ 𝐴:𝐵⟶On & ⊢ Ord 𝐵 & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ∈ 𝑦 → (𝐴‘𝑥) ∈ (𝐴‘𝑦))) & ⊢ dom 𝐴 = 𝐵 ⇒ ⊢ Smo 𝐴 | ||
Theorem | issmo2 5938* | Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ (𝐹:𝐴⟶𝐵 → ((𝐵 ⊆ On ∧ Ord 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝑥 (𝐹‘𝑦) ∈ (𝐹‘𝑥)) → Smo 𝐹)) | ||
Theorem | smoeq 5939 | Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ (𝐴 = 𝐵 → (Smo 𝐴 ↔ Smo 𝐵)) | ||
Theorem | smodm 5940 | The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ (Smo 𝐴 → Ord dom 𝐴) | ||
Theorem | smores 5941 | 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 5942 | A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.) |
⊢ ((Smo (𝐴 ↾ 𝐵) ∧ 𝐶 ∈ (dom 𝐴 ∩ 𝐵) ∧ Ord 𝐵) → Smo (𝐴 ↾ 𝐶)) | ||
Theorem | smores2 5943 | A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.) |
⊢ ((Smo 𝐹 ∧ Ord 𝐴) → Smo (𝐹 ↾ 𝐴)) | ||
Theorem | smodm2 5944 | The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ ((𝐹 Fn 𝐴 ∧ Smo 𝐹) → Ord 𝐴) | ||
Theorem | smofvon2dm 5945 | The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ ((Smo 𝐹 ∧ 𝐵 ∈ dom 𝐹) → (𝐹‘𝐵) ∈ On) | ||
Theorem | iordsmo 5946 | The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.) |
⊢ Ord 𝐴 ⇒ ⊢ Smo ( I ↾ 𝐴) | ||
Theorem | smo0 5947 | The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.) |
⊢ Smo ∅ | ||
Theorem | smofvon 5948 | 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 5949 | 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 5950* | The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.) |
⊢ ((Smo 𝐵 ∧ 𝐴 ∈ dom 𝐵) → ∪ 𝑥 ∈ 𝐴 (𝐵‘𝑥) ⊆ (𝐵‘𝐴)) | ||
Theorem | smoiso 5951 | 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 5952 | A strictly monotone ordinal function preserves the epsilon relation. (Contributed by Mario Carneiro, 12-Mar-2013.) |
⊢ (((𝐹 Fn 𝐴 ∧ Smo 𝐹) ∧ (𝐵 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵)) → (𝐹‘𝐶) ∈ (𝐹‘𝐵)) | ||
Syntax | crecs 5953 | Notation for a function defined by strong transfinite recursion. |
class recs(𝐹) | ||
Definition | df-recs 5954* |
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 6019 for more details on why
this definition is desirable. Unlike df-irdg 6019 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 5984 and
tfri2d 5985 for the primary contract of this definition.
(Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ recs(𝐹) = ∪ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} | ||
Theorem | recseq 5955 | Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ (𝐹 = 𝐺 → recs(𝐹) = recs(𝐺)) | ||
Theorem | nfrecs 5956 | Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.) |
⊢ Ⅎ𝑥𝐹 ⇒ ⊢ Ⅎ𝑥recs(𝐹) | ||
Theorem | tfrlem1 5957* | 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 5958* | 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 5959* | 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 5960* | 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 5961* | Lemma for transfinite recursion which changes a bound variable (Contributed by Jim Kingdon, 2-Jul-2019.) |
⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) ⇒ ⊢ (𝜑 → (Fun 𝐹 ∧ (𝐹‘𝑔) ∈ V)) | ||
Theorem | tfrlem4 5962* | 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 5963* | 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 5964* | 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 5965* | 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 5966* | 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 5967* | 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 5968* | 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 5969 | Transfinite recursion produces a function. (Contributed by Jim Kingdon, 20-Aug-2021.) |
⊢ Fun recs(𝐹) | ||
Theorem | tfr2a 5970 | A weak version of transfinite recursion. (Contributed by Mario Carneiro, 24-Jun-2015.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ (𝐴 ∈ dom 𝐹 → (𝐹‘𝐴) = (𝐺‘(𝐹 ↾ 𝐴))) | ||
Theorem | tfr0dm 5971 | Transfinite recursion is defined at the empty set. (Contributed by Jim Kingdon, 8-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ ((𝐺‘∅) ∈ 𝑉 → ∅ ∈ dom 𝐹) | ||
Theorem | tfr0 5972 | Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.) |
⊢ 𝐹 = recs(𝐺) ⇒ ⊢ ((𝐺‘∅) ∈ 𝑉 → (𝐹‘∅) = (𝐺‘∅)) | ||
Theorem | tfrlemisucfn 5973* | We can extend an acceptable function by one element to produce a function. Lemma for tfrlemi1 5981. (Contributed by Jim Kingdon, 2-Jul-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ (𝜑 → 𝑧 ∈ On) & ⊢ (𝜑 → 𝑔 Fn 𝑧) & ⊢ (𝜑 → 𝑔 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) Fn suc 𝑧) | ||
Theorem | tfrlemisucaccv 5974* | We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 5981. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ (𝜑 → 𝑧 ∈ On) & ⊢ (𝜑 → 𝑔 Fn 𝑧) & ⊢ (𝜑 → 𝑔 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}) ∈ 𝐴) | ||
Theorem | tfrlemibacc 5975* | Each element of 𝐵 is an acceptable function. Lemma for tfrlemi1 5981. (Contributed by Jim Kingdon, 14-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))} & ⊢ (𝜑 → 𝑥 ∈ On) & ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | ||
Theorem | tfrlemibxssdm 5976* | The union of 𝐵 is defined on all ordinals. Lemma for tfrlemi1 5981. (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 5977* | The union of 𝐵 is a function defined on 𝑥. Lemma for tfrlemi1 5981. (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 5978* | The set 𝐵 exists. Lemma for tfrlemi1 5981. (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 5979* | The union of 𝐵 satisfies the recursion rule (lemma for tfrlemi1 5981). (Contributed by Jim Kingdon, 22-Apr-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → ∀𝑥(Fun 𝐹 ∧ (𝐹‘𝑥) ∈ V)) & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐹‘𝑔)〉}))} & ⊢ (𝜑 → 𝑥 ∈ On) & ⊢ (𝜑 → ∀𝑧 ∈ 𝑥 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐹‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → ∀𝑢 ∈ 𝑥 (∪ 𝐵‘𝑢) = (𝐹‘(∪ 𝐵 ↾ 𝑢))) | ||
Theorem | tfrlemiex 5980* | Lemma for tfrlemi1 5981. (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 5981* |
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 5982* | 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 5983* | 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 5984* |
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 5985* | 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 6014). 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 5986* | Lemma for transfinite recursion. This lemma changes some bound variables in 𝐴 (version of tfrlem3ag 5958 but for tfr1on 5999 related lemmas). (Contributed by Jim Kingdon, 13-Mar-2022.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ (𝐻 ∈ 𝑉 → (𝐻 ∈ 𝐴 ↔ ∃𝑧 ∈ 𝑋 (𝐻 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝐻‘𝑤) = (𝐺‘(𝐻 ↾ 𝑤))))) | ||
Theorem | tfr1onlem3 5987* | Lemma for transfinite recursion. This lemma changes some bound variables in 𝐴 (version of tfrlem3 5960 but for tfr1on 5999 related lemmas). (Contributed by Jim Kingdon, 14-Mar-2022.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} ⇒ ⊢ 𝐴 = {𝑔 ∣ ∃𝑧 ∈ 𝑋 (𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))} | ||
Theorem | tfr1onlemssrecs 5988* | Lemma for tfr1on 5999. The union of functions acceptable for tfr1on 5999 is a subset of recs. (Contributed by Jim Kingdon, 15-Mar-2022.) |
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → Ord 𝑋) ⇒ ⊢ (𝜑 → ∪ 𝐴 ⊆ recs(𝐺)) | ||
Theorem | tfr1onlemsucfn 5989* | We can extend an acceptable function by one element to produce a function. Lemma for tfr1on 5999. (Contributed by Jim Kingdon, 12-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ (𝜑 → 𝑧 ∈ 𝑋) & ⊢ (𝜑 → 𝑔 Fn 𝑧) & ⊢ (𝜑 → 𝑔 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) Fn suc 𝑧) | ||
Theorem | tfr1onlemsucaccv 5990* | Lemma for tfr1on 5999. 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 𝑧) & ⊢ (𝜑 → 𝑔 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}) ∈ 𝐴) | ||
Theorem | tfr1onlembacc 5991* | Lemma for tfr1on 5999. Each element of 𝐵 is an acceptable function. (Contributed by Jim Kingdon, 14-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | ||
Theorem | tfr1onlembxssdm 5992* | Lemma for tfr1on 5999. The union of 𝐵 is defined on all elements of 𝑋. (Contributed by Jim Kingdon, 14-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → 𝐷 ⊆ dom ∪ 𝐵) | ||
Theorem | tfr1onlembfn 5993* | Lemma for tfr1on 5999. The union of 𝐵 is a function defined on 𝑥. (Contributed by Jim Kingdon, 15-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → ∪ 𝐵 Fn 𝐷) | ||
Theorem | tfr1onlembex 5994* | Lemma for tfr1on 5999. The set 𝐵 exists. (Contributed by Jim Kingdon, 14-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → 𝐵 ∈ V) | ||
Theorem | tfr1onlemubacc 5995* | Lemma for tfr1on 5999. The union of 𝐵 satisfies the recursion rule. (Contributed by Jim Kingdon, 15-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → ∀𝑢 ∈ 𝐷 (∪ 𝐵‘𝑢) = (𝐺‘(∪ 𝐵 ↾ 𝑢))) | ||
Theorem | tfr1onlemex 5996* | Lemma for tfr1on 5999. (Contributed by Jim Kingdon, 16-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ 𝐵 = {ℎ ∣ ∃𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ 𝑔 ∈ 𝐴 ∧ ℎ = (𝑔 ∪ {〈𝑧, (𝐺‘𝑔)〉}))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝐷 ∈ 𝑋) & ⊢ (𝜑 → ∀𝑧 ∈ 𝐷 ∃𝑔(𝑔 Fn 𝑧 ∧ ∀𝑤 ∈ 𝑧 (𝑔‘𝑤) = (𝐺‘(𝑔 ↾ 𝑤)))) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓 Fn 𝐷 ∧ ∀𝑢 ∈ 𝐷 (𝑓‘𝑢) = (𝐺‘(𝑓 ↾ 𝑢)))) | ||
Theorem | tfr1onlemaccex 5997* |
We can define an acceptable function on any element of 𝑋.
As with many of the transfinite recursion theorems, we have hypotheses that state that 𝐹 is a function and that it is defined up to 𝑋. (Contributed by Jim Kingdon, 16-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ 𝑋) → ∃𝑔(𝑔 Fn 𝐶 ∧ ∀𝑢 ∈ 𝐶 (𝑔‘𝑢) = (𝐺‘(𝑔 ↾ 𝑢)))) | ||
Theorem | tfr1onlemres 5998* | Lemma for tfr1on 5999. Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 18-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ 𝑋 (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐺‘(𝑓 ↾ 𝑦)))} & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑌 ⊆ dom 𝐹) | ||
Theorem | tfr1on 5999* | Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 12-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → Fun 𝐺) & ⊢ (𝜑 → Ord 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑓 Fn 𝑥) → (𝐺‘𝑓) ∈ V) & ⊢ ((𝜑 ∧ 𝑥 ∈ ∪ 𝑋) → suc 𝑥 ∈ 𝑋) & ⊢ (𝜑 → 𝑌 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑌 ⊆ dom 𝐹) | ||
Theorem | tfri1dALT 6000* |
Alternate proof of tfri1d 5984 in terms of tfr1on 5999.
Although this does show that the tfr1on 5999 proof is general enough to also prove tfri1d 5984, the tfri1d 5984 proof is simpler in places because it does not need to deal with 𝑋 being any ordinal. For that reason, we have both proofs. (Proof modification is discouraged.) (New usage is discouraged.) (Contributed by Jim Kingdon, 20-Mar-2022.) |
⊢ 𝐹 = recs(𝐺) & ⊢ (𝜑 → ∀𝑥(Fun 𝐺 ∧ (𝐺‘𝑥) ∈ V)) ⇒ ⊢ (𝜑 → 𝐹 Fn On) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |