supssd

Description: Inequality deduction for supremum of a subset. (Contributed by Thierry Arnoux, 21-Mar-2017)

	Ref	Expression
Hypotheses	supssd.0	$⊢ φ \to R Or A$
	supssd.1	$⊢ φ \to B \subseteq C$
	supssd.2	$⊢ φ \to C \subseteq A$
	supssd.3	$⊢ φ \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))$
	supssd.4	$⊢ φ \to \exists x \in A (\forall y \in C \neg x R y \land \forall y \in A (y R x \to \exists z \in C y R z))$
Assertion	supssd	$⊢ φ \to \neg sup (C, A, R) R sup (B, A, R)$

Step	Hyp	Ref	Expression
1		supssd.0	$⊢ φ \to R Or A$
2		supssd.1	$⊢ φ \to B \subseteq C$
3		supssd.2	$⊢ φ \to C \subseteq A$
4		supssd.3	$⊢ φ \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		supssd.4	$⊢ φ \to \exists x \in A (\forall y \in C \neg x R y \land \forall y \in A (y R x \to \exists z \in C y R z))$
6	1 5	supcl	$⊢ φ \to sup (C, A, R) \in A$
7	2	sseld	$⊢ φ \to (z \in B \to z \in C)$
8	1 5	supub	$⊢ φ \to (z \in C \to \neg sup (C, A, R) R z)$
9	7 8	syld	$⊢ φ \to (z \in B \to \neg sup (C, A, R) R z)$
10	9	ralrimiv	$⊢ φ \to \forall z \in B \neg sup (C, A, R) R z$
11	1 4	supnub	$⊢ φ \to ((sup (C, A, R) \in A \land \forall z \in B \neg sup (C, A, R) R z) \to \neg sup (C, A, R) R sup (B, A, R))$
12	6 10 11	mp2and	$⊢ φ \to \neg sup (C, A, R) R sup (B, A, R)$

Metamath Proof Explorer