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 \land A = B) \to WLim (R, A) = WLim (S, B)$

Step	Hyp	Ref	Expression
1		simpr	$⊢ (R = S \land A = B) \to A = B$
2		simpl	$⊢ (R = S \land A = B) \to R = S$
3	1 1 2	infeq123d	$⊢ (R = S \land A = B) \to sup (A, A, R) = sup (B, B, S)$
4	3	neeq2d	$⊢ (R = S \land A = B) \to (x \neq sup (A, A, R) \leftrightarrow x \neq sup (B, B, S))$
5		equid	$⊢ x = x$
6		predeq123	$⊢ (R = S \land A = B \land x = x) \to Pred (R, A, x) = Pred (S, B, x)$
7	5 6	mp3an3	$⊢ (R = S \land A = B) \to Pred (R, A, x) = Pred (S, B, x)$
8	7 1 2	supeq123d	$⊢ (R = S \land A = B) \to sup (Pred (R, A, x), A, R) = sup (Pred (S, B, x), B, S)$
9	8	eqeq2d	$⊢ (R = S \land A = B) \to (x = sup (Pred (R, A, x), A, R) \leftrightarrow x = sup (Pred (S, B, x), B, S))$
10	4 9	anbi12d	$⊢ (R = S \land A = B) \to ((x \neq sup (A, A, R) \land x = sup (Pred (R, A, x), A, R)) \leftrightarrow (x \neq sup (B, B, S) \land x = sup (Pred (S, B, x), B, S)))$
11	1 10	rabeqbidv	$⊢ (R = S \land A = B) \to \{x \in A \| (x \neq sup (A, A, R) \land x = sup (Pred (R, A, x), A, R))\} = \{x \in B \| (x \neq sup (B, B, S) \land x = sup (Pred (S, B, x), B, S))\}$
12		df-wlim	$⊢ WLim (R, A) = \{x \in A \| (x \neq sup (A, A, R) \land x = sup (Pred (R, A, x), A, R))\}$
13		df-wlim	$⊢ WLim (S, B) = \{x \in B \| (x \neq sup (B, B, S) \land x = sup (Pred (S, B, x), B, S))\}$
14	11 12 13	3eqtr4g	$⊢ (R = S \land A = B) \to WLim (R, A) = WLim (S, B)$

Metamath Proof Explorer