Theorem wsucex

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

	Ref	Expression
Hypothesis	wsucex.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
Assertion	wsucex	⊢ ( 𝜑 → wsuc ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		wsucex.1	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
2		df-wsuc	⊢ wsuc ( 𝑅 , 𝐴 , 𝑋 ) = inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 )
3	1	infexd	⊢ ( 𝜑 → inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) ∈ V )
4	2 3	eqeltrid	⊢ ( 𝜑 → wsuc ( 𝑅 , 𝐴 , 𝑋 ) ∈ V )