Theorem cnvtrclfv

Description: The converse of the transitive closure is equal to the transitive closure of the converse relation. (Contributed by RP, 19-Jul-2020)

	Ref	Expression
Assertion	cnvtrclfv	|- ( R e. V -> `' ( t+ ` R ) = ( t+ ` `' R ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( R e. V -> R e. _V )
2		nnnn0	|- ( n e. NN -> n e. NN0 )
3		relexpcnv	|- ( ( n e. NN0 /\ R e. _V ) -> `' ( R ^r n ) = ( `' R ^r n ) )
4	2 3	sylan	|- ( ( n e. NN /\ R e. _V ) -> `' ( R ^r n ) = ( `' R ^r n ) )
5	4	expcom	|- ( R e. _V -> ( n e. NN -> `' ( R ^r n ) = ( `' R ^r n ) ) )
6	5	ralrimiv	|- ( R e. _V -> A. n e. NN `' ( R ^r n ) = ( `' R ^r n ) )
7		iuneq2	|- ( A. n e. NN `' ( R ^r n ) = ( `' R ^r n ) -> U_ n e. NN `' ( R ^r n ) = U_ n e. NN ( `' R ^r n ) )
8	6 7	syl	|- ( R e. _V -> U_ n e. NN `' ( R ^r n ) = U_ n e. NN ( `' R ^r n ) )
9		oveq1	|- ( r = R -> ( r ^r n ) = ( R ^r n ) )
10	9	iuneq2d	|- ( r = R -> U_ n e. NN ( r ^r n ) = U_ n e. NN ( R ^r n ) )
11		dftrcl3	|- t+ = ( r e. _V |-> U_ n e. NN ( r ^r n ) )
12		nnex	|- NN e. _V
13		ovex	|- ( R ^r n ) e. _V
14	12 13	iunex	|- U_ n e. NN ( R ^r n ) e. _V
15	10 11 14	fvmpt	|- ( R e. _V -> ( t+ ` R ) = U_ n e. NN ( R ^r n ) )
16	15	cnveqd	|- ( R e. _V -> `' ( t+ ` R ) = `' U_ n e. NN ( R ^r n ) )
17		cnviun	|- `' U_ n e. NN ( R ^r n ) = U_ n e. NN `' ( R ^r n )
18	16 17	eqtrdi	|- ( R e. _V -> `' ( t+ ` R ) = U_ n e. NN `' ( R ^r n ) )
19		cnvexg	|- ( R e. _V -> `' R e. _V )
20		oveq1	|- ( s = `' R -> ( s ^r n ) = ( `' R ^r n ) )
21	20	iuneq2d	|- ( s = `' R -> U_ n e. NN ( s ^r n ) = U_ n e. NN ( `' R ^r n ) )
22		dftrcl3	|- t+ = ( s e. _V |-> U_ n e. NN ( s ^r n ) )
23		ovex	|- ( `' R ^r n ) e. _V
24	12 23	iunex	|- U_ n e. NN ( `' R ^r n ) e. _V
25	21 22 24	fvmpt	|- ( `' R e. _V -> ( t+ ` `' R ) = U_ n e. NN ( `' R ^r n ) )
26	19 25	syl	|- ( R e. _V -> ( t+ ` `' R ) = U_ n e. NN ( `' R ^r n ) )
27	8 18 26	3eqtr4d	|- ( R e. _V -> `' ( t+ ` R ) = ( t+ ` `' R ) )
28	1 27	syl	|- ( R e. V -> `' ( t+ ` R ) = ( t+ ` `' R ) )