P. 129 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	swrd2lsw 12801	Extract the last two single symbol from a word. (Contributed by Alexander van der Vekens, 23-Sep-2018.)
|- ( ( W e. Word V /\ 1 < ( # ` W ) ) -> ( W substr <. ( ( # ` W ) - 2 ) , ( # ` W ) >. ) = <" ( W ` ( ( # ` W ) - 2 ) ) ( lastS ` W ) "> )
Theorem	2swrd2eqwrdeq 12802	Two words of length at least 2 are equal if and only if they have the same prefix and the same two single symbols suffix. (Contributed by AV, 24-Sep-2018.) (Revised by Mario Carneiro/AV, 23-Oct-2018.)
|- ( ( W e. Word V /\ U e. Word V /\ 1 < ( # ` W ) ) -> ( W = U <-> ( ( # ` W ) = ( # ` U ) /\ ( ( W substr <. 0 , ( ( # ` W ) - 2 ) >. ) = ( U substr <. 0 , ( ( # ` W ) - 2 ) >. ) /\ ( W ` ( ( # ` W ) - 2 ) ) = ( U ` ( ( # ` W ) - 2 ) ) /\ ( lastS ` W ) = ( lastS ` U ) ) ) ) )
Theorem	ccatw2s1ccatws2 12803	The concatenation of a word with two singleton words equals the concatenation of the word with the doubleton consisting of the symbols of the two singletons. (Contributed by Mario Carneiro/AV, 21-Oct-2018.)
|- ( ( W e. Word V /\ X e. V /\ Y e. V ) -> ( ( W ++ <" X "> ) ++ <" Y "> ) = ( W ++ <" X Y "> ) )
Theorem	ccat2s1fvwALT 12804	Alternate proof of ccat2s1fvw 12551 using words of length 2, see df-s2 12724. A symbol of the concatenation of a word with two single symbols corresponding to the symbol of the word. (Contributed by AV, 22-Sep-2018.) (Proof shortened by Mario Carneiro/AV, 21-Oct-2018.) (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( W e. Word V /\ I e. NN0 /\ I < ( # ` W ) ) /\ ( X e. V /\ Y e. V ) ) -> ( ( ( W ++ <" X "> ) ++ <" Y "> ) ` I ) = ( W ` I ) )
Theorem	wwlktovf 12805*	Lemma 1 for wrd2f1tovbij 12809. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }   &    |- R = { n e. V | { P , n } e. X }   &    |- F = ( t e. D |-> ( t ` 1 ) )   =>    |- F : D --> R
Theorem	wwlktovf1 12806*	Lemma 2 for wrd2f1tovbij 12809. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }   &    |- R = { n e. V | { P , n } e. X }   &    |- F = ( t e. D |-> ( t ` 1 ) )   =>    |- F : D -1-1-> R
Theorem	wwlktovfo 12807*	Lemma 3 for wrd2f1tovbij 12809. (Contributed by Alexander van der Vekens, 27-Jul-2018.)
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }   &    |- R = { n e. V | { P , n } e. X }   &    |- F = ( t e. D |-> ( t ` 1 ) )   =>    |- ( P e. V -> F : D -onto-> R )
Theorem	wwlktovf1o 12808*	Lemma 4 for wrd2f1tovbij 12809. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }   &    |- R = { n e. V | { P , n } e. X }   &    |- F = ( t e. D |-> ( t ` 1 ) )   =>    |- ( P e. V -> F : D -1-1-onto-> R )
Theorem	wrd2f1tovbij 12809*	There is a bijection between words of length two with a fixed first symbol contained in a pair and the symbols contained in a pair together with the fixed symbol. (Contributed by Alexander van der Vekens, 28-Jul-2018.)
|- ( ( V e. Y /\ P e. V ) -> E. f f : { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) } -1-1-onto-> { n e. V | { P , n } e. X } )
5.8  Reflexive and transitive closures of relations A relation, R, has the reflexive property if A R A holds whenever A is an element which could be related by the the relation, namely elements of its domain and range. Eliminating dummy variables we see that a segment of the identity relation must be a subset of the relation or ( _I |` ( ran R u. dom R ) ) C_ R. See issref 5293. A relation, R, has the transitive property if A R C holds whenever there exists an intermediate value B such that both A R B and B R C hold. This can be expressed without dummy variables as ( R o. R ) C_ R. See cotr 5292. The transitive closure of a relation, ( t+ ` R ), is the smallest superset of the relation which has the transitive property. Likewise the reflexive-transitive closure, ( t* ` R ), is the smallest superset which has both the reflexive and transitive properties. Not to be confused with the transitive closure of a set, trcl 8072, which is a closure relative to a different transitive property, df-tr 4461.
5.8.1  The reflexive and transitive properties of relations
Theorem	coss12d 12810	Subset deduction for composition of two classes. (Contributed by RP, 24-Dec-2019.)
|- ( ph -> A C_ B )   &    |- ( ph -> C C_ D )   =>    |- ( ph -> ( A o. C ) C_ ( B o. D ) )
Theorem	trrelssd 12811	The composition of subclasses of a transitive relation is a subclass of that relation. (Contributed by RP, 24-Dec-2019.)
|- ( ph -> ( R o. R ) C_ R )   &    |- ( ph -> S C_ R )   &    |- ( ph -> T C_ R )   =>    |- ( ph -> ( S o. T ) C_ R )
Theorem	xpcogend 12812	The most interesting case of the composition of two cross products. (Contributed by RP, 24-Dec-2019.)
|- ( ph -> ( B i^i C ) =/= (/) )   =>    |- ( ph -> ( ( C X. D ) o. ( A X. B ) ) = ( A X. D ) )
Theorem	xpcoidgend 12813	If two classes are not disjoint, then the composition of their cross-product with itself is idempotent. (Contributed by RP, 24-Dec-2019.)
|- ( ph -> ( A i^i B ) =/= (/) )   =>    |- ( ph -> ( ( A X. B ) o. ( A X. B ) ) = ( A X. B ) )
Theorem	cotr2g 12814*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 12815 for the main application. (Contributed by RP, 22-Mar-2020.)
|- dom B C_ D   &    |- ( ran B i^i dom A ) C_ E   &    |- ran A C_ F   =>    |- ( ( A o. B ) C_ C <-> A. x e. D A. y e. E A. z e. F ( ( x B y /\ y A z ) -> x C z ) )
Theorem	cotr2 12815*	Two ways of saying a relation is transitive. Special instance of cotr2g 12814. (Contributed by RP, 22-Mar-2020.)
|- dom R C_ A   &    |- ( dom R i^i ran R ) C_ B   &    |- ran R C_ C   =>    |- ( ( R o. R ) C_ R <-> A. x e. A A. y e. B A. z e. C ( ( x R y /\ y R z ) -> x R z ) )
Theorem	cotr3 12816*	Two ways of saying a relation is transitive. (Contributed by RP, 22-Mar-2020.)
|- A = dom R   &    |- B = ( A i^i C )   &    |- C = ran R   =>    |- ( ( R o. R ) C_ R <-> A. x e. A A. y e. B A. z e. C ( ( x R y /\ y R z ) -> x R z ) )
Theorem	coemptyd 12817	Deduction about composition of classes with no relational content in common. (Contributed by RP, 24-Dec-2019.)
|- ( ph -> ( dom A i^i ran B ) = (/) )   =>    |- ( ph -> ( A o. B ) = (/) )
Theorem	xptrrel 12818	The cross product is always a transitive relation. (Contributed by RP, 24-Dec-2019.)
|- ( ( A X. B ) o. ( A X. B ) ) C_ ( A X. B )
Theorem	0trrel 12819	The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019.)
|- ( (/) o. (/) ) C_ (/)
5.8.2  Basic properties of closures
Theorem	cleq1lem 12820	Equality implies bijection. (Contributed by RP, 9-May-2020.)
|- ( A = B -> ( ( A C_ C /\ ph ) <-> ( B C_ C /\ ph ) ) )
Theorem	cleq1 12821*	Equality of relations implies equality of closures. (Contributed by RP, 9-May-2020.)
|- ( R = S -> |^| { r | ( R C_ r /\ ph ) } = |^| { r | ( S C_ r /\ ph ) } )
Theorem	clsslem 12822*	The closure of a subclass is a subclass of the closure. (Contributed by RP, 16-May-2020.)
|- ( R C_ S -> |^| { r | ( R C_ r /\ ph ) } C_ |^| { r | ( S C_ r /\ ph ) } )
5.8.3  Definitions and basic properties of transitive closures
Syntax	ctcl 12823	Extend class notation to include the transitive closure symbol.
class t+
Syntax	crtcl 12824	Extend class notation with reflexive-transitive closure.
class t*
Definition	df-trcl 12825*	Transitive closure of a relation. This is the smallest superset which has the transitive property. (Contributed by FL, 27-Jun-2011.)
|- t+ = ( x e. _V |-> |^| { z | ( x C_ z /\ ( z o. z ) C_ z ) } )
Definition	df-rtrcl 12826*	Reflexive-transitive closure of a relation. This is the smallest superset which is reflexive property over all elements of its domain and range and has the transitive property. (Contributed by FL, 27-Jun-2011.)
|- t* = ( x e. _V |-> |^| { z | ( ( _I |` ( dom x u. ran x ) ) C_ z /\ x C_ z /\ ( z o. z ) C_ z ) } )
Theorem	trcleq1 12827*	Equality of relations implies equality of transitive closures. (Contributed by RP, 9-May-2020.)
|- ( R = S -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } = |^| { r | ( S C_ r /\ ( r o. r ) C_ r ) } )
Theorem	trclsslem 12828*	The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.)
|- ( R C_ S -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ |^| { r | ( S C_ r /\ ( r o. r ) C_ r ) } )
Theorem	trcleq2lem 12829	Equality implies bijection. (Contributed by RP, 5-May-2020.)
|- ( A = B -> ( ( R C_ A /\ ( A o. A ) C_ A ) <-> ( R C_ B /\ ( B o. B ) C_ B ) ) )
Theorem	cvbtrcl 12830*	Change of bound variable in class of all transitive relations which are supersets of a relation. (Contributed by RP, 5-May-2020.)
|- { x | ( R C_ x /\ ( x o. x ) C_ x ) } = { y | ( R C_ y /\ ( y o. y ) C_ y ) }
Theorem	trcleq12lem 12831	Equality implies bijection. (Contributed by RP, 9-May-2020.)
|- ( ( R = S /\ A = B ) -> ( ( R C_ A /\ ( A o. A ) C_ A ) <-> ( S C_ B /\ ( B o. B ) C_ B ) ) )
Theorem	trclexlem 12832	Existence of relation implies existence of union with Cartesian product of domain and range. (Contributed by RP, 5-May-2020.)
|- ( R e. V -> ( R u. ( dom R X. ran R ) ) e. _V )
Theorem	trclublem 12833*	If a relation exists then the class of transitive relations which are supersets of that relation is not empty. (Contributed by RP, 28-Apr-2020.)
|- ( R e. V -> ( R u. ( dom R X. ran R ) ) e. { x | ( R C_ x /\ ( x o. x ) C_ x ) } )
Theorem	trclubi 12834*	The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 2-Jan-2020.) (Revised by RP, 28-Apr-2020.)
|- Rel R   &    |- R e. V   =>    |- |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( dom R X. ran R )
Theorem	trclubgi 12835*	The union with the Cartesian product of its domain and range is an upper bound for a set's transitive closure. (Contributed by RP, 3-Jan-2020.) (Revised by RP, 28-Apr-2020.)
|- R e. V   =>    |- |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( R u. ( dom R X. ran R ) )
Theorem	trclub 12836*	The Cartesian product of the domain and range of a relation is an upper bound for its transitive closure. (Contributed by RP, 17-May-2020.)
|- ( ( R e. V /\ Rel R ) -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ ( dom R X. ran R ) )
Theorem	trclubg 12837*	The union with the Cartesian product of its domain and range is an upper bound for a set's transitive closure (as a relation). (Contributed by RP, 17-May-2020.)
|- ( R e. V -> |^| { r | ( R C_ r /\ ( r o. r ) C_ r ) } C_ ( R u. ( dom R X. ran R ) ) )
Theorem	trclfv 12838*	The transitive closure of a relation. (Contributed by RP, 28-Apr-2020.)
|- ( R e. V -> ( t+ ` R ) = |^| { x | ( R C_ x /\ ( x o. x ) C_ x ) } )
Theorem	brintclab 12839*	Two ways to express a binary relation which is the intersection of a class. (Contributed by RP, 4-Apr-2020.)
|- ( A |^| { x | ph } B <-> A. x ( ph -> <. A , B >. e. x ) )
Theorem	brtrclfv 12840*	Two ways of expressing the transitive closure of a binary relation. (Contributed by RP, 9-May-2020.)
|- ( R e. V -> ( A ( t+ ` R ) B <-> A. r ( ( R C_ r /\ ( r o. r ) C_ r ) -> A r B ) ) )
Theorem	brcnvtrclfv 12841*	Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 9-May-2020.)
|- ( ( R e. U /\ A e. V /\ B e. W ) -> ( A `' ( t+ ` R ) B <-> A. r ( ( R C_ r /\ ( r o. r ) C_ r ) -> B r A ) ) )
Theorem	brtrclfvcnv 12842*	Two ways of expressing the transitive closure of the converse of a binary relation. (Contributed by RP, 10-May-2020.)
|- ( R e. V -> ( A ( t+ ` `' R ) B <-> A. r ( ( `' R C_ r /\ ( r o. r ) C_ r ) -> A r B ) ) )
Theorem	brcnvtrclfvcnv 12843*	Two ways of expressing the transitive closure of the converse of the converse of a binary relation. (Contributed by RP, 10-May-2020.)
|- ( ( R e. U /\ A e. V /\ B e. W ) -> ( A `' ( t+ ` `' R ) B <-> A. r ( ( `' R C_ r /\ ( r o. r ) C_ r ) -> B r A ) ) )
Theorem	trclfvss 12844	The transitive closure (as a relation) of a subclass is a subclass of the transitive closure. (Contributed by RP, 3-May-2020.)
|- ( ( R e. V /\ S e. W /\ R C_ S ) -> ( t+ ` R ) C_ ( t+ ` S ) )
Theorem	trclfvub 12845	The transitive closure of a relation has an upper bound. (Contributed by RP, 28-Apr-2020.)
|- ( R e. V -> ( t+ ` R ) C_ ( R u. ( dom R X. ran R ) ) )
Theorem	trclfvlb 12846	The transitive closure of a relation has a lower bound. (Contributed by RP, 28-Apr-2020.)
|- ( R e. V -> R C_ ( t+ ` R ) )
Theorem	trclfvcotr 12847	The transitive closure of a relation is a transitive relation. (Contributed by RP, 29-Apr-2020.)
|- ( R e. V -> ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R ) )
Theorem	trclfvlb2 12848	The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.)
|- ( R e. V -> ( R o. R ) C_ ( t+ ` R ) )
Theorem	trclfvlb3 12849	The transitive closure of a relation has a lower bound. (Contributed by RP, 8-May-2020.)
|- ( R e. V -> ( R u. ( R o. R ) ) C_ ( t+ ` R ) )
Theorem	cotrtrclfv 12850	The transitive closure of a transitive relation. (Contributed by RP, 28-Apr-2020.)
|- ( ( R e. V /\ ( R o. R ) C_ R ) -> ( t+ ` R ) = R )
Theorem	trclidm 12851	The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020.)
|- ( R e. V -> ( t+ ` ( t+ ` R ) ) = ( t+ ` R ) )
Theorem	trclun 12852	Transitive closure of a union of relations. (Contributed by RP, 5-May-2020.)
|- ( ( R e. V /\ S e. W ) -> ( t+ ` ( R u. S ) ) = ( t+ ` ( ( t+ ` R ) u. ( t+ ` S ) ) ) )
Theorem	trclfvg 12853	The value of the transitive closure of a relation is a superset or (for proper classes) the empty set. (Contributed by RP, 8-May-2020.)
|- ( R C_ ( t+ ` R ) \/ ( t+ ` R ) = (/) )
Theorem	trclfvcotrg 12854	The value of the transitive closure of a relation is always a transitive relation. (Contributed by RP, 8-May-2020.)
|- ( ( t+ ` R ) o. ( t+ ` R ) ) C_ ( t+ ` R )
Theorem	reltrclfv 12855	The transitive closure of a relation is a relation. (Contributed by RP, 9-May-2020.)
|- ( ( R e. V /\ Rel R ) -> Rel ( t+ ` R ) )
Theorem	dmtrclfv 12856	The domain of the transitive closure is equal to the domain of the relation. (Contributed by RP, 9-May-2020.)
|- ( R e. V -> dom ( t+ ` R ) = dom R )
5.8.4  Exponentiation of relations
Syntax	crelexp 12857	Extend class notation to include relation exponentiation.
class ^r
Definition	df-relexp 12858*	Definition of repeated composition of a relation with itself, aka relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 22-May-2020.)
|- ^r = ( r e. _V , n e. NN0 |-> if ( n = 0 , ( _I |` ( dom r u. ran r ) ) , ( seq 1 ( ( x e. _V , y e. _V |-> ( x o. r ) ) , ( z e. _V |-> r ) ) ` n ) ) )
Theorem	relexp0g 12859	A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
|- ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
Theorem	relexp0 12860	A relation composed zero times is the (restricted) identity. (Contributed by RP, 22-May-2020.)
|- ( ( R e. V /\ Rel R ) -> ( R ^r 0 ) = ( _I |` U. U. R ) )
Theorem	relexp0d 12861	A relation composed zero times is the (restricted) identity. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> ( R ^r 0 ) = ( _I |` U. U. R ) )
Theorem	relexpsucnnr 12862	A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020.)
|- ( ( R e. V /\ N e. NN ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )
Theorem	relexp1g 12863	A relation composed once is itself. (Contributed by RP, 22-May-2020.)
|- ( R e. V -> ( R ^r 1 ) = R )
Theorem	relexpsucr 12864	A reduction for relation exponentiation to the right. (Contributed by RP, 23-May-2020.)
|- ( ( R e. V /\ Rel R /\ N e. NN0 ) -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) )
Theorem	relexpsucrd 12865	A reduction for relation exponentiation to the right. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> ( N e. NN0 -> ( R ^r ( N + 1 ) ) = ( ( R ^r N ) o. R ) ) )
Theorem	relexp1d 12866	A relation composed once is itself. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> ( R ^r 1 ) = R )
Theorem	relexpsucnnl 12867	A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.)
|- ( ( R e. V /\ N e. NN ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )
Theorem	relexpsucl 12868	A reduction for relation exponentiation to the left. (Contributed by RP, 23-May-2020.)
|- ( ( R e. V /\ Rel R /\ N e. NN0 ) -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) )
Theorem	relexpsucld 12869	A reduction for relation exponentiation to the left. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> ( N e. NN0 -> ( R ^r ( N + 1 ) ) = ( R o. ( R ^r N ) ) ) )
Theorem	relexpcnv 12870	Commutation of converse and relation exponentiation. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN0 /\ R e. V ) -> `' ( R ^r N ) = ( `' R ^r N ) )
Theorem	relexpcnvd 12871	Commutation of converse and relation exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> ( N e. NN0 -> `' ( R ^r N ) = ( `' R ^r N ) ) )
Theorem	relexp0rel 12872	The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020.)
|- ( R e. V -> Rel ( R ^r 0 ) )
Theorem	relexprelg 12873	The exponentiation of a class is a relation except when the exponent is one and the class is not a relation. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN0 /\ R e. V /\ ( N = 1 -> Rel R ) ) -> Rel ( R ^r N ) )
Theorem	relexprel 12874	The exponentiation of a relation is a relation. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN0 /\ R e. V /\ Rel R ) -> Rel ( R ^r N ) )
Theorem	relexpreld 12875	The exponentiation of a relation is a relation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> ( N e. NN0 -> Rel ( R ^r N ) ) )
Theorem	relexpnndm 12876	The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN /\ R e. V ) -> dom ( R ^r N ) C_ dom R )
Theorem	relexpdmg 12877	The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN0 /\ R e. V ) -> dom ( R ^r N ) C_ ( dom R u. ran R ) )
Theorem	relexpdm 12878	The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN0 /\ R e. V ) -> dom ( R ^r N ) C_ U. U. R )
Theorem	relexpdmd 12879	The domain of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> ( N e. NN0 -> dom ( R ^r N ) C_ U. U. R ) )
Theorem	relexpnnrn 12880	The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN /\ R e. V ) -> ran ( R ^r N ) C_ ran R )
Theorem	relexprng 12881	The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN0 /\ R e. V ) -> ran ( R ^r N ) C_ ( dom R u. ran R ) )
Theorem	relexprn 12882	The range of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN0 /\ R e. V ) -> ran ( R ^r N ) C_ U. U. R )
Theorem	relexprnd 12883	The range of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> ( N e. NN0 -> ran ( R ^r N ) C_ U. U. R ) )
Theorem	relexpfld 12884	The field of an exponentiation of a relation a subset of the relation's field. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN0 /\ R e. V ) -> U. U. ( R ^r N ) C_ U. U. R )
Theorem	relexpfldd 12885	The field of an exponentiation of a relation a subset of the relation's field. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> ( N e. NN0 -> U. U. ( R ^r N ) C_ U. U. R ) )
Theorem	relexpaddnn 12886	Relation composition becomes addition under exponentiation. (Contributed by RP, 23-May-2020.)
|- ( ( N e. NN /\ M e. NN /\ R e. V ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
Theorem	relexpuzrel 12887	The exponentiation of a class to an integer not smaller than 2 is a relation. (Contributed by RP, 23-May-2020.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ R e. V ) -> Rel ( R ^r N ) )
Theorem	relexpaddg 12888	Relation composition becomes addition under exponentiation except when the exponents total to one and the class isn't a relation. (Contributed by RP, 30-May-2020.)
|- ( ( N e. NN0 /\ ( M e. NN0 /\ R e. V /\ ( ( N + M ) = 1 -> Rel R ) ) ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) )
Theorem	relexpaddd 12889	Relation composition becomes addition under exponentiation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> ( ( N e. NN0 /\ M e. NN0 ) -> ( ( R ^r N ) o. ( R ^r M ) ) = ( R ^r ( N + M ) ) ) )
5.8.5  Reflexive-transitive closure as an indexed union
Syntax	crtrcl 12890	Extend class notation with recursively defined reflexive, transitive closure.
class t*rec
Definition	df-rtrclrec 12891*	The reflexive, transitive closure of a relation constructed as the union of all finite exponentiations. (Contributed by Drahflow, 12-Nov-2015.)
|- t*rec = ( r e. _V |-> U_ n e. NN0 ( r ^r n ) )
Theorem	dfrtrclrec2 12892*	If two elements are connected by a reflexive, transitive closure, then they are connected via n instances the relation, for some n. (Contributed by Drahflow, 12-Nov-2015.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> ( A ( t*rec ` R ) B <-> E. n e. NN0 A ( R ^r n ) B ) )
Theorem	rtrclreclem1 12893	The reflexive, transitive closure is indeed reflexive. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> ( _I |` U. U. R ) C_ ( t*rec ` R ) )
Theorem	rtrclreclem2 12894	The reflexive, transitive closure is indeed a closure. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> R e. _V )   =>    |- ( ph -> R C_ ( t*rec ` R ) )
Theorem	rtrclreclem3 12895	The reflexive, transitive closure is indeed transitive. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> ( ( t*rec ` R ) o. ( t*rec ` R ) ) C_ ( t*rec ` R ) )
Theorem	rtrclreclem4 12896*	The reflexive, transitive closure of R is the smallest reflexive, transitive relation which contains R and the identity. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> A. s ( ( ( _I |` ( dom R u. ran R ) ) C_ s /\ R C_ s /\ ( s o. s ) C_ s ) -> ( t*rec ` R ) C_ s ) )
Theorem	dfrtrcl2 12897	The two definitions t* and t*rec of the reflexive, transitive closure coincide if R is indeed a relation. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( ph -> Rel R )   &    |- ( ph -> R e. _V )   =>    |- ( ph -> ( t* ` R ) = ( t*rec ` R ) )
5.8.6  Principle of transitive induction. If we have a statement that holds for some element, and a relation between elements that implies if it holds for the first element then it must hold for the second element, the principle of transitive induction shows the statement holds for any element related to the first by the (reflexive-)transitive closure of the relation.
Theorem	relexpindlem 12898*	Principle of transitive induction, finite and non-class version. The first three hypotheses give various existences, the next three give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( et -> Rel R )   &    |- ( et -> R e. _V )   &    |- ( et -> S e. _V )   &    |- ( i = S -> ( ph <-> ch ) )   &    |- ( i = x -> ( ph <-> ps ) )   &    |- ( i = j -> ( ph <-> th ) )   &    |- ( et -> ch )   &    |- ( et -> ( j R x -> ( th -> ps ) ) )   =>    |- ( et -> ( n e. NN0 -> ( S ( R ^r n ) x -> ps ) ) )
Theorem	relexpind 12899*	Principle of transitive induction, finite version. The first three hypotheses give various existences, the next three give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015.) (Revised by RP, 30-May-2020.)
|- ( et -> Rel R )   &    |- ( et -> R e. _V )   &    |- ( et -> S e. _V )   &    |- ( et -> X e. _V )   &    |- ( i = S -> ( ph <-> ch ) )   &    |- ( i = x -> ( ph <-> ps ) )   &    |- ( i = j -> ( ph <-> th ) )   &    |- ( x = X -> ( ps <-> ta ) )   &    |- ( et -> ch )   &    |- ( et -> ( j R x -> ( th -> ps ) ) )   =>    |- ( et -> ( n e. NN0 -> ( S ( R ^r n ) X -> ta ) ) )
Theorem	rtrclind 12900*	Principle of transitive induction. The first four hypotheses give various existences, the next four give necessary substitutions and the last two are the basis and the induction step. (Contributed by Drahflow, 12-Nov-2015.)
|- ( et -> Rel R )   &    |- ( et -> R e. _V )   &    |- ( et -> S e. _V )   &    |- ( et -> X e. _V )   &    |- ( i = S -> ( ph <-> ch ) )   &    |- ( i = x -> ( ph <-> ps ) )   &    |- ( i = j -> ( ph <-> th ) )   &    |- ( x = X -> ( ps <-> ta ) )   &    |- ( et -> ch )   &    |- ( et -> ( j R x -> ( th -> ps ) ) )   =>    |- ( et -> ( S ( t* ` R ) X -> ta ) )