Theorem wsuccl

Description: If X is a set with an R successor in A , then its well-founded successor is a member of A . (Contributed by Scott Fenton, 15-Jun-2018) (Proof shortened by AV, 10-Oct-2021)

	Ref	Expression
Hypotheses	wsuccl.1	$$⊢\phi \to R\mathrm{We}A$$
	wsuccl.2	$$⊢\phi \to R\mathrm{Se}A$$
	wsuccl.3	$$⊢\phi \to X\in V$$
	wsuccl.4	$$⊢\phi \to \exists y\in AXRy$$
Assertion	wsuccl	$$⊢\phi \to wsuc\left(R,A,X\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		wsuccl.1	$$⊢\phi \to R\mathrm{We}A$$
2		wsuccl.2	$$⊢\phi \to R\mathrm{Se}A$$
3		wsuccl.3	$$⊢\phi \to X\in V$$
4		wsuccl.4	$$⊢\phi \to \exists y\in AXRy$$
5		df-wsuc	$$⊢wsuc\left(R,A,X\right)=inf\left(Pred\left(R^{-1},A,X\right),A,R\right)$$
6		weso	$$⊢R\mathrm{We}A\to R\mathrm{Or}A$$
7	1 6	syl	$$⊢\phi \to R\mathrm{Or}A$$
8	1 2 3 4	wsuclem	$$⊢\phi \to \exists a\in A\left(\forall b\in Pred\left(R^{-1},A,X\right)\neg bRa\wedge \forall b\in A\left(aRb\to \exists c\in Pred\left(R^{-1},A,X\right)cRb\right)\right)$$
9	7 8	infcl	$$⊢\phi \to inf\left(Pred\left(R^{-1},A,X\right),A,R\right)\in A$$
10	5 9	eqeltrid	$$⊢\phi \to wsuc\left(R,A,X\right)\in A$$