Metamath Proof Explorer

Theorem lbzbi

Description: If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion lbzbi ⊢A⊆ℝ→∃x∈ℝ∀y∈Ax≤y↔∃x∈ℤ∀y∈Ax≤y

Proof

Step Hyp Ref Expression
1 nfv ⊢ℲxA⊆ℝ
2 nfre1 ⊢Ⅎx∃x∈ℤ∀y∈Ax≤y
3 btwnz ⊢x∈ℝ→∃z∈ℤz<x∧∃z∈ℤx<z
4 3 simpld ⊢x∈ℝ→∃z∈ℤz<x
5 ssel2 ⊢A⊆ℝ∧y∈A→y∈ℝ
6 zre ⊢z∈ℤ→z∈ℝ
7 ltleletr ⊢z∈ℝ∧x∈ℝ∧y∈ℝ→z<x∧x≤y→z≤y
8 6 7 syl3an1 ⊢z∈ℤ∧x∈ℝ∧y∈ℝ→z<x∧x≤y→z≤y
9 8 expd ⊢z∈ℤ∧x∈ℝ∧y∈ℝ→z<x→x≤y→z≤y
10 9 3expia ⊢z∈ℤ∧x∈ℝ→y∈ℝ→z<x→x≤y→z≤y
11 5 10 syl5 ⊢z∈ℤ∧x∈ℝ→A⊆ℝ∧y∈A→z<x→x≤y→z≤y
12 11 expdimp ⊢z∈ℤ∧x∈ℝ∧A⊆ℝ→y∈A→z<x→x≤y→z≤y
13 12 com23 ⊢z∈ℤ∧x∈ℝ∧A⊆ℝ→z<x→y∈A→x≤y→z≤y
14 13 imp ⊢z∈ℤ∧x∈ℝ∧A⊆ℝ∧z<x→y∈A→x≤y→z≤y
15 14 ralrimiv ⊢z∈ℤ∧x∈ℝ∧A⊆ℝ∧z<x→∀y∈Ax≤y→z≤y
16 ralim ⊢∀y∈Ax≤y→z≤y→∀y∈Ax≤y→∀y∈Az≤y
17 15 16 syl ⊢z∈ℤ∧x∈ℝ∧A⊆ℝ∧z<x→∀y∈Ax≤y→∀y∈Az≤y
18 17 ex ⊢z∈ℤ∧x∈ℝ∧A⊆ℝ→z<x→∀y∈Ax≤y→∀y∈Az≤y
19 18 anasss ⊢z∈ℤ∧x∈ℝ∧A⊆ℝ→z<x→∀y∈Ax≤y→∀y∈Az≤y
20 19 expcom ⊢x∈ℝ∧A⊆ℝ→z∈ℤ→z<x→∀y∈Ax≤y→∀y∈Az≤y
21 20 com23 ⊢x∈ℝ∧A⊆ℝ→z<x→z∈ℤ→∀y∈Ax≤y→∀y∈Az≤y
22 21 imp ⊢x∈ℝ∧A⊆ℝ∧z<x→z∈ℤ→∀y∈Ax≤y→∀y∈Az≤y
23 22 imdistand ⊢x∈ℝ∧A⊆ℝ∧z<x→z∈ℤ∧∀y∈Ax≤y→z∈ℤ∧∀y∈Az≤y
24 breq1 ⊢x=z→x≤y↔z≤y
25 24 ralbidv ⊢x=z→∀y∈Ax≤y↔∀y∈Az≤y
26 25 rspcev ⊢z∈ℤ∧∀y∈Az≤y→∃x∈ℤ∀y∈Ax≤y
27 23 26 syl6 ⊢x∈ℝ∧A⊆ℝ∧z<x→z∈ℤ∧∀y∈Ax≤y→∃x∈ℤ∀y∈Ax≤y
28 27 ex ⊢x∈ℝ∧A⊆ℝ→z<x→z∈ℤ∧∀y∈Ax≤y→∃x∈ℤ∀y∈Ax≤y
29 28 com23 ⊢x∈ℝ∧A⊆ℝ→z∈ℤ∧∀y∈Ax≤y→z<x→∃x∈ℤ∀y∈Ax≤y
30 29 ancomsd ⊢x∈ℝ∧A⊆ℝ→∀y∈Ax≤y∧z∈ℤ→z<x→∃x∈ℤ∀y∈Ax≤y
31 30 expdimp ⊢x∈ℝ∧A⊆ℝ∧∀y∈Ax≤y→z∈ℤ→z<x→∃x∈ℤ∀y∈Ax≤y
32 31 rexlimdv ⊢x∈ℝ∧A⊆ℝ∧∀y∈Ax≤y→∃z∈ℤz<x→∃x∈ℤ∀y∈Ax≤y
33 32 anasss ⊢x∈ℝ∧A⊆ℝ∧∀y∈Ax≤y→∃z∈ℤz<x→∃x∈ℤ∀y∈Ax≤y
34 33 expcom ⊢A⊆ℝ∧∀y∈Ax≤y→x∈ℝ→∃z∈ℤz<x→∃x∈ℤ∀y∈Ax≤y
35 4 34 mpdi ⊢A⊆ℝ∧∀y∈Ax≤y→x∈ℝ→∃x∈ℤ∀y∈Ax≤y
36 35 ex ⊢A⊆ℝ→∀y∈Ax≤y→x∈ℝ→∃x∈ℤ∀y∈Ax≤y
37 36 com23 ⊢A⊆ℝ→x∈ℝ→∀y∈Ax≤y→∃x∈ℤ∀y∈Ax≤y
38 1 2 37 rexlimd ⊢A⊆ℝ→∃x∈ℝ∀y∈Ax≤y→∃x∈ℤ∀y∈Ax≤y
39 zssre ⊢ℤ⊆ℝ
40 ssrexv ⊢ℤ⊆ℝ→∃x∈ℤ∀y∈Ax≤y→∃x∈ℝ∀y∈Ax≤y
41 39 40 ax-mp ⊢∃x∈ℤ∀y∈Ax≤y→∃x∈ℝ∀y∈Ax≤y
42 38 41 impbid1 ⊢A⊆ℝ→∃x∈ℝ∀y∈Ax≤y↔∃x∈ℤ∀y∈Ax≤y