Theorem ttrcleq

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

	Ref	Expression
Assertion	ttrcleq	Could not format assertion : No typesetting found for |- ( R = S -> t++ R = t++ S ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		breq	$$⊢R=S\to \left(f\left(m\right)Rf\left(\mathrm{suc}m\right)\leftrightarrow f\left(m\right)Sf\left(\mathrm{suc}m\right)\right)$$
2	1	ralbidv	$$⊢R=S\to \left(\forall m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)\leftrightarrow \forall m\in nf\left(m\right)Sf\left(\mathrm{suc}m\right)\right)$$
3	2	3anbi3d	$$⊢R=S\to \left(\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)\right)\leftrightarrow \left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Sf\left(\mathrm{suc}m\right)\right)\right)$$
4	3	exbidv	$$⊢R=S\to \left(\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)\right)\leftrightarrow \exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Sf\left(\mathrm{suc}m\right)\right)\right)$$
5	4	rexbidv	$$⊢R=S\to \left(\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)\right)\leftrightarrow \exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Sf\left(\mathrm{suc}m\right)\right)\right)$$
6	5	opabbidv	$$⊢R=S\to \left\{⟨x,y⟩|\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Rf\left(\mathrm{suc}m\right)\right)\right\}=\left\{⟨x,y⟩|\exists n\in \left(\mathrm{\omega }\setminus 1_{𝑜}\right)\exists f\left(fFn\mathrm{suc}n\wedge \left(f\left(\varnothing \right)=x\wedge f\left(n\right)=y\right)\wedge \forall m\in nf\left(m\right)Sf\left(\mathrm{suc}m\right)\right)\right\}$$
7		df-ttrcl	Could not format 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 ) ) } : No typesetting found for |- 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 ) ) } with typecode |-
8		df-ttrcl	Could not format 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 ) ) } : No typesetting found for |- 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 ) ) } with typecode |-
9	6 7 8	3eqtr4g	Could not format ( R = S -> t++ R = t++ S ) : No typesetting found for |- ( R = S -> t++ R = t++ S ) with typecode |-