P. 138 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 13701-13800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	wwlktovfo 13701*	Lemma 3 for wrd2f1tovbij 13703. (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 13702*	Lemma 4 for wrd2f1tovbij 13703. (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 13703*	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 } )
Theorem	eqwrds3 13704	A word is equal with a length 3 string iff it has length 3 and the same symbol at each position. (Contributed by AV, 12-May-2021.)
|- ( ( W e. Word V /\ ( A e. V /\ B e. V /\ C e. V ) ) -> ( W = <" A B C "> <-> ( ( # ` W ) = 3 /\ ( ( W ` 0 ) = A /\ ( W ` 1 ) = B /\ ( W ` 2 ) = C ) ) ) )
Theorem	wrdl3s3 13705*	A word of length 3 is a length 3 string. (Contributed by AV, 18-May-2021.)
|- ( ( W e. Word V /\ ( # ` W ) = 3 ) <-> E. a e. V E. b e. V E. c e. V W = <" a b c "> )
Theorem	s3sndisj 13706*	The singletons consisting of length 3 strings which have distinct third symbols are disjunct. (Contributed by AV, 17-May-2021.)
|- ( ( A e. X /\ B e. Y ) -> Disj c e. Z { <" A B c "> } )
Theorem	s3iunsndisj 13707*	The union of singletons consisting of length 3 strings which have distinct first and third symbols are disjunct. (Contributed by AV, 17-May-2021.)
|- ( B e. X -> Disj a e. Y U_ c e. ( Z \ { a } ) { <" a B c "> } )
Theorem	ofccat 13708	Letterwise operations on word concatenations. (Contributed by Thierry Arnoux, 28-Sep-2018.)
|- ( ph -> E e. Word S )   &    |- ( ph -> F e. Word S )   &    |- ( ph -> G e. Word T )   &    |- ( ph -> H e. Word T )   &    |- ( ph -> ( # ` E ) = ( # ` G ) )   &    |- ( ph -> ( # ` F ) = ( # ` H ) )   =>    |- ( ph -> ( ( E ++ F ) oF R ( G ++ H ) ) = ( ( E oF R G ) ++ ( F oF R H ) ) )
Theorem	ofs1 13709	Letterwise operations on a single letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
|- ( ( A e. S /\ B e. T ) -> ( <" A "> oF R <" B "> ) = <" ( A R B ) "> )
Theorem	ofs2 13710	Letterwise operations on a double letter word. (Contributed by Thierry Arnoux, 7-Oct-2018.)
|- ( ( ( A e. S /\ B e. S ) /\ ( C e. T /\ D e. T ) ) -> ( <" A B "> oF R <" C D "> ) = <" ( A R C ) ( B R D ) "> )
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 5509. 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 5508. 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 8604, which is a closure relative to a different transitive property, df-tr 4753.
5.8.1  The reflexive and transitive properties of relations
Theorem	coss12d 13711	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 13712	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 13713	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 13714	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 13715*	Two ways of saying that the composition of two relations is included in a third relation. See its special instance cotr2 13716 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 13716*	Two ways of saying a relation is transitive. Special instance of cotr2g 13715. (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 13717*	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 13718	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 13719	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 13720	The empty class is a transitive relation. (Contributed by RP, 24-Dec-2019.)
|- ( (/) o. (/) ) C_ (/)
5.8.2  Basic properties of closures
Theorem	cleq1lem 13721	Equality implies bijection. (Contributed by RP, 9-May-2020.)
|- ( A = B -> ( ( A C_ C /\ ph ) <-> ( B C_ C /\ ph ) ) )
Theorem	cleq1 13722*	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 13723*	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 13724	Extend class notation to include the transitive closure symbol.
class t+
Syntax	crtcl 13725	Extend class notation with reflexive-transitive closure.
class t*
Definition	df-trcl 13726*	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 13727*	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 13728*	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 13729*	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 13730	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 13731*	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 13732	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 13733	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 13734*	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 13735*	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.) (Revised by AV, 26-Mar-2021.)
|- Rel R   &    |- R e. _V   =>    |- |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( dom R X. ran R )
Theorem	trclubiOLD 13736*	Obsolete version of trclubi 13735 as of 26-Mar-2021. (Contributed by RP, 2-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- Rel R   &    |- R e. V   =>    |- |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( dom R X. ran R )
Theorem	trclubgi 13737*	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.) (Revised by AV, 26-Mar-2021.)
|- R e. _V   =>    |- |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( R u. ( dom R X. ran R ) )
Theorem	trclubgiOLD 13738*	Obsolete version of trclubgi 13737 as of 26-Mar-2021. (Contributed by RP, 3-Jan-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
|- R e. V   =>    |- |^| { s | ( R C_ s /\ ( s o. s ) C_ s ) } C_ ( R u. ( dom R X. ran R ) )
Theorem	trclub 13739*	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 13740*	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 13741*	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 13742*	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 13743*	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 13744*	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 13745*	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 13746*	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 13747	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 13748	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 13749	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 13750	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 13751	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 13752	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 13753	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 13754	The transitive closure of a relation is idempotent. (Contributed by RP, 29-Apr-2020.)
|- ( R e. V -> ( t+ ` ( t+ ` R ) ) = ( t+ ` R ) )
Theorem	trclun 13755	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 13756	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 13757	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 13758	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 13759	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 13760	Extend class notation to include relation exponentiation.
class ^r
Definition	df-relexp 13761*	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 13762	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 13763	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 13764	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 13765	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 13766	A relation composed once is itself. (Contributed by RP, 22-May-2020.)
|- ( R e. V -> ( R ^r 1 ) = R )
Theorem	dfid5 13767	Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020.)
|- _I = ( x e. _V |-> ( x ^r 1 ) )
Theorem	dfid6 13768*	Identity relation expressed as indexed union of relational powers. (Contributed by RP, 9-Jun-2020.)
|- _I = ( x e. _V |-> U_ n e. { 1 } ( x ^r n ) )
Theorem	relexpsucr 13769	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 13770	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 13771	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 13772	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 13773	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 13774	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 13775	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 13776	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 13777	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 13778	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 13779	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 13780	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 13781	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 13782	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 13783	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 13784	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 13785	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 13786	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 13787	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 13788	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 13789	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 13790	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 13791	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 13792	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 13793	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 13794	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 13795	Extend class notation with recursively defined reflexive, transitive closure.
class t*rec
Definition	df-rtrclrec 13796*	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 13797*	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 13798	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 13799	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 13800	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 ) )