supexd

Description: A supremum is a set. (Contributed by NM, 22-May-1999) (Revised by Mario Carneiro, 24-Dec-2016)

		Ref	Expression
	Hypothesis	supmo.1	$⊢ φ \to R Or A$
	Assertion	supexd	$⊢ φ \to sup (B, A, R) \in V$

Step	Hyp	Ref	Expression
1		supmo.1	$⊢ φ \to R Or A$
2		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))\}$
3	1	supmo	$⊢ φ \to \exists^{*} 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))$
4		rmorabex	$⊢ \exists^{*} 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)) \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$
5		uniexg	$⊢ \{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 \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$
6	3 4 5	3syl	$⊢ φ \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$
7	2 6	eqeltrid	$⊢ φ \to sup (B, A, R) \in V$

Metamath Proof Explorer