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 ⊢∃x∈ℝ∀y∈Ay≤x→∃x∈ℝ∀y∈z∈ℝ|−z∈Ax≤y

Proof

Step Hyp Ref Expression
1 breq1 ⊢b=y→b≤a↔y≤a
2 1 cbvralvw ⊢∀b∈Ab≤a↔∀y∈Ay≤a
3 2 rexbii ⊢∃a∈ℝ∀b∈Ab≤a↔∃a∈ℝ∀y∈Ay≤a
4 breq2 ⊢a=x→y≤a↔y≤x
5 4 ralbidv ⊢a=x→∀y∈Ay≤a↔∀y∈Ay≤x
6 5 cbvrexvw ⊢∃a∈ℝ∀y∈Ay≤a↔∃x∈ℝ∀y∈Ay≤x
7 3 6 bitri ⊢∃a∈ℝ∀b∈Ab≤a↔∃x∈ℝ∀y∈Ay≤x
8 renegcl ⊢a∈ℝ→−a∈ℝ
9 elrabi ⊢y∈z∈ℝ|−z∈A→y∈ℝ
10 negeq ⊢z=y→−z=−y
11 10 eleq1d ⊢z=y→−z∈A↔−y∈A
12 11 elrab3 ⊢y∈ℝ→y∈z∈ℝ|−z∈A↔−y∈A
13 12 biimpd ⊢y∈ℝ→y∈z∈ℝ|−z∈A→−y∈A
14 9 13 mpcom ⊢y∈z∈ℝ|−z∈A→−y∈A
15 breq1 ⊢b=−y→b≤a↔−y≤a
16 15 rspcv ⊢−y∈A→∀b∈Ab≤a→−y≤a
17 14 16 syl ⊢y∈z∈ℝ|−z∈A→∀b∈Ab≤a→−y≤a
18 17 adantl ⊢a∈ℝ∧y∈z∈ℝ|−z∈A→∀b∈Ab≤a→−y≤a
19 lenegcon1 ⊢a∈ℝ∧y∈ℝ→−a≤y↔−y≤a
20 9 19 sylan2 ⊢a∈ℝ∧y∈z∈ℝ|−z∈A→−a≤y↔−y≤a
21 18 20 sylibrd ⊢a∈ℝ∧y∈z∈ℝ|−z∈A→∀b∈Ab≤a→−a≤y
22 21 ralrimdva ⊢a∈ℝ→∀b∈Ab≤a→∀y∈z∈ℝ|−z∈A−a≤y
23 breq1 ⊢x=−a→x≤y↔−a≤y
24 23 ralbidv ⊢x=−a→∀y∈z∈ℝ|−z∈Ax≤y↔∀y∈z∈ℝ|−z∈A−a≤y
25 24 rspcev ⊢−a∈ℝ∧∀y∈z∈ℝ|−z∈A−a≤y→∃x∈ℝ∀y∈z∈ℝ|−z∈Ax≤y
26 8 22 25 syl6an ⊢a∈ℝ→∀b∈Ab≤a→∃x∈ℝ∀y∈z∈ℝ|−z∈Ax≤y
27 26 rexlimiv ⊢∃a∈ℝ∀b∈Ab≤a→∃x∈ℝ∀y∈z∈ℝ|−z∈Ax≤y
28 7 27 sylbir ⊢∃x∈ℝ∀y∈Ay≤x→∃x∈ℝ∀y∈z∈ℝ|−z∈Ax≤y