This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem supeq3

Description: Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018)

		Ref	Expression
	Assertion	supeq3	$⊢ R = S \to sup (A, B, R) = sup (A, B, S)$

Proof

Step	Hyp	Ref	Expression
1		breq	$⊢ R = S \to (x R y \leftrightarrow x S y)$
2	1	notbid	$⊢ R = S \to (\neg x R y \leftrightarrow \neg x S y)$
3	2	ralbidv	$⊢ R = S \to (\forall y \in A \neg x R y \leftrightarrow \forall y \in A \neg x S y)$
4		breq	$⊢ R = S \to (y R x \leftrightarrow y S x)$
5		breq	$⊢ R = S \to (y R z \leftrightarrow y S z)$
6	5	rexbidv	$⊢ R = S \to (\exists z \in A y R z \leftrightarrow \exists z \in A y S z)$
7	4 6	imbi12d	$⊢ R = S \to ((y R x \to \exists z \in A y R z) \leftrightarrow (y S x \to \exists z \in A y S z))$
8	7	ralbidv	$⊢ R = S \to (\forall y \in B (y R x \to \exists z \in A y R z) \leftrightarrow \forall y \in B (y S x \to \exists z \in A y S z))$
9	3 8	anbi12d	$⊢ R = S \to ((\forall y \in A \neg x R y \land \forall y \in B (y R x \to \exists z \in A y R z)) \leftrightarrow (\forall y \in A \neg x S y \land \forall y \in B (y S x \to \exists z \in A y S z)))$
10	9	rabbidv	$⊢ R = S \to \{x \in B \| (\forall y \in A \neg x R y \land \forall y \in B (y R x \to \exists z \in A y R z))\} = \{x \in B \| (\forall y \in A \neg x S y \land \forall y \in B (y S x \to \exists z \in A y S z))\}$
11	10	unieqd	$⊢ R = S \to ⋃ \{x \in B \| (\forall y \in A \neg x R y \land \forall y \in B (y R x \to \exists z \in A y R z))\} = ⋃ \{x \in B \| (\forall y \in A \neg x S y \land \forall y \in B (y S x \to \exists z \in A y S z))\}$
12		df-sup	$⊢ sup (A, B, R) = ⋃ \{x \in B \| (\forall y \in A \neg x R y \land \forall y \in B (y R x \to \exists z \in A y R z))\}$
13		df-sup	$⊢ sup (A, B, S) = ⋃ \{x \in B \| (\forall y \in A \neg x S y \land \forall y \in B (y S x \to \exists z \in A y S z))\}$
14	11 12 13	3eqtr4g	$⊢ R = S \to sup (A, B, R) = sup (A, B, S)$