supval2

Description: Alternate expression for the supremum. (Contributed by Mario Carneiro, 24-Dec-2016) (Revised by Thierry Arnoux, 24-Sep-2017)

		Ref	Expression
	Hypothesis	supmo.1	$⊢ φ \to R Or A$
	Assertion	supval2	$⊢ φ \to 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)))$

Proof

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		simpl	$⊢ (R Or A \land \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 R Or A$
4		simpr	$⊢ (R Or A \land \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 \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))$
5	3 4	supeu	$⊢ (R Or A \land \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 \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))$
6		riotauni	$⊢ \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))) = ⋃ \{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))\}$
7	5 6	syl	$⊢ (R Or A \land \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))) = ⋃ \{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))\}$
8	2 7	eqtr4id	$⊢ (R Or A \land \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 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)))$
9		rabn0	$⊢ \{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))\} \neq \emptyset \leftrightarrow \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))$
10	9	necon1bbii	$⊢ \neg \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)) \leftrightarrow \{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))\} = \emptyset$
11	10	biimpi	$⊢ \neg \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))\} = \emptyset$
12	11	unieqd	$⊢ \neg \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))\} = ⋃ \emptyset$
13		uni0	$⊢ ⋃ \emptyset = \emptyset$
14	12 13	eqtrdi	$⊢ \neg \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))\} = \emptyset$
15	2 14	syl5eq	$⊢ \neg \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 sup (B, A, R) = \emptyset$
16		reurex	$⊢ \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 \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))$
17		riotaund	$⊢ \neg \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))) = \emptyset$
18	16 17	nsyl5	$⊢ \neg \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))) = \emptyset$
19	15 18	eqtr4d	$⊢ \neg \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 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)))$
20	19	adantl	$⊢ (R Or A \land \neg \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 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)))$
21	8 20	pm2.61dan	$⊢ R Or A \to 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)))$
22	1 21	syl	$⊢ φ \to 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)))$

Metamath Proof Explorer

Theorem supval2

Proof