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 ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )

Proof

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