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