Theorem wsuceq123

Description: Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018) (Proof shortened by AV, 10-Oct-2021)

	Ref	Expression
Assertion	wsuceq123	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to wsuc\left(R,A,X\right)=wsuc\left(S,B,Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to R=S$$
2	1	cnveqd	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to R^{-1}=S^{-1}$$
3		predeq123	$$⊢\left(R^{-1}=S^{-1}\wedge A=B\wedge X=Y\right)\to Pred\left(R^{-1},A,X\right)=Pred\left(S^{-1},B,Y\right)$$
4	2 3	syld3an1	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to Pred\left(R^{-1},A,X\right)=Pred\left(S^{-1},B,Y\right)$$
5		simp2	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to A=B$$
6	4 5 1	infeq123d	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to inf\left(Pred\left(R^{-1},A,X\right),A,R\right)=inf\left(Pred\left(S^{-1},B,Y\right),B,S\right)$$
7		df-wsuc	$$⊢wsuc\left(R,A,X\right)=inf\left(Pred\left(R^{-1},A,X\right),A,R\right)$$
8		df-wsuc	$$⊢wsuc\left(S,B,Y\right)=inf\left(Pred\left(S^{-1},B,Y\right),B,S\right)$$
9	6 7 8	3eqtr4g	$$⊢\left(R=S\wedge A=B\wedge X=Y\right)\to wsuc\left(R,A,X\right)=wsuc\left(S,B,Y\right)$$