supex2g

Description: Existence of supremum. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	supex2g	$⊢ A \in C \to sup (B, A, R) \in V$

Step	Hyp	Ref	Expression
1		df-sup	$⊢ sup (B, A, R) = ⋃ \{x \in A \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\}$
2		rabexg	$⊢ A \in C \to \{x \in A \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} \in V$
3	2	uniexd	$⊢ A \in C \to ⋃ \{x \in A \| (\forall y \in B \neg x R y \land \forall y \in A (y R x \to \exists z \in B y R z))\} \in V$
4	1 3	eqeltrid	$⊢ A \in C \to sup (B, A, R) \in V$

Metamath Proof Explorer