This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝐶 , ℝ* , < ) )