Theorem wlimeq12

Description: Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018) (Proof shortened by AV, 10-Oct-2021)

	Ref	Expression
Assertion	wlimeq12	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → WLim ( 𝑅 , 𝐴 ) = WLim ( 𝑆 , 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
2		simpl	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → 𝑅 = 𝑆 )
3	1 1 2	infeq123d	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → inf ( 𝐴 , 𝐴 , 𝑅 ) = inf ( 𝐵 , 𝐵 , 𝑆 ) )
4	3	neeq2d	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ↔ 𝑥 ≠ inf ( 𝐵 , 𝐵 , 𝑆 ) ) )
5		equid	⊢ 𝑥 = 𝑥
6		predeq123	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ∧ 𝑥 = 𝑥 ) → Pred ( 𝑅 , 𝐴 , 𝑥 ) = Pred ( 𝑆 , 𝐵 , 𝑥 ) )
7	5 6	mp3an3	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → Pred ( 𝑅 , 𝐴 , 𝑥 ) = Pred ( 𝑆 , 𝐵 , 𝑥 ) )
8	7 1 2	supeq123d	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) = sup ( Pred ( 𝑆 , 𝐵 , 𝑥 ) , 𝐵 , 𝑆 ) )
9	8	eqeq2d	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → ( 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) ↔ 𝑥 = sup ( Pred ( 𝑆 , 𝐵 , 𝑥 ) , 𝐵 , 𝑆 ) ) )
10	4 9	anbi12d	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → ( ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) ) ↔ ( 𝑥 ≠ inf ( 𝐵 , 𝐵 , 𝑆 ) ∧ 𝑥 = sup ( Pred ( 𝑆 , 𝐵 , 𝑥 ) , 𝐵 , 𝑆 ) ) ) )
11	1 10	rabeqbidv	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) ) } = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 ≠ inf ( 𝐵 , 𝐵 , 𝑆 ) ∧ 𝑥 = sup ( Pred ( 𝑆 , 𝐵 , 𝑥 ) , 𝐵 , 𝑆 ) ) } )
12		df-wlim	⊢ WLim ( 𝑅 , 𝐴 ) = { 𝑥 ∈ 𝐴 ∣ ( 𝑥 ≠ inf ( 𝐴 , 𝐴 , 𝑅 ) ∧ 𝑥 = sup ( Pred ( 𝑅 , 𝐴 , 𝑥 ) , 𝐴 , 𝑅 ) ) }
13		df-wlim	⊢ WLim ( 𝑆 , 𝐵 ) = { 𝑥 ∈ 𝐵 ∣ ( 𝑥 ≠ inf ( 𝐵 , 𝐵 , 𝑆 ) ∧ 𝑥 = sup ( Pred ( 𝑆 , 𝐵 , 𝑥 ) , 𝐵 , 𝑆 ) ) }
14	11 12 13	3eqtr4g	⊢ ( ( 𝑅 = 𝑆 ∧ 𝐴 = 𝐵 ) → WLim ( 𝑅 , 𝐴 ) = WLim ( 𝑆 , 𝐵 ) )