Metamath Proof Explorer

Theorem supeq2

Description: Equality theorem for supremum. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	supeq2	$⊢ B = C \to sup (A, B, R) = sup (A, C, R)$

Proof

Step	Hyp	Ref	Expression
1		rabeq	$⊢ B = C \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 C \| (\forall y \in A \neg x R y \land \forall y \in B (y R x \to \exists z \in A y R z))\}$
2		raleq	$⊢ B = C \to (\forall y \in B (y R x \to \exists z \in A y R z) \leftrightarrow \forall y \in C (y R x \to \exists z \in A y R z))$
3	2	anbi2d	$⊢ B = C \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 R y \land \forall y \in C (y R x \to \exists z \in A y R z)))$
4	3	rabbidv	$⊢ B = C \to \{x \in C \| (\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 C \| (\forall y \in A \neg x R y \land \forall y \in C (y R x \to \exists z \in A y R z))\}$
5	1 4	eqtrd	$⊢ B = C \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 C \| (\forall y \in A \neg x R y \land \forall y \in C (y R x \to \exists z \in A y R z))\}$
6	5	unieqd	$⊢ B = C \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 C \| (\forall y \in A \neg x R y \land \forall y \in C (y R x \to \exists z \in A y R z))\}$
7		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))\}$
8		df-sup	$⊢ sup (A, C, R) = ⋃ \{x \in C \| (\forall y \in A \neg x R y \land \forall y \in C (y R x \to \exists z \in A y R z))\}$
9	6 7 8	3eqtr4g	$⊢ B = C \to sup (A, B, R) = sup (A, C, R)$