Theorem ttrcleq

Description: Equality theorem for transitive closure. (Contributed by Scott Fenton, 17-Oct-2024)

	Ref	Expression
Assertion	ttrcleq	|- ( R = S -> t++ R = t++ S )

Proof

Step	Hyp	Ref	Expression
1		breq	|- ( R = S -> ( ( f ` m ) R ( f ` suc m ) <-> ( f ` m ) S ( f ` suc m ) ) )
2	1	ralbidv	|- ( R = S -> ( A. m e. n ( f ` m ) R ( f ` suc m ) <-> A. m e. n ( f ` m ) S ( f ` suc m ) ) )
3	2	3anbi3d	|- ( R = S -> ( ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) <-> ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) S ( f ` suc m ) ) ) )
4	3	exbidv	|- ( R = S -> ( E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) <-> E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) S ( f ` suc m ) ) ) )
5	4	rexbidv	|- ( R = S -> ( E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) <-> E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) S ( f ` suc m ) ) ) )
6	5	opabbidv	|- ( R = S -> { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) } = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) S ( f ` suc m ) ) } )
7		df-ttrcl	|- t++ R = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) R ( f ` suc m ) ) }
8		df-ttrcl	|- t++ S = { <. x , y >. | E. n e. ( _om \ 1o ) E. f ( f Fn suc n /\ ( ( f ` (/) ) = x /\ ( f ` n ) = y ) /\ A. m e. n ( f ` m ) S ( f ` suc m ) ) }
9	6 7 8	3eqtr4g	|- ( R = S -> t++ R = t++ S )