Theorem elwlim

Description: Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018) (Revised by AV, 10-Oct-2021)

	Ref	Expression
Assertion	elwlim	⊢ ( 𝑋 ∈ WLim ( 𝑅 , 𝐴 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑋 = sup ( Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		neeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ↔ 𝑋 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ) )
2		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
3		predeq3	⊢ ( 𝑥 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑥 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
4	3	supeq1d	⊢ ( 𝑥 = 𝑋 → sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) = sup ( Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) )
5	2 4	eqeq12d	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) ↔ 𝑋 = sup ( Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) ) )
6	1 5	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) ) ↔ ( 𝑋 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑋 = sup ( Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) ) ) )
7		df-wlim	⊢ WLim ( 𝑅 , 𝐴 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) ) }
8	6 7	elrab2	⊢ ( 𝑋 ∈ WLim ( 𝑅 , 𝐴 ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝑋 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑋 = sup ( Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) ) ) )
9		3anass	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑋 = sup ( Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) ) ↔ ( 𝑋 ∈ 𝐴 ∧ ( 𝑋 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑋 = sup ( Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) ) ) )
10	8 9	bitr4i	⊢ ( 𝑋 ∈ WLim ( 𝑅 , 𝐴 ) ↔ ( 𝑋 ∈ 𝐴 ∧ 𝑋 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑋 = sup ( Pred ( 𝑅 , 𝐴 , 𝑋 ) , 𝐴 , 𝑅 ) ) )