Theorem xrsupssd

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

	Ref	Expression
Hypotheses	xrsupssd.1	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
	xrsupssd.2	⊢ ( 𝜑 → 𝐶 ⊆ ℝ* )
Assertion	xrsupssd	⊢ ( 𝜑 → sup ( 𝐵 , ℝ* , < ) ≤ sup ( 𝐶 , ℝ* , < ) )

Proof

Step	Hyp	Ref	Expression
1		xrsupssd.1	⊢ ( 𝜑 → 𝐵 ⊆ 𝐶 )
2		xrsupssd.2	⊢ ( 𝜑 → 𝐶 ⊆ ℝ* )
3		xrltso	⊢ < Or ℝ*
4	3	a1i	⊢ ( 𝜑 → < Or ℝ* )
5	1 2	sstrd	⊢ ( 𝜑 → 𝐵 ⊆ ℝ* )
6		xrsupss	⊢ ( 𝐵 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ) ) )
7	5 6	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐵 𝑦 < 𝑧 ) ) )
8		xrsupss	⊢ ( 𝐶 ⊆ ℝ* → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 < 𝑧 ) ) )
9	2 8	syl	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ* ( ∀ 𝑦 ∈ 𝐶 ¬ 𝑥 < 𝑦 ∧ ∀ 𝑦 ∈ ℝ* ( 𝑦 < 𝑥 → ∃ 𝑧 ∈ 𝐶 𝑦 < 𝑧 ) ) )
10	4 1 2 7 9	supssd	⊢ ( 𝜑 → ¬ sup ( 𝐶 , ℝ* , < ) < sup ( 𝐵 , ℝ* , < ) )
11	4 7	supcl	⊢ ( 𝜑 → sup ( 𝐵 , ℝ* , < ) ∈ ℝ* )
12	4 9	supcl	⊢ ( 𝜑 → sup ( 𝐶 , ℝ* , < ) ∈ ℝ* )
13		xrlenlt	⊢ ( ( sup ( 𝐵 , ℝ* , < ) ∈ ℝ* ∧ sup ( 𝐶 , ℝ* , < ) ∈ ℝ* ) → ( sup ( 𝐵 , ℝ* , < ) ≤ sup ( 𝐶 , ℝ* , < ) ↔ ¬ sup ( 𝐶 , ℝ* , < ) < sup ( 𝐵 , ℝ* , < ) ) )
14	11 12 13	syl2anc	⊢ ( 𝜑 → ( sup ( 𝐵 , ℝ* , < ) ≤ sup ( 𝐶 , ℝ* , < ) ↔ ¬ sup ( 𝐶 , ℝ* , < ) < sup ( 𝐵 , ℝ* , < ) ) )
15	10 14	mpbird	⊢ ( 𝜑 → sup ( 𝐵 , ℝ* , < ) ≤ sup ( 𝐶 , ℝ* , < ) )