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	|- ( ph -> R We A )
	wsuccl.2	|- ( ph -> R Se A )
	wsuccl.3	|- ( ph -> X e. V )
	wsuccl.4	|- ( ph -> E. y e. A X R y )
Assertion	wsuccl	|- ( ph -> wsuc ( R , A , X ) e. A )

Proof

Step	Hyp	Ref	Expression
1		wsuccl.1	|- ( ph -> R We A )
2		wsuccl.2	|- ( ph -> R Se A )
3		wsuccl.3	|- ( ph -> X e. V )
4		wsuccl.4	|- ( ph -> E. y e. A X R y )
5		df-wsuc	|- wsuc ( R , A , X ) = inf ( Pred ( `' R , A , X ) , A , R )
6		weso	|- ( R We A -> R Or A )
7	1 6	syl	|- ( ph -> R Or A )
8	1 2 3 4	wsuclem	|- ( ph -> E. a e. A ( A. b e. Pred ( `' R , A , X ) -. b R a /\ A. b e. A ( a R b -> E. c e. Pred ( `' R , A , X ) c R b ) ) )
9	7 8	infcl	|- ( ph -> inf ( Pred ( `' R , A , X ) , A , R ) e. A )
10	5 9	eqeltrid	|- ( ph -> wsuc ( R , A , X ) e. A )