xrsupssd

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

Step	Hyp	Ref	Expression
1		xrsupssd.1	$⊢ φ \to B \subseteq C$
2		xrsupssd.2	$⊢ φ \to C \subseteq ℝ^{*}$
3		xrltso	$⊢ < Or ℝ^{*}$
4	3	a1i	$⊢ φ \to < Or ℝ^{*}$
5	1 2	sstrd	$⊢ φ \to B \subseteq ℝ^{*}$
6		xrsupss	$⊢ B \subseteq ℝ^{} \to \exists x \in ℝ^{} (\forall y \in B \neg x < y \land \forall y \in ℝ^{*} (y < x \to \exists z \in B y < z))$
7	5 6	syl	$⊢ φ \to \exists x \in ℝ^{} (\forall y \in B \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in B y < z))$
8		xrsupss	$⊢ C \subseteq ℝ^{} \to \exists x \in ℝ^{} (\forall y \in C \neg x < y \land \forall y \in ℝ^{*} (y < x \to \exists z \in C y < z))$
9	2 8	syl	$⊢ φ \to \exists x \in ℝ^{} (\forall y \in C \neg x < y \land \forall y \in ℝ^{} (y < x \to \exists z \in C y < z))$
10	4 1 2 7 9	supssd	$⊢ φ \to \neg sup (C ℝ^{} <) < sup (B ℝ^{} <)$
11	4 7	supcl	$⊢ φ \to sup (B ℝ^{} <) \in ℝ^{}$
12	4 9	supcl	$⊢ φ \to sup (C ℝ^{} <) \in ℝ^{}$
13		xrlenlt	$⊢ (sup (B ℝ^{} <) \in ℝ^{} \land sup (C ℝ^{} <) \in ℝ^{}) \to (sup (B ℝ^{} <) \leq sup (C ℝ^{} <) \leftrightarrow \neg sup (C ℝ^{} <) < sup (B ℝ^{} <))$
14	11 12 13	syl2anc	$⊢ φ \to (sup (B ℝ^{} <) \leq sup (C ℝ^{} <) \leftrightarrow \neg sup (C ℝ^{} <) < sup (B ℝ^{} <))$
15	10 14	mpbird	$⊢ φ \to sup (B ℝ^{} <) \leq sup (C ℝ^{} <)$

Metamath Proof Explorer