P. 64 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6301-6400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	tposeqd 6301	Equality theorem for transposition. (Contributed by Mario Carneiro, 7-Jan-2017.)
|- ( ph -> F = G )   =>    |- ( ph -> tpos F = tpos G )
Theorem	tposssxp 6302	The transposition is a subset of a cross product. (Contributed by Mario Carneiro, 12-Jan-2017.)
|- tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F )
Theorem	reltpos 6303	The transposition is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- Rel tpos F
Theorem	brtpos2 6304	Value of the transposition at a pair <. A , B >.. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( B e. V -> ( Atpos F B <-> ( A e. ( `' dom F u. { (/) } ) /\ U. `' { A } F B ) ) )
Theorem	brtpos0 6305	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.)
|- ( A e. V -> ( (/)tpos F A <-> (/) F A ) )
Theorem	reldmtpos 6306	Necessary and sufficient condition for dom tpos F to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom tpos F <-> -. (/) e. dom F )
Theorem	brtposg 6307	The transposition swaps arguments of a three-parameter relation. (Contributed by Jim Kingdon, 31-Jan-2019.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. A , B >.tpos F C <-> <. B , A >. F C ) )
Theorem	ottposg 6308	The transposition swaps the first two elements in a collection of ordered triples. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. A , B , C >. e. tpos F <-> <. B , A , C >. e. F ) )
Theorem	dmtpos 6309	The domain of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> dom tpos F = `' dom F )
Theorem	rntpos 6310	The range of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> ran tpos F = ran F )
Theorem	tposexg 6311	The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( F e. V -> tpos F e. _V )
Theorem	ovtposg 6312	The transposition swaps the arguments in a two-argument function. When F is a matrix, which is to say a function from ( 1 ... m ) X. ( 1 ... n ) to the reals or some ring, tpos F is the transposition of F, which is where the name comes from. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( ( A e. V /\ B e. W ) -> ( Atpos F B ) = ( B F A ) )
Theorem	tposfun 6313	The transposition of a function is a function. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Fun F -> Fun tpos F )
Theorem	dftpos2 6314*	Alternate definition of tpos when F has relational domain. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> tpos F = ( F o. ( x e. `' dom F |-> U. `' { x } ) ) )
Theorem	dftpos3 6315*	Alternate definition of tpos when F has relational domain. Compare df-cnv 4667. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- ( Rel dom F -> tpos F = { <. <. x , y >. , z >. | <. y , x >. F z } )
Theorem	dftpos4 6316*	Alternate definition of tpos. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- tpos F = ( F o. ( x e. ( ( _V X. _V ) u. { (/) } ) |-> U. `' { x } ) )
Theorem	tpostpos 6317	Value of the double transposition for a general class F. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- tpos tpos F = ( F i^i ( ( ( _V X. _V ) u. { (/) } ) X. _V ) )
Theorem	tpostpos2 6318	Value of the double transposition for a relation on triples. (Contributed by Mario Carneiro, 16-Sep-2015.)
|- ( ( Rel F /\ Rel dom F ) -> tpos tpos F = F )
Theorem	tposfn2 6319	The domain of a transposition. (Contributed by NM, 10-Sep-2015.)
|- ( Rel A -> ( F Fn A -> tpos F Fn `' A ) )
Theorem	tposfo2 6320	Condition for a surjective transposition. (Contributed by NM, 10-Sep-2015.)
|- ( Rel A -> ( F : A -onto-> B -> tpos F : `' A -onto-> B ) )
Theorem	tposf2 6321	The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015.)
|- ( Rel A -> ( F : A --> B -> tpos F : `' A --> B ) )
Theorem	tposf12 6322	Condition for an injective transposition. (Contributed by NM, 10-Sep-2015.)
|- ( Rel A -> ( F : A -1-1-> B -> tpos F : `' A -1-1-> B ) )
Theorem	tposf1o2 6323	Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015.)
|- ( Rel A -> ( F : A -1-1-onto-> B -> tpos F : `' A -1-1-onto-> B ) )
Theorem	tposfo 6324	The domain and codomain/range of a transposition. (Contributed by NM, 10-Sep-2015.)
|- ( F : ( A X. B ) -onto-> C -> tpos F : ( B X. A ) -onto-> C )
Theorem	tposf 6325	The domain and codomain of a transposition. (Contributed by NM, 10-Sep-2015.)
|- ( F : ( A X. B ) --> C -> tpos F : ( B X. A ) --> C )
Theorem	tposfn 6326	Functionality of a transposition. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( F Fn ( A X. B ) -> tpos F Fn ( B X. A ) )
Theorem	tpos0 6327	Transposition of the empty set. (Contributed by NM, 10-Sep-2015.)
|- tpos (/) = (/)
Theorem	tposco 6328	Transposition of a composition. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- tpos ( F o. G ) = ( F o. tpos G )
Theorem	tpossym 6329*	Two ways to say a function is symmetric. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( F Fn ( A X. A ) -> (tpos F = F <-> A. x e. A A. y e. A ( x F y ) = ( y F x ) ) )
Theorem	tposeqi 6330	Equality theorem for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F = G   =>    |- tpos F = tpos G
Theorem	tposex 6331	A transposition is a set. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F e. _V   =>    |- tpos F e. _V
Theorem	nftpos 6332	Hypothesis builder for transposition. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F/_ x F   =>    |- F/_ xtpos F
Theorem	tposoprab 6333*	Transposition of a class of ordered triples. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F = { <. <. x , y >. , z >. | ph }   =>    |- tpos F = { <. <. y , x >. , z >. | ph }
Theorem	tposmpo 6334*	Transposition of a two-argument mapping. (Contributed by Mario Carneiro, 10-Sep-2015.)
|- F = ( x e. A , y e. B |-> C )   =>    |- tpos F = ( y e. B , x e. A |-> C )
2.6.18  Undefined values
Theorem	pwuninel2 6335	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.)
|- ( U. A e. V -> -. ~P U. A e. A )
Theorem	2pwuninelg 6336	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.)
|- ( A e. V -> -. ~P ~P U. A e. A )
2.6.19  Functions on ordinals; strictly monotone ordinal functions
Theorem	iunon 6337*	The indexed union of a set of ordinal numbers B ( x ) is an ordinal number. (Contributed by NM, 13-Oct-2003.) (Revised by Mario Carneiro, 5-Dec-2016.)
|- ( ( A e. V /\ A. x e. A B e. On ) -> U_ x e. A B e. On )
Syntax	wsmo 6338	Introduce the strictly monotone ordinal function. A strictly monotone function is one that is constantly increasing across the ordinals.
wff Smo A
Definition	df-smo 6339*	Definition of a strictly monotone ordinal function. Definition 7.46 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 15-Nov-2011.)
|- ( Smo A <-> ( A : dom A --> On /\ Ord dom A /\ A. x e. dom A A. y e. dom A ( x e. y -> ( A ` x ) e. ( A ` y ) ) ) )
Theorem	dfsmo2 6340*	Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 4-Mar-2013.)
|- ( Smo F <-> ( F : dom F --> On /\ Ord dom F /\ A. x e. dom F A. y e. x ( F ` y ) e. ( F ` x ) ) )
Theorem	issmo 6341*	Conditions for which A is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 15-Nov-2011.)
|- A : B --> On   &    |- Ord B   &    |- ( ( x e. B /\ y e. B ) -> ( x e. y -> ( A ` x ) e. ( A ` y ) ) )   &    |- dom A = B   =>    |- Smo A
Theorem	issmo2 6342*	Alternate definition of a strictly monotone ordinal function. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- ( F : A --> B -> ( ( B C_ On /\ Ord A /\ A. x e. A A. y e. x ( F ` y ) e. ( F ` x ) ) -> Smo F ) )
Theorem	smoeq 6343	Equality theorem for strictly monotone functions. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( A = B -> ( Smo A <-> Smo B ) )
Theorem	smodm 6344	The domain of a strictly monotone function is an ordinal. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- ( Smo A -> Ord dom A )
Theorem	smores 6345	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 A /\ B e. dom A ) -> Smo ( A |` B ) )
Theorem	smores3 6346	A strictly monotone function restricted to an ordinal remains strictly monotone. (Contributed by Andrew Salmon, 19-Nov-2011.)
|- ( ( Smo ( A |` B ) /\ C e. ( dom A i^i B ) /\ Ord B ) -> Smo ( A |` C ) )
Theorem	smores2 6347	A strictly monotone ordinal function restricted to an ordinal is still monotone. (Contributed by Mario Carneiro, 15-Mar-2013.)
|- ( ( Smo F /\ Ord A ) -> Smo ( F |` A ) )
Theorem	smodm2 6348	The domain of a strictly monotone ordinal function is an ordinal. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- ( ( F Fn A /\ Smo F ) -> Ord A )
Theorem	smofvon2dm 6349	The function values of a strictly monotone ordinal function are ordinals. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- ( ( Smo F /\ B e. dom F ) -> ( F ` B ) e. On )
Theorem	iordsmo 6350	The identity relation restricted to the ordinals is a strictly monotone function. (Contributed by Andrew Salmon, 16-Nov-2011.)
|- Ord A   =>    |- Smo ( _I |` A )
Theorem	smo0 6351	The null set is a strictly monotone ordinal function. (Contributed by Andrew Salmon, 20-Nov-2011.)
|- Smo (/)
Theorem	smofvon 6352	If B is a strictly monotone ordinal function, and A is in the domain of B, then the value of the function at A is an ordinal. (Contributed by Andrew Salmon, 20-Nov-2011.)
|- ( ( Smo B /\ A e. dom B ) -> ( B ` A ) e. On )
Theorem	smoel 6353	If x is less than y then a strictly monotone function's value will be strictly less at x than at y. (Contributed by Andrew Salmon, 22-Nov-2011.)
|- ( ( Smo B /\ A e. dom B /\ C e. A ) -> ( B ` C ) e. ( B ` A ) )
Theorem	smoiun 6354*	The value of a strictly monotone ordinal function contains its indexed union. (Contributed by Andrew Salmon, 22-Nov-2011.)
|- ( ( Smo B /\ A e. dom B ) -> U_ x e. A ( B ` x ) C_ ( B ` A ) )
Theorem	smoiso 6355	If F is an isomorphism from an ordinal A onto B, which is a subset of the ordinals, then F is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.)
|- ( ( F Isom _E , _E ( A , B ) /\ Ord A /\ B C_ On ) -> Smo F )
Theorem	smoel2 6356	A strictly monotone ordinal function preserves the epsilon relation. (Contributed by Mario Carneiro, 12-Mar-2013.)
|- ( ( ( F Fn A /\ Smo F ) /\ ( B e. A /\ C e. B ) ) -> ( F ` C ) e. ( F ` B ) )
2.6.20  "Strong" transfinite recursion
Syntax	crecs 6357	Notation for a function defined by strong transfinite recursion.
class recs ( F )
Definition	df-recs 6358*	Define a function recs ( F ) on On, the class of ordinal numbers, by transfinite recursion given a rule F which sets the next value given all values so far. See df-irdg 6423 for more details on why this definition is desirable. Unlike df-irdg 6423 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 6388 and tfri2d 6389 for the primary contract of this definition. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- recs ( F ) = U. { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }
Theorem	recseq 6359	Equality theorem for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- ( F = G -> recs ( F ) = recs ( G ) )
Theorem	nfrecs 6360	Bound-variable hypothesis builder for recs. (Contributed by Stefan O'Rear, 18-Jan-2015.)
|- F/_ x F   =>    |- F/_ xrecs ( F )
Theorem	tfrlem1 6361*	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.)
|- ( ph -> A e. On )   &    |- ( ph -> ( Fun F /\ A C_ dom F ) )   &    |- ( ph -> ( Fun G /\ A C_ dom G ) )   &    |- ( ph -> A. x e. A ( F ` x ) = ( B ` ( F |` x ) ) )   &    |- ( ph -> A. x e. A ( G ` x ) = ( B ` ( G |` x ) ) )   =>    |- ( ph -> A. x e. A ( F ` x ) = ( G ` x ) )
Theorem	tfrlem3ag 6362*	Lemma for transfinite recursion. This lemma just changes some bound variables in A for later use. (Contributed by Jim Kingdon, 5-Jul-2019.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- ( G e. _V -> ( G e. A <-> E. z e. On ( G Fn z /\ A. w e. z ( G ` w ) = ( F ` ( G |` w ) ) ) ) )
Theorem	tfrlem3a 6363*	Lemma for transfinite recursion. Let A 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 A for later use. (Contributed by NM, 9-Apr-1995.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   &    |- G e. _V   =>    |- ( G e. A <-> E. z e. On ( G Fn z /\ A. w e. z ( G ` w ) = ( F ` ( G |` w ) ) ) )
Theorem	tfrlem3 6364*	Lemma for transfinite recursion. Let A 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 A for later use. (Contributed by NM, 9-Apr-1995.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- A = { g | E. z e. On ( g Fn z /\ A. w e. z ( g ` w ) = ( F ` ( g |` w ) ) ) }
Theorem	tfrlem3-2d 6365*	Lemma for transfinite recursion which changes a bound variable (Contributed by Jim Kingdon, 2-Jul-2019.)
|- ( ph -> A. x ( Fun F /\ ( F ` x ) e. _V ) )   =>    |- ( ph -> ( Fun F /\ ( F ` g ) e. _V ) )
Theorem	tfrlem4 6366*	Lemma for transfinite recursion. A is the class of all "acceptable" functions, and F is their union. First we show that an acceptable function is in fact a function. (Contributed by NM, 9-Apr-1995.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- ( g e. A -> Fun g )
Theorem	tfrlem5 6367*	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.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- ( ( g e. A /\ h e. A ) -> ( ( x g u /\ x h v ) -> u = v ) )
Theorem	recsfval 6368*	Lemma for transfinite recursion. The definition recs is the union of all acceptable functions. (Contributed by Mario Carneiro, 9-May-2015.)
|- A = { f | E. x e. On ( f Fn x /\ A. y e. x ( f ` y ) = ( F ` ( f |` y ) ) ) }   =>    |- recs ( F ) = U. A
Theorem	tfrlem6 6369*	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 6370*	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 6371*	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 6372*	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 6373	Transfinite recursion produces a function. (Contributed by Jim Kingdon, 20-Aug-2021.)
|- Fun recs ( F )
Theorem	tfr2a 6374	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 6375	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 6376	Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.)
|- F = recs ( G )   =>    |- ( ( G ` (/) ) e. V -> ( F ` (/) ) = ( G ` (/) ) )
Theorem	tfrlemisucfn 6377*	We can extend an acceptable function by one element to produce a function. Lemma for tfrlemi1 6385. (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 6378*	We can extend an acceptable function by one element to produce an acceptable function. Lemma for tfrlemi1 6385. (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 6379*	Each element of B is an acceptable function. Lemma for tfrlemi1 6385. (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 6380*	The union of B is defined on all ordinals. Lemma for tfrlemi1 6385. (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 6381*	The union of B is a function defined on x. Lemma for tfrlemi1 6385. (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 6382*	The set B exists. Lemma for tfrlemi1 6385. (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 6383*	The union of B satisfies the recursion rule (lemma for tfrlemi1 6385). (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 6384*	Lemma for tfrlemi1 6385. (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 6385*	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 6386*	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 6387*	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 6388*	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 6389*	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 6418). 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 6390*	Lemma for transfinite recursion. This lemma changes some bound variables in A (version of tfrlem3ag 6362 but for tfr1on 6403 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 6391*	Lemma for transfinite recursion. This lemma changes some bound variables in A (version of tfrlem3 6364 but for tfr1on 6403 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 6392*	Lemma for tfr1on 6403. The union of functions acceptable for tfr1on 6403 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 6393*	We can extend an acceptable function by one element to produce a function. Lemma for tfr1on 6403. (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 6394*	Lemma for tfr1on 6403. 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 6395*	Lemma for tfr1on 6403. 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 6396*	Lemma for tfr1on 6403. 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 6397*	Lemma for tfr1on 6403. 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 6398*	Lemma for tfr1on 6403. 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 6399*	Lemma for tfr1on 6403. 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 6400*	Lemma for tfr1on 6403. (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 ) ) ) )