Metamath Proof Explorer

Theorem infm3

Description: The completeness axiom for reals in terms of infimum: a nonempty, bounded-below set of reals has an infimum. (This theorem is the dual of sup3 .) (Contributed by NM, 14-Jun-2005)

Ref Expression
Assertion infm3 ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y→∃x∈ℝ∀y∈A¬y<x∧∀y∈ℝx<y→∃z∈Az<y

Proof

Step Hyp Ref Expression
1 ssel ⊢A⊆ℝ→v∈A→v∈ℝ
2 1 pm4.71rd ⊢A⊆ℝ→v∈A↔v∈ℝ∧v∈A
3 2 exbidv ⊢A⊆ℝ→∃vv∈A↔∃vv∈ℝ∧v∈A
4 df-rex ⊢∃v∈ℝv∈A↔∃vv∈ℝ∧v∈A
5 renegcl ⊢w∈ℝ→−w∈ℝ
6 infm3lem ⊢v∈ℝ→∃w∈ℝv=−w
7 eleq1 ⊢v=−w→v∈A↔−w∈A
8 5 6 7 rexxfr ⊢∃v∈ℝv∈A↔∃w∈ℝ−w∈A
9 4 8 bitr3i ⊢∃vv∈ℝ∧v∈A↔∃w∈ℝ−w∈A
10 3 9 bitrdi ⊢A⊆ℝ→∃vv∈A↔∃w∈ℝ−w∈A
11 n0 ⊢A≠∅↔∃vv∈A
12 rabn0 ⊢w∈ℝ|−w∈A≠∅↔∃w∈ℝ−w∈A
13 10 11 12 3bitr4g ⊢A⊆ℝ→A≠∅↔w∈ℝ|−w∈A≠∅
14 ssel ⊢A⊆ℝ→y∈A→y∈ℝ
15 14 pm4.71rd ⊢A⊆ℝ→y∈A↔y∈ℝ∧y∈A
16 15 imbi1d ⊢A⊆ℝ→y∈A→x≤y↔y∈ℝ∧y∈A→x≤y
17 impexp ⊢y∈ℝ∧y∈A→x≤y↔y∈ℝ→y∈A→x≤y
18 16 17 bitrdi ⊢A⊆ℝ→y∈A→x≤y↔y∈ℝ→y∈A→x≤y
19 18 albidv ⊢A⊆ℝ→∀yy∈A→x≤y↔∀yy∈ℝ→y∈A→x≤y
20 df-ral ⊢∀y∈Ax≤y↔∀yy∈A→x≤y
21 renegcl ⊢v∈ℝ→−v∈ℝ
22 infm3lem ⊢y∈ℝ→∃v∈ℝy=−v
23 eleq1 ⊢y=−v→y∈A↔−v∈A
24 breq2 ⊢y=−v→x≤y↔x≤−v
25 23 24 imbi12d ⊢y=−v→y∈A→x≤y↔−v∈A→x≤−v
26 21 22 25 ralxfr ⊢∀y∈ℝy∈A→x≤y↔∀v∈ℝ−v∈A→x≤−v
27 df-ral ⊢∀y∈ℝy∈A→x≤y↔∀yy∈ℝ→y∈A→x≤y
28 26 27 bitr3i ⊢∀v∈ℝ−v∈A→x≤−v↔∀yy∈ℝ→y∈A→x≤y
29 19 20 28 3bitr4g ⊢A⊆ℝ→∀y∈Ax≤y↔∀v∈ℝ−v∈A→x≤−v
30 29 rexbidv ⊢A⊆ℝ→∃x∈ℝ∀y∈Ax≤y↔∃x∈ℝ∀v∈ℝ−v∈A→x≤−v
31 renegcl ⊢u∈ℝ→−u∈ℝ
32 infm3lem ⊢x∈ℝ→∃u∈ℝx=−u
33 breq1 ⊢x=−u→x≤−v↔−u≤−v
34 33 imbi2d ⊢x=−u→−v∈A→x≤−v↔−v∈A→−u≤−v
35 34 ralbidv ⊢x=−u→∀v∈ℝ−v∈A→x≤−v↔∀v∈ℝ−v∈A→−u≤−v
36 31 32 35 rexxfr ⊢∃x∈ℝ∀v∈ℝ−v∈A→x≤−v↔∃u∈ℝ∀v∈ℝ−v∈A→−u≤−v
37 negeq ⊢w=v→−w=−v
38 37 eleq1d ⊢w=v→−w∈A↔−v∈A
39 38 elrab ⊢v∈w∈ℝ|−w∈A↔v∈ℝ∧−v∈A
40 39 imbi1i ⊢v∈w∈ℝ|−w∈A→v≤u↔v∈ℝ∧−v∈A→v≤u
41 impexp ⊢v∈ℝ∧−v∈A→v≤u↔v∈ℝ→−v∈A→v≤u
42 40 41 bitri ⊢v∈w∈ℝ|−w∈A→v≤u↔v∈ℝ→−v∈A→v≤u
43 42 albii ⊢∀vv∈w∈ℝ|−w∈A→v≤u↔∀vv∈ℝ→−v∈A→v≤u
44 df-ral ⊢∀v∈w∈ℝ|−w∈Av≤u↔∀vv∈w∈ℝ|−w∈A→v≤u
45 df-ral ⊢∀v∈ℝ−v∈A→v≤u↔∀vv∈ℝ→−v∈A→v≤u
46 43 44 45 3bitr4ri ⊢∀v∈ℝ−v∈A→v≤u↔∀v∈w∈ℝ|−w∈Av≤u
47 leneg ⊢v∈ℝ∧u∈ℝ→v≤u↔−u≤−v
48 47 ancoms ⊢u∈ℝ∧v∈ℝ→v≤u↔−u≤−v
49 48 imbi2d ⊢u∈ℝ∧v∈ℝ→−v∈A→v≤u↔−v∈A→−u≤−v
50 49 ralbidva ⊢u∈ℝ→∀v∈ℝ−v∈A→v≤u↔∀v∈ℝ−v∈A→−u≤−v
51 46 50 bitr3id ⊢u∈ℝ→∀v∈w∈ℝ|−w∈Av≤u↔∀v∈ℝ−v∈A→−u≤−v
52 51 rexbiia ⊢∃u∈ℝ∀v∈w∈ℝ|−w∈Av≤u↔∃u∈ℝ∀v∈ℝ−v∈A→−u≤−v
53 36 52 bitr4i ⊢∃x∈ℝ∀v∈ℝ−v∈A→x≤−v↔∃u∈ℝ∀v∈w∈ℝ|−w∈Av≤u
54 30 53 bitrdi ⊢A⊆ℝ→∃x∈ℝ∀y∈Ax≤y↔∃u∈ℝ∀v∈w∈ℝ|−w∈Av≤u
55 13 54 anbi12d ⊢A⊆ℝ→A≠∅∧∃x∈ℝ∀y∈Ax≤y↔w∈ℝ|−w∈A≠∅∧∃u∈ℝ∀v∈w∈ℝ|−w∈Av≤u
56 ssrab2 ⊢w∈ℝ|−w∈A⊆ℝ
57 sup3 ⊢w∈ℝ|−w∈A⊆ℝ∧w∈ℝ|−w∈A≠∅∧∃u∈ℝ∀v∈w∈ℝ|−w∈Av≤u→∃u∈ℝ∀v∈w∈ℝ|−w∈A¬u<v∧∀v∈ℝv<u→∃t∈w∈ℝ|−w∈Av<t
58 56 57 mp3an1 ⊢w∈ℝ|−w∈A≠∅∧∃u∈ℝ∀v∈w∈ℝ|−w∈Av≤u→∃u∈ℝ∀v∈w∈ℝ|−w∈A¬u<v∧∀v∈ℝv<u→∃t∈w∈ℝ|−w∈Av<t
59 55 58 syl6bi ⊢A⊆ℝ→A≠∅∧∃x∈ℝ∀y∈Ax≤y→∃u∈ℝ∀v∈w∈ℝ|−w∈A¬u<v∧∀v∈ℝv<u→∃t∈w∈ℝ|−w∈Av<t
60 15 imbi1d ⊢A⊆ℝ→y∈A→¬y<x↔y∈ℝ∧y∈A→¬y<x
61 impexp ⊢y∈ℝ∧y∈A→¬y<x↔y∈ℝ→y∈A→¬y<x
62 60 61 bitrdi ⊢A⊆ℝ→y∈A→¬y<x↔y∈ℝ→y∈A→¬y<x
63 62 albidv ⊢A⊆ℝ→∀yy∈A→¬y<x↔∀yy∈ℝ→y∈A→¬y<x
64 df-ral ⊢∀y∈A¬y<x↔∀yy∈A→¬y<x
65 breq1 ⊢y=−v→y<x↔−v<x
66 65 notbid ⊢y=−v→¬y<x↔¬−v<x
67 23 66 imbi12d ⊢y=−v→y∈A→¬y<x↔−v∈A→¬−v<x
68 21 22 67 ralxfr ⊢∀y∈ℝy∈A→¬y<x↔∀v∈ℝ−v∈A→¬−v<x
69 df-ral ⊢∀y∈ℝy∈A→¬y<x↔∀yy∈ℝ→y∈A→¬y<x
70 68 69 bitr3i ⊢∀v∈ℝ−v∈A→¬−v<x↔∀yy∈ℝ→y∈A→¬y<x
71 63 64 70 3bitr4g ⊢A⊆ℝ→∀y∈A¬y<x↔∀v∈ℝ−v∈A→¬−v<x
72 breq2 ⊢y=−v→x<y↔x<−v
73 breq2 ⊢y=−v→z<y↔z<−v
74 73 rexbidv ⊢y=−v→∃z∈Az<y↔∃z∈Az<−v
75 72 74 imbi12d ⊢y=−v→x<y→∃z∈Az<y↔x<−v→∃z∈Az<−v
76 21 22 75 ralxfr ⊢∀y∈ℝx<y→∃z∈Az<y↔∀v∈ℝx<−v→∃z∈Az<−v
77 ssel ⊢A⊆ℝ→z∈A→z∈ℝ
78 77 adantrd ⊢A⊆ℝ→z∈A∧z<−v→z∈ℝ
79 78 pm4.71rd ⊢A⊆ℝ→z∈A∧z<−v↔z∈ℝ∧z∈A∧z<−v
80 79 exbidv ⊢A⊆ℝ→∃zz∈A∧z<−v↔∃zz∈ℝ∧z∈A∧z<−v
81 df-rex ⊢∃z∈Az<−v↔∃zz∈A∧z<−v
82 renegcl ⊢t∈ℝ→−t∈ℝ
83 infm3lem ⊢z∈ℝ→∃t∈ℝz=−t
84 eleq1 ⊢z=−t→z∈A↔−t∈A
85 breq1 ⊢z=−t→z<−v↔−t<−v
86 84 85 anbi12d ⊢z=−t→z∈A∧z<−v↔−t∈A∧−t<−v
87 82 83 86 rexxfr ⊢∃z∈ℝz∈A∧z<−v↔∃t∈ℝ−t∈A∧−t<−v
88 df-rex ⊢∃z∈ℝz∈A∧z<−v↔∃zz∈ℝ∧z∈A∧z<−v
89 87 88 bitr3i ⊢∃t∈ℝ−t∈A∧−t<−v↔∃zz∈ℝ∧z∈A∧z<−v
90 80 81 89 3bitr4g ⊢A⊆ℝ→∃z∈Az<−v↔∃t∈ℝ−t∈A∧−t<−v
91 90 imbi2d ⊢A⊆ℝ→x<−v→∃z∈Az<−v↔x<−v→∃t∈ℝ−t∈A∧−t<−v
92 91 ralbidv ⊢A⊆ℝ→∀v∈ℝx<−v→∃z∈Az<−v↔∀v∈ℝx<−v→∃t∈ℝ−t∈A∧−t<−v
93 76 92 bitrid ⊢A⊆ℝ→∀y∈ℝx<y→∃z∈Az<y↔∀v∈ℝx<−v→∃t∈ℝ−t∈A∧−t<−v
94 71 93 anbi12d ⊢A⊆ℝ→∀y∈A¬y<x∧∀y∈ℝx<y→∃z∈Az<y↔∀v∈ℝ−v∈A→¬−v<x∧∀v∈ℝx<−v→∃t∈ℝ−t∈A∧−t<−v
95 94 rexbidv ⊢A⊆ℝ→∃x∈ℝ∀y∈A¬y<x∧∀y∈ℝx<y→∃z∈Az<y↔∃x∈ℝ∀v∈ℝ−v∈A→¬−v<x∧∀v∈ℝx<−v→∃t∈ℝ−t∈A∧−t<−v
96 breq2 ⊢x=−u→−v<x↔−v<−u
97 96 notbid ⊢x=−u→¬−v<x↔¬−v<−u
98 97 imbi2d ⊢x=−u→−v∈A→¬−v<x↔−v∈A→¬−v<−u
99 98 ralbidv ⊢x=−u→∀v∈ℝ−v∈A→¬−v<x↔∀v∈ℝ−v∈A→¬−v<−u
100 breq1 ⊢x=−u→x<−v↔−u<−v
101 100 imbi1d ⊢x=−u→x<−v→∃t∈ℝ−t∈A∧−t<−v↔−u<−v→∃t∈ℝ−t∈A∧−t<−v
102 101 ralbidv ⊢x=−u→∀v∈ℝx<−v→∃t∈ℝ−t∈A∧−t<−v↔∀v∈ℝ−u<−v→∃t∈ℝ−t∈A∧−t<−v
103 99 102 anbi12d ⊢x=−u→∀v∈ℝ−v∈A→¬−v<x∧∀v∈ℝx<−v→∃t∈ℝ−t∈A∧−t<−v↔∀v∈ℝ−v∈A→¬−v<−u∧∀v∈ℝ−u<−v→∃t∈ℝ−t∈A∧−t<−v
104 31 32 103 rexxfr ⊢∃x∈ℝ∀v∈ℝ−v∈A→¬−v<x∧∀v∈ℝx<−v→∃t∈ℝ−t∈A∧−t<−v↔∃u∈ℝ∀v∈ℝ−v∈A→¬−v<−u∧∀v∈ℝ−u<−v→∃t∈ℝ−t∈A∧−t<−v
105 39 imbi1i ⊢v∈w∈ℝ|−w∈A→¬u<v↔v∈ℝ∧−v∈A→¬u<v
106 impexp ⊢v∈ℝ∧−v∈A→¬u<v↔v∈ℝ→−v∈A→¬u<v
107 105 106 bitri ⊢v∈w∈ℝ|−w∈A→¬u<v↔v∈ℝ→−v∈A→¬u<v
108 107 albii ⊢∀vv∈w∈ℝ|−w∈A→¬u<v↔∀vv∈ℝ→−v∈A→¬u<v
109 df-ral ⊢∀v∈w∈ℝ|−w∈A¬u<v↔∀vv∈w∈ℝ|−w∈A→¬u<v
110 df-ral ⊢∀v∈ℝ−v∈A→¬u<v↔∀vv∈ℝ→−v∈A→¬u<v
111 108 109 110 3bitr4ri ⊢∀v∈ℝ−v∈A→¬u<v↔∀v∈w∈ℝ|−w∈A¬u<v
112 ltneg ⊢u∈ℝ∧v∈ℝ→u<v↔−v<−u
113 112 notbid ⊢u∈ℝ∧v∈ℝ→¬u<v↔¬−v<−u
114 113 imbi2d ⊢u∈ℝ∧v∈ℝ→−v∈A→¬u<v↔−v∈A→¬−v<−u
115 114 ralbidva ⊢u∈ℝ→∀v∈ℝ−v∈A→¬u<v↔∀v∈ℝ−v∈A→¬−v<−u
116 111 115 bitr3id ⊢u∈ℝ→∀v∈w∈ℝ|−w∈A¬u<v↔∀v∈ℝ−v∈A→¬−v<−u
117 ltneg ⊢v∈ℝ∧u∈ℝ→v<u↔−u<−v
118 117 ancoms ⊢u∈ℝ∧v∈ℝ→v<u↔−u<−v
119 negeq ⊢w=t→−w=−t
120 119 eleq1d ⊢w=t→−w∈A↔−t∈A
121 120 rexrab ⊢∃t∈w∈ℝ|−w∈Av<t↔∃t∈ℝ−t∈A∧v<t
122 ltneg ⊢v∈ℝ∧t∈ℝ→v<t↔−t<−v
123 122 anbi2d ⊢v∈ℝ∧t∈ℝ→−t∈A∧v<t↔−t∈A∧−t<−v
124 123 rexbidva ⊢v∈ℝ→∃t∈ℝ−t∈A∧v<t↔∃t∈ℝ−t∈A∧−t<−v
125 121 124 bitrid ⊢v∈ℝ→∃t∈w∈ℝ|−w∈Av<t↔∃t∈ℝ−t∈A∧−t<−v
126 125 adantl ⊢u∈ℝ∧v∈ℝ→∃t∈w∈ℝ|−w∈Av<t↔∃t∈ℝ−t∈A∧−t<−v
127 118 126 imbi12d ⊢u∈ℝ∧v∈ℝ→v<u→∃t∈w∈ℝ|−w∈Av<t↔−u<−v→∃t∈ℝ−t∈A∧−t<−v
128 127 ralbidva ⊢u∈ℝ→∀v∈ℝv<u→∃t∈w∈ℝ|−w∈Av<t↔∀v∈ℝ−u<−v→∃t∈ℝ−t∈A∧−t<−v
129 116 128 anbi12d ⊢u∈ℝ→∀v∈w∈ℝ|−w∈A¬u<v∧∀v∈ℝv<u→∃t∈w∈ℝ|−w∈Av<t↔∀v∈ℝ−v∈A→¬−v<−u∧∀v∈ℝ−u<−v→∃t∈ℝ−t∈A∧−t<−v
130 129 rexbiia ⊢∃u∈ℝ∀v∈w∈ℝ|−w∈A¬u<v∧∀v∈ℝv<u→∃t∈w∈ℝ|−w∈Av<t↔∃u∈ℝ∀v∈ℝ−v∈A→¬−v<−u∧∀v∈ℝ−u<−v→∃t∈ℝ−t∈A∧−t<−v
131 104 130 bitr4i ⊢∃x∈ℝ∀v∈ℝ−v∈A→¬−v<x∧∀v∈ℝx<−v→∃t∈ℝ−t∈A∧−t<−v↔∃u∈ℝ∀v∈w∈ℝ|−w∈A¬u<v∧∀v∈ℝv<u→∃t∈w∈ℝ|−w∈Av<t
132 95 131 bitrdi ⊢A⊆ℝ→∃x∈ℝ∀y∈A¬y<x∧∀y∈ℝx<y→∃z∈Az<y↔∃u∈ℝ∀v∈w∈ℝ|−w∈A¬u<v∧∀v∈ℝv<u→∃t∈w∈ℝ|−w∈Av<t
133 59 132 sylibrd ⊢A⊆ℝ→A≠∅∧∃x∈ℝ∀y∈Ax≤y→∃x∈ℝ∀y∈A¬y<x∧∀y∈ℝx<y→∃z∈Az<y
134 133 3impib ⊢A⊆ℝ∧A≠∅∧∃x∈ℝ∀y∈Ax≤y→∃x∈ℝ∀y∈A¬y<x∧∀y∈ℝx<y→∃z∈Az<y