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	$$⊢\phi \to R\mathrm{Or}A$$
Assertion	wsucex	$$⊢\phi \to wsuc\left(R,A,X\right)\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		wsucex.1	$$⊢\phi \to R\mathrm{Or}A$$
2		df-wsuc	$$⊢wsuc\left(R,A,X\right)=inf\left(Pred\left(R^{-1},A,X\right),A,R\right)$$
3	1	infexd	$$⊢\phi \to inf\left(Pred\left(R^{-1},A,X\right),A,R\right)\in \mathrm{V}$$
4	2 3	eqeltrid	$$⊢\phi \to wsuc\left(R,A,X\right)\in \mathrm{V}$$