Definition df-wlim

Description: Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018) (Revised by AV, 10-Oct-2021)

	Ref	Expression
Assertion	df-wlim	⊢ WLim ( 𝑅 , 𝐴 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2	1 0	cwlim	⊢ WLim ( 𝑅 , 𝐴 )
3		vx	⊢ 𝑥
4	3	cv	⊢ 𝑥
5	1 1 0	cinf	⊢ inf ( 𝐴 , 𝐴 , 𝑅 )
6	4 5	wne	⊢ 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 )
7	1 0 4	cpred	⊢ Pred ( 𝑅 , 𝐴 , 𝑥 )
8	7 1 0	csup	⊢ sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 )
9	4 8	wceq	⊢ 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 )
10	6 9	wa	⊢ ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) )
11	10 3 1	crab	⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) ) }
12	2 11	wceq	⊢ WLim ( 𝑅 , 𝐴 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) ) }