Theorem nfwsuc

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

	Ref	Expression
Hypotheses	nfwsuc.1	$$⊢\underset{\_}{Ⅎ}xR$$
	nfwsuc.2	$$⊢\underset{\_}{Ⅎ}xA$$
	nfwsuc.3	$$⊢\underset{\_}{Ⅎ}xX$$
Assertion	nfwsuc	$$⊢\underset{\_}{Ⅎ}xwsuc\left(R,A,X\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfwsuc.1	$$⊢\underset{\_}{Ⅎ}xR$$
2		nfwsuc.2	$$⊢\underset{\_}{Ⅎ}xA$$
3		nfwsuc.3	$$⊢\underset{\_}{Ⅎ}xX$$
4		df-wsuc	$$⊢wsuc\left(R,A,X\right)=inf\left(Pred\left(R^{-1},A,X\right),A,R\right)$$
5	1	nfcnv	$$⊢\underset{\_}{Ⅎ}x{R}^{-1}$$
6	5 2 3	nfpred	$$⊢\underset{\_}{Ⅎ}xPred\left(R^{-1},A,X\right)$$
7	6 2 1	nfinf	$$⊢\underset{\_}{Ⅎ}xinf\left(Pred\left(R^{-1},A,X\right),A,R\right)$$
8	4 7	nfcxfr	$$⊢\underset{\_}{Ⅎ}xwsuc\left(R,A,X\right)$$