P. 65 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6401-6500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tfrlem6 6401*	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.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- Rel recs ( F )
Theorem	tfrlem7 6402*	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.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- Fun recs ( F )
Theorem	tfrlem8 6403*	Lemma for transfinite recursion. The domain of recs is ordinal. (Contributed by NM, 14-Aug-1994.) (Proof shortened by Alan Sare, 11-Mar-2008.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- Ord dom recs ( F )
Theorem	tfrlem9 6404*	Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- ( B e. dom recs ( F ) -> (recs ( F ) ` B ) = ( F ` (recs ( F ) |` B ) ) )
Theorem	tfrfun 6405	Transfinite recursion produces a function. (Contributed by Jim Kingdon, 20-Aug-2021.)
|- Fun recs ( F )
Theorem	tfr2a 6406	A weak version of transfinite recursion. (Contributed by Mario Carneiro, 24-Jun-2015.)
|- F = recs ( G )   =>    |- ( A e. dom F -> ( F ` A ) = ( G ` ( F |` A ) ) )
Theorem	tfr0dm 6407	Transfinite recursion is defined at the empty set. (Contributed by Jim Kingdon, 8-Mar-2022.)
|- F = recs ( G )   =>    |- ( ( G ` (/) ) e. V -> (/) e. dom F )
Theorem	tfr0 6408	Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.)
|- F = recs ( G )   =>    |- ( ( G ` (/) ) e. V -> ( F ` (/) ) = ( G ` (/) ) )
Theorem	tfrlemisucfn 6409*	We can extend an acceptable function by one element to produce a function. Lemma for tfrlemi1 6417. (Contributed by Jim Kingdon, 2-Jul-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   &    |- ( ph -> z e. On )   &    |- ( ph -> g Fn z )   &    |- ( ph -> g e. A )   =>    |- ( ph -> ( g u. { <. z , ( F ` g ) >. } ) Fn suc z )
Theorem	tfrlemisucaccv 6410*	We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 6417. (Contributed by Jim Kingdon, 4-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   &    |- ( ph -> z e. On )   &    |- ( ph -> g Fn z )   &    |- ( ph -> g e. A )   =>    |- ( ph -> ( g u. { <. z , ( F ` g ) >. } ) e. A )
Theorem	tfrlemibacc 6411*	Each element of B is an acceptable function. Lemma for tfrlemi1 6417. (Contributed by Jim Kingdon, 14-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   &    |- B = { h | E. z e. x E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( F ` g ) >. } ) ) }   &    |- ( ph -> x e. On )   &    |- ( ph -> A. z e. x E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) )   =>    |- ( ph -> B C_ A )
Theorem	tfrlemibxssdm 6412*	The union of B is defined on all ordinals. Lemma for tfrlemi1 6417. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   &    |- B = { h | E. z e. x E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( F ` g ) >. } ) ) }   &    |- ( ph -> x e. On )   &    |- ( ph -> A. z e. x E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) )   =>    |- ( ph -> x C_ dom U. B )
Theorem	tfrlemibfn 6413*	The union of B is a function defined on x. Lemma for tfrlemi1 6417. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   &    |- B = { h | E. z e. x E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( F ` g ) >. } ) ) }   &    |- ( ph -> x e. On )   &    |- ( ph -> A. z e. x E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) )   =>    |- ( ph -> U. B Fn x )
Theorem	tfrlemibex 6414*	The set B exists. Lemma for tfrlemi1 6417. (Contributed by Jim Kingdon, 17-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   &    |- B = { h | E. z e. x E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( F ` g ) >. } ) ) }   &    |- ( ph -> x e. On )   &    |- ( ph -> A. z e. x E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) )   =>    |- ( ph -> B e. _V )
Theorem	tfrlemiubacc 6415*	The union of B satisfies the recursion rule (lemma for tfrlemi1 6417). (Contributed by Jim Kingdon, 22-Apr-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   &    |- B = { h | E. z e. x E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( F ` g ) >. } ) ) }   &    |- ( ph -> x e. On )   &    |- ( ph -> A. z e. x E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) )   =>    |- ( ph -> A. u e. x ( U. B ` u ) = ( F ` ( U. B |` u ) ) )
Theorem	tfrlemiex 6416*	Lemma for tfrlemi1 6417. (Contributed by Jim Kingdon, 18-Mar-2019.) (Proof shortened by Mario Carneiro, 24-May-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   &    |- B = { h | E. z e. x E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( F ` g ) >. } ) ) }   &    |- ( ph -> x e. On )   &    |- ( ph -> A. z e. x E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) )   =>    |- ( ph -> E. f ( f Fn x /\ A. u e. x ( f ` u ) = ( F ` ( f |` u ) ) ) )
Theorem	tfrlemi1 6417*	We can define an acceptable function on any ordinal. As with many of the transfinite recursion theorems, we have a hypothesis that states that F 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.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   =>    |- ( ( ph /\ C e. On ) -> E. g ( g Fn C /\ A. u e. C ( g ` u ) = ( F ` ( g |` u ) ) ) )
Theorem	tfrlemi14d 6418*	The domain of recs is all ordinals (lemma for transfinite recursion). (Contributed by Jim Kingdon, 9-Jul-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   =>    |- ( ph -> dom recs ( F ) = On )
Theorem	tfrexlem 6419*	The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   =>    |- ( ( ph /\ C e. V ) -> (recs ( F ) ` C ) e. _V )
Theorem	tfri1d 6420*	Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47, with an additional condition. The condition is that G is defined "everywhere", which is stated here as ( G ` x ) e. _V. Alternately, A. x e. On A. f ( f Fn x -> f e. dom G ) would suffice. Given a function G satisfying that condition, we define a class A of all "acceptable" functions. The final function we're interested in is the union F = recs ( G ) of them. F is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of F. In this first part we show that F is a function whose domain is all ordinal numbers. (Contributed by Jim Kingdon, 4-May-2019.) (Revised by Mario Carneiro, 24-May-2019.)
|- F = recs ( G )   &    |- ( ph -> A. x ( Fun G /\ ( G ` x ) e. _V ) )   =>    |- ( ph -> F Fn On )
Theorem	tfri2d 6421*	Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule G ( as described at tfri1 6450). Here we show that the function F has the property that for any function G satisfying that condition, the "next" value of F is G recursively applied to all "previous" values of F. (Contributed by Jim Kingdon, 4-May-2019.)
|- F = recs ( G )   &    |- ( ph -> A. x ( Fun G /\ ( G ` x ) e. _V ) )   =>    |- ( ( ph /\ A e. On ) -> ( F ` A ) = ( G ` ( F |` A ) ) )
Theorem	tfr1onlem3ag 6422*	Lemma for transfinite recursion. This lemma changes some bound variables in A (version of tfrlem3ag 6394 but for tfr1on 6435 related lemmas). (Contributed by Jim Kingdon, 13-Mar-2022.)
|- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   =>    |- ( H e. V -> ( H e. A <-> E. z e. X ( H Fn z /\ A. w e. z ( H ` w ) = ( G ` ( H |` w ) ) ) ) )
Theorem	tfr1onlem3 6423*	Lemma for transfinite recursion. This lemma changes some bound variables in A (version of tfrlem3 6396 but for tfr1on 6435 related lemmas). (Contributed by Jim Kingdon, 14-Mar-2022.)
|- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   =>    |- A = { g | E. z e. X ( g Fn z /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) }
Theorem	tfr1onlemssrecs 6424*	Lemma for tfr1on 6435. The union of functions acceptable for tfr1on 6435 is a subset of recs. (Contributed by Jim Kingdon, 15-Mar-2022.)
|- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- ( ph -> Ord X )   =>    |- ( ph -> U. A C_ recs ( G ) )
Theorem	tfr1onlemsucfn 6425*	We can extend an acceptable function by one element to produce a function. Lemma for tfr1on 6435. (Contributed by Jim Kingdon, 12-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- ( ph -> z e. X )   &    |- ( ph -> g Fn z )   &    |- ( ph -> g e. A )   =>    |- ( ph -> ( g u. { <. z , ( G ` g ) >. } ) Fn suc z )
Theorem	tfr1onlemsucaccv 6426*	Lemma for tfr1on 6435. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 12-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- ( ph -> Y e. X )   &    |- ( ph -> z e. Y )   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> g Fn z )   &    |- ( ph -> g e. A )   =>    |- ( ph -> ( g u. { <. z , ( G ` g ) >. } ) e. A )
Theorem	tfr1onlembacc 6427*	Lemma for tfr1on 6435. Each element of B is an acceptable function. (Contributed by Jim Kingdon, 14-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> B C_ A )
Theorem	tfr1onlembxssdm 6428*	Lemma for tfr1on 6435. The union of B is defined on all elements of X. (Contributed by Jim Kingdon, 14-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> D C_ dom U. B )
Theorem	tfr1onlembfn 6429*	Lemma for tfr1on 6435. The union of B is a function defined on x. (Contributed by Jim Kingdon, 15-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> U. B Fn D )
Theorem	tfr1onlembex 6430*	Lemma for tfr1on 6435. The set B exists. (Contributed by Jim Kingdon, 14-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> B e. _V )
Theorem	tfr1onlemubacc 6431*	Lemma for tfr1on 6435. The union of B satisfies the recursion rule. (Contributed by Jim Kingdon, 15-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> A. u e. D ( U. B ` u ) = ( G ` ( U. B |` u ) ) )
Theorem	tfr1onlemex 6432*	Lemma for tfr1on 6435. (Contributed by Jim Kingdon, 16-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g Fn z /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g Fn z /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> E. f ( f Fn D /\ A. u e. D ( f ` u ) = ( G ` ( f |` u ) ) ) )
Theorem	tfr1onlemaccex 6433*	We can define an acceptable function on any element of X. As with many of the transfinite recursion theorems, we have hypotheses that state that F is a function and that it is defined up to X. (Contributed by Jim Kingdon, 16-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   =>    |- ( ( ph /\ C e. X ) -> E. g ( g Fn C /\ A. u e. C ( g ` u ) = ( G ` ( g |` u ) ) ) )
Theorem	tfr1onlemres 6434*	Lemma for tfr1on 6435. Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 18-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- A = { f | E. x e. X ( f Fn x /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> Y e. X )   =>    |- ( ph -> Y C_ dom F )
Theorem	tfr1on 6435*	Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 12-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f Fn x ) -> ( G ` f ) e. _V )   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> Y e. X )   =>    |- ( ph -> Y C_ dom F )
Theorem	tfri1dALT 6436*	Alternate proof of tfri1d 6420 in terms of tfr1on 6435. Although this does show that the tfr1on 6435 proof is general enough to also prove tfri1d 6420, the tfri1d 6420 proof is simpler in places because it does not need to deal with X 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.)
|- F = recs ( G )   &    |- ( ph -> A. x ( Fun G /\ ( G ` x ) e. _V ) )   =>    |- ( ph -> F Fn On )
Theorem	tfrcllemssrecs 6437*	Lemma for tfrcl 6449. The union of functions acceptable for tfrcl 6449 is a subset of recs. (Contributed by Jim Kingdon, 25-Mar-2022.)
|- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- ( ph -> Ord X )   =>    |- ( ph -> U. A C_ recs ( G ) )
Theorem	tfrcllemsucfn 6438*	We can extend an acceptable function by one element to produce a function. Lemma for tfrcl 6449. (Contributed by Jim Kingdon, 24-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- ( ph -> z e. X )   &    |- ( ph -> g : z --> S )   &    |- ( ph -> g e. A )   =>    |- ( ph -> ( g u. { <. z , ( G ` g ) >. } ) : suc z --> S )
Theorem	tfrcllemsucaccv 6439*	Lemma for tfrcl 6449. We can extend an acceptable function by one element to produce an acceptable function. (Contributed by Jim Kingdon, 24-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- ( ph -> Y e. X )   &    |- ( ph -> z e. Y )   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> g : z --> S )   &    |- ( ph -> g e. A )   =>    |- ( ph -> ( g u. { <. z , ( G ` g ) >. } ) e. A )
Theorem	tfrcllembacc 6440*	Lemma for tfrcl 6449. Each element of B is an acceptable function. (Contributed by Jim Kingdon, 25-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g : z --> S /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> B C_ A )
Theorem	tfrcllembxssdm 6441*	Lemma for tfrcl 6449. The union of B is defined on all elements of X. (Contributed by Jim Kingdon, 25-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g : z --> S /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> D C_ dom U. B )
Theorem	tfrcllembfn 6442*	Lemma for tfrcl 6449. The union of B is a function defined on x. (Contributed by Jim Kingdon, 25-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g : z --> S /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> U. B : D --> S )
Theorem	tfrcllembex 6443*	Lemma for tfrcl 6449. The set B exists. (Contributed by Jim Kingdon, 25-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g : z --> S /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> B e. _V )
Theorem	tfrcllemubacc 6444*	Lemma for tfrcl 6449. The union of B satisfies the recursion rule. (Contributed by Jim Kingdon, 25-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g : z --> S /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> A. u e. D ( U. B ` u ) = ( G ` ( U. B |` u ) ) )
Theorem	tfrcllemex 6445*	Lemma for tfrcl 6449. (Contributed by Jim Kingdon, 26-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- B = { h | E. z e. D E. g ( g : z --> S /\ g e. A /\ h = ( g u. { <. z , ( G ` g ) >. } ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> D e. X )   &    |- ( ph -> A. z e. D E. g ( g : z --> S /\ A. w e. z ( g ` w ) = ( G ` ( g |` w ) ) ) )   =>    |- ( ph -> E. f ( f : D --> S /\ A. u e. D ( f ` u ) = ( G ` ( f |` u ) ) ) )
Theorem	tfrcllemaccex 6446*	We can define an acceptable function on any element of X. As with many of the transfinite recursion theorems, we have hypotheses that state that F is a function and that it is defined up to X. (Contributed by Jim Kingdon, 26-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   =>    |- ( ( ph /\ C e. X ) -> E. g ( g : C --> S /\ A. u e. C ( g ` u ) = ( G ` ( g |` u ) ) ) )
Theorem	tfrcllemres 6447*	Lemma for tfr1on 6435. Recursion is defined on an ordinal if the characteristic function is defined up to a suitable point. (Contributed by Jim Kingdon, 18-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- A = { f | E. x e. X ( f : x --> S /\ A. y e. x ( f ` y ) = ( G ` ( f |` y ) ) ) }   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> Y e. X )   =>    |- ( ph -> Y C_ dom F )
Theorem	tfrcldm 6448*	Recursion is defined on an ordinal if the characteristic function satisfies a closure hypothesis up to a suitable point. (Contributed by Jim Kingdon, 26-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> Y e. U. X )   =>    |- ( ph -> Y e. dom F )
Theorem	tfrcl 6449*	Closure for transfinite recursion. As with tfr1on 6435, the characteristic function must be defined up to a suitable point, not necessarily on all ordinals. (Contributed by Jim Kingdon, 25-Mar-2022.)
|- F = recs ( G )   &    |- ( ph -> Fun G )   &    |- ( ph -> Ord X )   &    |- ( ( ph /\ x e. X /\ f : x --> S ) -> ( G ` f ) e. S )   &    |- ( ( ph /\ x e. U. X ) -> suc x e. X )   &    |- ( ph -> Y e. U. X )   =>    |- ( ph -> ( F ` Y ) e. S )
Theorem	tfri1 6450*	Principle of Transfinite Recursion, part 1 of 3. Theorem 7.41(1) of [TakeutiZaring] p. 47, with an additional condition. The condition is that G is defined "everywhere", which is stated here as ( G ` x ) e. _V. Alternately, A. x e. On A. f ( f Fn x -> f e. dom G ) would suffice. Given a function G satisfying that condition, we define a class A of all "acceptable" functions. The final function we're interested in is the union F = recs ( G ) of them. F is then said to be defined by transfinite recursion. The purpose of the 3 parts of this theorem is to demonstrate properties of F. In this first part we show that F is a function whose domain is all ordinal numbers. (Contributed by Jim Kingdon, 4-May-2019.) (Revised by Mario Carneiro, 24-May-2019.)
|- F = recs ( G )   &    |- ( Fun G /\ ( G ` x ) e. _V )   =>    |- F Fn On
Theorem	tfri2 6451*	Principle of Transfinite Recursion, part 2 of 3. Theorem 7.41(2) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule G ( as described at tfri1 6450). Here we show that the function F has the property that for any function G satisfying that condition, the "next" value of F is G recursively applied to all "previous" values of F. (Contributed by Jim Kingdon, 4-May-2019.)
|- F = recs ( G )   &    |- ( Fun G /\ ( G ` x ) e. _V )   =>    |- ( A e. On -> ( F ` A ) = ( G ` ( F |` A ) ) )
Theorem	tfri3 6452*	Principle of Transfinite Recursion, part 3 of 3. Theorem 7.41(3) of [TakeutiZaring] p. 47, with an additional condition on the recursion rule G ( as described at tfri1 6450). Finally, we show that F is unique. We do this by showing that any class B with the same properties of F that we showed in parts 1 and 2 is identical to F. (Contributed by Jim Kingdon, 4-May-2019.)
|- F = recs ( G )   &    |- ( Fun G /\ ( G ` x ) e. _V )   =>    |- ( ( B Fn On /\ A. x e. On ( B ` x ) = ( G ` ( B |` x ) ) ) -> B = F )
Theorem	tfrex 6453*	The transfinite recursion function is set-like if the input is. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- F = recs ( G )   &    |- ( ph -> A. x ( Fun G /\ ( G ` x ) e. _V ) )   =>    |- ( ( ph /\ A e. V ) -> ( F ` A ) e. _V )
2.6.21  Recursive definition generator
Syntax	crdg 6454	Extend class notation with the recursive definition generator, with characteristic function F and initial value I.
class rec ( F , I )
Definition	df-irdg 6455*	Define a recursive definition generator on On (the class of ordinal numbers) with characteristic function F and initial value I. This rather amazing operation allows us to define, with compact direct definitions, functions that are usually defined in textbooks only with indirect self-referencing recursive definitions. A recursive definition requires advanced metalogic to justify - in particular, eliminating a recursive definition is very difficult and often not even shown in textbooks. On the other hand, the elimination of a direct definition is a matter of simple mechanical substitution. The price paid is the daunting complexity of our rec operation (especially when df-recs 6390 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple. In classical logic it would be easier to divide this definition into cases based on whether the domain of g is zero, a successor, or a limit ordinal. Cases do not (in general) work that way in intuitionistic logic, so instead we choose a definition which takes the union of all the results of the characteristic function for ordinals in the domain of g. This means that this definition has the expected properties for increasing and continuous ordinal functions, which include ordinal addition and multiplication. For finite recursion we also define df-frec 6476 and for suitable characteristic functions df-frec 6476 yields the same result as rec restricted to om, as seen at frecrdg 6493. Note: We introduce rec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by Jim Kingdon, 19-May-2019.)
|- rec ( F , I ) = recs ( ( g e. _V |-> ( I u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) )
Theorem	rdgeq1 6456	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
|- ( F = G -> rec ( F , A ) = rec ( G , A ) )
Theorem	rdgeq2 6457	Equality theorem for the recursive definition generator. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 9-May-2015.)
|- ( A = B -> rec ( F , A ) = rec ( F , B ) )
Theorem	rdgfun 6458	The recursive definition generator is a function. (Contributed by Mario Carneiro, 16-Nov-2014.)
|- Fun rec ( F , A )
Theorem	rdgtfr 6459*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.)
|- ( ( A. z ( F ` z ) e. _V /\ A e. V ) -> ( Fun ( g e. _V |-> ( A u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) /\ ( ( g e. _V |-> ( A u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) ` f ) e. _V ) )
Theorem	rdgruledefgg 6460*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
|- ( ( F Fn _V /\ A e. V ) -> ( Fun ( g e. _V |-> ( A u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) /\ ( ( g e. _V |-> ( A u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) ` f ) e. _V ) )
Theorem	rdgruledefg 6461*	The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 4-Jul-2019.)
|- F Fn _V   =>    |- ( A e. V -> ( Fun ( g e. _V |-> ( A u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) /\ ( ( g e. _V |-> ( A u. U_ x e. dom g ( F ` ( g ` x ) ) ) ) ` f ) e. _V ) )
Theorem	rdgexggg 6462	The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.)
|- ( ( F Fn _V /\ A e. V /\ B e. W ) -> ( rec ( F , A ) ` B ) e. _V )
Theorem	rdgexgg 6463	The recursive definition generator produces a set on a set input. (Contributed by Jim Kingdon, 4-Jul-2019.)
|- F Fn _V   =>    |- ( ( A e. V /\ B e. W ) -> ( rec ( F , A ) ` B ) e. _V )
Theorem	rdgifnon 6464	The recursive definition generator is a function on ordinal numbers. The F Fn _V condition states that the characteristic function is defined for all sets (being defined for all ordinals might be enough if being used in a manner similar to rdgon 6471; in cases like df-oadd 6505 either presumably could work). (Contributed by Jim Kingdon, 13-Jul-2019.)
|- ( ( F Fn _V /\ A e. V ) -> rec ( F , A ) Fn On )
Theorem	rdgifnon2 6465*	The recursive definition generator is a function on ordinal numbers. (Contributed by Jim Kingdon, 14-May-2020.)
|- ( ( A. z ( F ` z ) e. _V /\ A e. V ) -> rec ( F , A ) Fn On )
Theorem	rdgivallem 6466*	Value of the recursive definition generator. Lemma for rdgival 6467 which simplifies the value further. (Contributed by Jim Kingdon, 13-Jul-2019.) (New usage is discouraged.)
|- ( ( F Fn _V /\ A e. V /\ B e. On ) -> ( rec ( F , A ) ` B ) = ( A u. U_ x e. B ( F ` ( ( rec ( F , A ) |` B ) ` x ) ) ) )
Theorem	rdgival 6467*	Value of the recursive definition generator. (Contributed by Jim Kingdon, 26-Jul-2019.)
|- ( ( F Fn _V /\ A e. V /\ B e. On ) -> ( rec ( F , A ) ` B ) = ( A u. U_ x e. B ( F ` ( rec ( F , A ) ` x ) ) ) )
Theorem	rdgss 6468	Subset and recursive definition generator. (Contributed by Jim Kingdon, 15-Jul-2019.)
|- ( ph -> F Fn _V )   &    |- ( ph -> I e. V )   &    |- ( ph -> A e. On )   &    |- ( ph -> B e. On )   &    |- ( ph -> A C_ B )   =>    |- ( ph -> ( rec ( F , I ) ` A ) C_ ( rec ( F , I ) ` B ) )
Theorem	rdgisuc1 6469*	One way of describing the value of the recursive definition generator at a successor. There is no condition on the characteristic function F other than F Fn _V. Given that, the resulting expression encompasses both the expected successor term ( F ` ( rec ( F , A ) ` B ) ) but also terms that correspond to the initial value A and to limit ordinals U_ x e. B ( F ` ( rec ( F , A ) ` x ) ). If we add conditions on the characteristic function, we can show tighter results such as rdgisucinc 6470. (Contributed by Jim Kingdon, 9-Jun-2019.)
|- ( ph -> F Fn _V )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. On )   =>    |- ( ph -> ( rec ( F , A ) ` suc B ) = ( A u. ( U_ x e. B ( F ` ( rec ( F , A ) ` x ) ) u. ( F ` ( rec ( F , A ) ` B ) ) ) ) )
Theorem	rdgisucinc 6470*	Value of the recursive definition generator at a successor. This can be thought of as a generalization of oasuc 6549 and omsuc 6557. (Contributed by Jim Kingdon, 29-Aug-2019.)
|- ( ph -> F Fn _V )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. On )   &    |- ( ph -> A. x x C_ ( F ` x ) )   =>    |- ( ph -> ( rec ( F , A ) ` suc B ) = ( F ` ( rec ( F , A ) ` B ) ) )
Theorem	rdgon 6471*	Evaluating the recursive definition generator produces an ordinal. There is a hypothesis that the characteristic function produces ordinals on ordinal arguments. (Contributed by Jim Kingdon, 26-Jul-2019.) (Revised by Jim Kingdon, 13-Apr-2022.)
|- ( ph -> A e. On )   &    |- ( ph -> A. x e. On ( F ` x ) e. On )   =>    |- ( ( ph /\ B e. On ) -> ( rec ( F , A ) ` B ) e. On )
Theorem	rdg0 6472	The initial value of the recursive definition generator. (Contributed by NM, 23-Apr-1995.) (Revised by Mario Carneiro, 14-Nov-2014.)
|- A e. _V   =>    |- ( rec ( F , A ) ` (/) ) = A
Theorem	rdg0g 6473	The initial value of the recursive definition generator. (Contributed by NM, 25-Apr-1995.)
|- ( A e. C -> ( rec ( F , A ) ` (/) ) = A )
Theorem	rdgexg 6474	The recursive definition generator produces a set on a set input. (Contributed by Mario Carneiro, 3-Jul-2019.)
|- A e. _V   &    |- F Fn _V   =>    |- ( B e. V -> ( rec ( F , A ) ` B ) e. _V )
2.6.22  Finite recursion
Syntax	cfrec 6475	Extend class notation with the finite recursive definition generator, with characteristic function F and initial value I.
class frec ( F , I )
Definition	df-frec 6476*	Define a recursive definition generator on om (the class of finite ordinals) with characteristic function F and initial value I. This rather amazing operation allows us to define, with compact direct definitions, functions that are usually defined in textbooks only with indirect self-referencing recursive definitions. A recursive definition requires advanced metalogic to justify - in particular, eliminating a recursive definition is very difficult and often not even shown in textbooks. On the other hand, the elimination of a direct definition is a matter of simple mechanical substitution. The price paid is the daunting complexity of our frec operation (especially when df-recs 6390 that it is built on is also eliminated). But once we get past this hurdle, definitions that would otherwise be recursive become relatively simple; see frec0g 6482 and frecsuc 6492. Unlike with transfinite recursion, finite recurson can readily divide definitions and proofs into zero and successor cases, because even without excluded middle we have theorems such as nn0suc 4651. The analogous situation with transfinite recursion - being able to say that an ordinal is zero, successor, or limit - is enabled by excluded middle and thus is not available to us. For the characteristic functions which satisfy the conditions given at frecrdg 6493, this definition and df-irdg 6455 restricted to om produce the same result. Note: We introduce frec with the philosophical goal of being able to eliminate all definitions with direct mechanical substitution and to verify easily the soundness of definitions. Metamath itself has no built-in technical limitation that prevents multiple-part recursive definitions in the traditional textbook style. (Contributed by Mario Carneiro and Jim Kingdon, 10-Aug-2019.)
|- frec ( F , I ) = (recs ( ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. I ) ) } ) ) |` om )
Theorem	freceq1 6477	Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( F = G -> frec ( F , A ) = frec ( G , A ) )
Theorem	freceq2 6478	Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- ( A = B -> frec ( F , A ) = frec ( F , B ) )
Theorem	frecex 6479	Finite recursion produces a set. (Contributed by Jim Kingdon, 20-Aug-2021.)
|- frec ( F , A ) e. _V
Theorem	frecfun 6480	Finite recursion produces a function. See also frecfnom 6486 which also states that the domain of that function is om but which puts conditions on A and F. (Contributed by Jim Kingdon, 13-Feb-2022.)
|- Fun frec ( F , A )
Theorem	nffrec 6481	Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.)
|- F/_ x F   &    |- F/_ x A   =>    |- F/_ xfrec ( F , A )
Theorem	frec0g 6482	The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.)
|- ( A e. V -> (frec ( F , A ) ` (/) ) = A )
Theorem	frecabex 6483*	The class abstraction from df-frec 6476 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.)
|- ( ph -> S e. V )   &    |- ( ph -> A. y ( F ` y ) e. _V )   &    |- ( ph -> A e. W )   =>    |- ( ph -> { x | ( E. m e. om ( dom S = suc m /\ x e. ( F ` ( S ` m ) ) ) \/ ( dom S = (/) /\ x e. A ) ) } e. _V )
Theorem	frecabcl 6484*	The class abstraction from df-frec 6476 exists. Unlike frecabex 6483 the function F only needs to be defined on S, not all sets. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 21-Mar-2022.)
|- ( ph -> N e. om )   &    |- ( ph -> G : N --> S )   &    |- ( ph -> A. y e. S ( F ` y ) e. S )   &    |- ( ph -> A e. S )   =>    |- ( ph -> { x | ( E. m e. om ( dom G = suc m /\ x e. ( F ` ( G ` m ) ) ) \/ ( dom G = (/) /\ x e. A ) ) } e. S )
Theorem	frectfr 6485*	Lemma to connect transfinite recursion theorems with finite recursion. That is, given the conditions F Fn _V and A e. V on frec ( F , A ), we want to be able to apply tfri1d 6420 or tfri2d 6421, and this lemma lets us satisfy hypotheses of those theorems. (Contributed by Jim Kingdon, 15-Aug-2019.)
|- G = ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. A ) ) } )   =>    |- ( ( A. z ( F ` z ) e. _V /\ A e. V ) -> A. y ( Fun G /\ ( G ` y ) e. _V ) )
Theorem	frecfnom 6486*	The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.)
|- ( ( A. z ( F ` z ) e. _V /\ A e. V ) -> frec ( F , A ) Fn om )
Theorem	freccllem 6487*	Lemma for freccl 6488. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 27-Mar-2022.)
|- ( ph -> A e. S )   &    |- ( ( ph /\ z e. S ) -> ( F ` z ) e. S )   &    |- ( ph -> B e. om )   &    |- G = recs ( ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. A ) ) } ) )   =>    |- ( ph -> (frec ( F , A ) ` B ) e. S )
Theorem	freccl 6488*	Closure for finite recursion. (Contributed by Jim Kingdon, 27-Mar-2022.)
|- ( ph -> A e. S )   &    |- ( ( ph /\ z e. S ) -> ( F ` z ) e. S )   &    |- ( ph -> B e. om )   =>    |- ( ph -> (frec ( F , A ) ` B ) e. S )
Theorem	frecfcllem 6489*	Lemma for frecfcl 6490. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 30-Mar-2022.)
|- G = recs ( ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. A ) ) } ) )   =>    |- ( ( A. z e. S ( F ` z ) e. S /\ A e. S ) -> frec ( F , A ) : om --> S )
Theorem	frecfcl 6490*	Finite recursion yields a function on the natural numbers. (Contributed by Jim Kingdon, 30-Mar-2022.)
|- ( ( A. z e. S ( F ` z ) e. S /\ A e. S ) -> frec ( F , A ) : om --> S )
Theorem	frecsuclem 6491*	Lemma for frecsuc 6492. Just giving a name to a common expression to simplify the proof. (Contributed by Jim Kingdon, 29-Mar-2022.)
|- G = ( g e. _V |-> { x | ( E. m e. om ( dom g = suc m /\ x e. ( F ` ( g ` m ) ) ) \/ ( dom g = (/) /\ x e. A ) ) } )   =>    |- ( ( A. z e. S ( F ` z ) e. S /\ A e. S /\ B e. om ) -> (frec ( F , A ) ` suc B ) = ( F ` (frec ( F , A ) ` B ) ) )
Theorem	frecsuc 6492*	The successor value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 31-Mar-2022.)
|- ( ( A. z e. S ( F ` z ) e. S /\ A e. S /\ B e. om ) -> (frec ( F , A ) ` suc B ) = ( F ` (frec ( F , A ) ` B ) ) )
Theorem	frecrdg 6493*	Transfinite recursion restricted to omega. Given a suitable characteristic function, df-frec 6476 produces the same results as df-irdg 6455 restricted to om. Presumably the theorem would also hold if F Fn _V were changed to A. z ( F ` z ) e. _V. (Contributed by Jim Kingdon, 29-Aug-2019.)
|- ( ph -> F Fn _V )   &    |- ( ph -> A e. V )   &    |- ( ph -> A. x x C_ ( F ` x ) )   =>    |- ( ph -> frec ( F , A ) = ( rec ( F , A ) |` om ) )
2.6.23  Ordinal arithmetic
Syntax	c1o 6494	Extend the definition of a class to include the ordinal number 1.
class 1o
Syntax	c2o 6495	Extend the definition of a class to include the ordinal number 2.
class 2o
Syntax	c3o 6496	Extend the definition of a class to include the ordinal number 3.
class 3o
Syntax	c4o 6497	Extend the definition of a class to include the ordinal number 4.
class 4o
Syntax	coa 6498	Extend the definition of a class to include the ordinal addition operation.
class +o
Syntax	comu 6499	Extend the definition of a class to include the ordinal multiplication operation.
class .o
Syntax	coei 6500	Extend the definition of a class to include the ordinal exponentiation operation.
class ↑o