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