This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )