Metamath Proof Explorer

Theorem ublbneg

Description: The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion ublbneg ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } 𝑥 ≤ 𝑦 )

Proof

Step Hyp Ref Expression
1 breq1 ⊢ ( 𝑏 = 𝑦 → ( 𝑏 ≤ 𝑎 ↔ 𝑦 ≤ 𝑎 ) )
2 1 cbvralvw ⊢ ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑎 )
3 2 rexbii ⊢ ( ∃ 𝑎 ∈ ℝ ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ↔ ∃ 𝑎 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑎 )
4 breq2 ⊢ ( 𝑎 = 𝑥 → ( 𝑦 ≤ 𝑎 ↔ 𝑦 ≤ 𝑥 ) )
5 4 ralbidv ⊢ ( 𝑎 = 𝑥 → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑎 ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )
6 5 cbvrexvw ⊢ ( ∃ 𝑎 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑎 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
7 3 6 bitri ⊢ ( ∃ 𝑎 ∈ ℝ ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 )
8 renegcl ⊢ ( 𝑎 ∈ ℝ → - 𝑎 ∈ ℝ )
9 elrabi ⊢ ( 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } → 𝑦 ∈ ℝ )
10 negeq ⊢ ( 𝑧 = 𝑦 → - 𝑧 = - 𝑦 )
11 10 eleq1d ⊢ ( 𝑧 = 𝑦 → ( - 𝑧 ∈ 𝐴 ↔ - 𝑦 ∈ 𝐴 ) )
12 11 elrab3 ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ↔ - 𝑦 ∈ 𝐴 ) )
13 12 biimpd ⊢ ( 𝑦 ∈ ℝ → ( 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } → - 𝑦 ∈ 𝐴 ) )
14 9 13 mpcom ⊢ ( 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } → - 𝑦 ∈ 𝐴 )
15 breq1 ⊢ ( 𝑏 = - 𝑦 → ( 𝑏 ≤ 𝑎 ↔ - 𝑦 ≤ 𝑎 ) )
16 15 rspcv ⊢ ( - 𝑦 ∈ 𝐴 → ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 → - 𝑦 ≤ 𝑎 ) )
17 14 16 syl ⊢ ( 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } → ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 → - 𝑦 ≤ 𝑎 ) )
18 17 adantl ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ) → ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 → - 𝑦 ≤ 𝑎 ) )
19 lenegcon1 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( - 𝑎 ≤ 𝑦 ↔ - 𝑦 ≤ 𝑎 ) )
20 9 19 sylan2 ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ) → ( - 𝑎 ≤ 𝑦 ↔ - 𝑦 ≤ 𝑎 ) )
21 18 20 sylibrd ⊢ ( ( 𝑎 ∈ ℝ ∧ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } ) → ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 → - 𝑎 ≤ 𝑦 ) )
22 21 ralrimdva ⊢ ( 𝑎 ∈ ℝ → ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 → ∀ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } - 𝑎 ≤ 𝑦 ) )
23 breq1 ⊢ ( 𝑥 = - 𝑎 → ( 𝑥 ≤ 𝑦 ↔ - 𝑎 ≤ 𝑦 ) )
24 23 ralbidv ⊢ ( 𝑥 = - 𝑎 → ( ∀ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } 𝑥 ≤ 𝑦 ↔ ∀ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } - 𝑎 ≤ 𝑦 ) )
25 24 rspcev ⊢ ( ( - 𝑎 ∈ ℝ ∧ ∀ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } - 𝑎 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } 𝑥 ≤ 𝑦 )
26 8 22 25 syl6an ⊢ ( 𝑎 ∈ ℝ → ( ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } 𝑥 ≤ 𝑦 ) )
27 26 rexlimiv ⊢ ( ∃ 𝑎 ∈ ℝ ∀ 𝑏 ∈ 𝐴 𝑏 ≤ 𝑎 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } 𝑥 ≤ 𝑦 )
28 7 27 sylbir ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } 𝑥 ≤ 𝑦 )