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	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → wsuc ( 𝑅 , 𝐴 , 𝑋 ) = wsuc ( 𝑆 , 𝐵 , 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → 𝑅 = 𝑆 )
2	1	cnveqd	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → ◡ 𝑅 = ◡ 𝑆 )
3		predeq123	⊢ ( ( ◡ 𝑅 = ◡ 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) = Pred ( ◡ 𝑆 , 𝐵 , 𝑌 ) )
4	2 3	syld3an1	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) = Pred ( ◡ 𝑆 , 𝐵 , 𝑌 ) )
5		simp2	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → 𝐴 = 𝐵 )
6	4 5 1	infeq123d	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) = inf ( Pred ( ◡ 𝑆 , 𝐵 , 𝑌 ) , 𝐵 , 𝑆 ) )
7		df-wsuc	⊢ wsuc ( 𝑅 , 𝐴 , 𝑋 ) = inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 )
8		df-wsuc	⊢ wsuc ( 𝑆 , 𝐵 , 𝑌 ) = inf ( Pred ( ◡ 𝑆 , 𝐵 , 𝑌 ) , 𝐵 , 𝑆 )
9	6 7 8	3eqtr4g	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑋 = 𝑌 ) → wsuc ( 𝑅 , 𝐴 , 𝑋 ) = wsuc ( 𝑆 , 𝐵 , 𝑌 ) )