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	⊢ ( 𝜑 → 𝑅 We 𝐴 )
	wsuccl.2	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
	wsuccl.3	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	wsuccl.4	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐴 𝑋 𝑅 𝑦 )
Assertion	wsuccl	⊢ ( 𝜑 → wsuc ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		wsuccl.1	⊢ ( 𝜑 → 𝑅 We 𝐴 )
2		wsuccl.2	⊢ ( 𝜑 → 𝑅 Se 𝐴 )
3		wsuccl.3	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
4		wsuccl.4	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐴 𝑋 𝑅 𝑦 )
5		df-wsuc	⊢ wsuc ( 𝑅 , 𝐴 , 𝑋 ) = inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 )
6		weso	⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
7	1 6	syl	⊢ ( 𝜑 → 𝑅 Or 𝐴 )
8	1 2 3 4	wsuclem	⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐴 ( ∀ 𝑏 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) ¬ 𝑏 𝑅 𝑎 ∧ ∀ 𝑏 ∈ 𝐴 ( 𝑎 𝑅 𝑏 → ∃ 𝑐 ∈ Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) 𝑐 𝑅 𝑏 ) ) )
9	7 8	infcl	⊢ ( 𝜑 → inf ( Pred ( ◡ 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) ∈ 𝐴 )
10	5 9	eqeltrid	⊢ ( 𝜑 → wsuc ( 𝑅 , 𝐴 , 𝑋 ) ∈ 𝐴 )