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 ( ∃ 𝑥 ∈ ℝ ∀ 𝑦𝐴 𝑦𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ { 𝑧 ∈ ℝ ∣ - 𝑧𝐴 } 𝑥𝑦 )