Metamath Proof Explorer

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 ⊢ R = S ∧ A = B → WLim R A = WLim S B

Proof

Step Hyp Ref Expression
1 simpr ⊢ R = S ∧ A = B → A = B
2 simpl ⊢ R = S ∧ A = B → R = S
3 1 1 2 infeq123d ⊢ R = S ∧ A = B → inf A A R = inf B B S
4 3 neeq2d ⊢ R = S ∧ A = B → x ≠ inf A A R ↔ x ≠ inf B B S
5 equid ⊢ x = x
6 predeq123 ⊢ R = S ∧ A = B ∧ x = x → Pred R A x = Pred S B x
7 5 6 mp3an3 ⊢ R = S ∧ A = B → Pred R A x = Pred S B x
8 7 1 2 supeq123d ⊢ R = S ∧ A = B → sup Pred R A x A R = sup Pred S B x B S
9 8 eqeq2d ⊢ R = S ∧ A = B → x = sup Pred R A x A R ↔ x = sup Pred S B x B S
10 4 9 anbi12d ⊢ R = S ∧ A = B → x ≠ inf A A R ∧ x = sup Pred R A x A R ↔ x ≠ inf B B S ∧ x = sup Pred S B x B S
11 1 10 rabeqbidv ⊢ R = S ∧ A = B → x ∈ A | x ≠ inf A A R ∧ x = sup Pred R A x A R = x ∈ B | x ≠ inf B B S ∧ x = sup Pred S B x B S
12 df-wlim ⊢ WLim R A = x ∈ A | x ≠ inf A A R ∧ x = sup Pred R A x A R
13 df-wlim ⊢ WLim S B = x ∈ B | x ≠ inf B B S ∧ x = sup Pred S B x B S
14 11 12 13 3eqtr4g ⊢ R = S ∧ A = B → WLim R A = WLim S B