Metamath Proof Explorer


Theorem unb2ltle

Description: "Unbounded below" expressed with < and with <_ . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Assertion unb2ltle ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 ) )

Proof

Step Hyp Ref Expression
1 nfv 𝑤 𝐴 ⊆ ℝ*
2 nfra1 𝑤𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤
3 1 2 nfan 𝑤 ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 )
4 simpll ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 ) ∧ 𝑤 ∈ ℝ ) → 𝐴 ⊆ ℝ* )
5 simpr ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 ) ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
6 rspa ( ( ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤𝑤 ∈ ℝ ) → ∃ 𝑦𝐴 𝑦 < 𝑤 )
7 6 adantll ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦𝐴 𝑦 < 𝑤 )
8 ssel2 ( ( 𝐴 ⊆ ℝ*𝑦𝐴 ) → 𝑦 ∈ ℝ* )
9 8 ad4ant13 ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 𝑤 ) → 𝑦 ∈ ℝ* )
10 simpllr ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 𝑤 ) → 𝑤 ∈ ℝ )
11 10 rexrd ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 𝑤 ) → 𝑤 ∈ ℝ* )
12 simpr ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 𝑤 ) → 𝑦 < 𝑤 )
13 9 11 12 xrltled ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 < 𝑤 ) → 𝑦𝑤 )
14 13 ex ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) → ( 𝑦 < 𝑤𝑦𝑤 ) )
15 14 reximdva ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) → ( ∃ 𝑦𝐴 𝑦 < 𝑤 → ∃ 𝑦𝐴 𝑦𝑤 ) )
16 15 imp ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ ∃ 𝑦𝐴 𝑦 < 𝑤 ) → ∃ 𝑦𝐴 𝑦𝑤 )
17 4 5 7 16 syl21anc ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦𝐴 𝑦𝑤 )
18 3 17 ralrimia ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 ) → ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑤 )
19 breq2 ( 𝑤 = 𝑥 → ( 𝑦𝑤𝑦𝑥 ) )
20 19 rexbidv ( 𝑤 = 𝑥 → ( ∃ 𝑦𝐴 𝑦𝑤 ↔ ∃ 𝑦𝐴 𝑦𝑥 ) )
21 20 cbvralvw ( ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑤 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 )
22 18 21 sylib ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 )
23 22 ex ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 → ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 ) )
24 simpll ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 ) ∧ 𝑤 ∈ ℝ ) → 𝐴 ⊆ ℝ* )
25 simpr ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 ) ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
26 peano2rem ( 𝑤 ∈ ℝ → ( 𝑤 − 1 ) ∈ ℝ )
27 26 adantl ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥𝑤 ∈ ℝ ) → ( 𝑤 − 1 ) ∈ ℝ )
28 simpl ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥𝑤 ∈ ℝ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 )
29 breq2 ( 𝑥 = ( 𝑤 − 1 ) → ( 𝑦𝑥𝑦 ≤ ( 𝑤 − 1 ) ) )
30 29 rexbidv ( 𝑥 = ( 𝑤 − 1 ) → ( ∃ 𝑦𝐴 𝑦𝑥 ↔ ∃ 𝑦𝐴 𝑦 ≤ ( 𝑤 − 1 ) ) )
31 30 rspcva ( ( ( 𝑤 − 1 ) ∈ ℝ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 ) → ∃ 𝑦𝐴 𝑦 ≤ ( 𝑤 − 1 ) )
32 27 28 31 syl2anc ( ( ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥𝑤 ∈ ℝ ) → ∃ 𝑦𝐴 𝑦 ≤ ( 𝑤 − 1 ) )
33 32 adantll ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦𝐴 𝑦 ≤ ( 𝑤 − 1 ) )
34 8 ad4ant13 ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → 𝑦 ∈ ℝ* )
35 simpllr ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → 𝑤 ∈ ℝ )
36 26 rexrd ( 𝑤 ∈ ℝ → ( 𝑤 − 1 ) ∈ ℝ* )
37 35 36 syl ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → ( 𝑤 − 1 ) ∈ ℝ* )
38 35 rexrd ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → 𝑤 ∈ ℝ* )
39 simpr ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → 𝑦 ≤ ( 𝑤 − 1 ) )
40 35 ltm1d ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → ( 𝑤 − 1 ) < 𝑤 )
41 34 37 38 39 40 xrlelttrd ( ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) ∧ 𝑦 ≤ ( 𝑤 − 1 ) ) → 𝑦 < 𝑤 )
42 41 ex ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ 𝑦𝐴 ) → ( 𝑦 ≤ ( 𝑤 − 1 ) → 𝑦 < 𝑤 ) )
43 42 reximdva ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) → ( ∃ 𝑦𝐴 𝑦 ≤ ( 𝑤 − 1 ) → ∃ 𝑦𝐴 𝑦 < 𝑤 ) )
44 43 imp ( ( ( 𝐴 ⊆ ℝ*𝑤 ∈ ℝ ) ∧ ∃ 𝑦𝐴 𝑦 ≤ ( 𝑤 − 1 ) ) → ∃ 𝑦𝐴 𝑦 < 𝑤 )
45 24 25 33 44 syl21anc ( ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑦𝐴 𝑦 < 𝑤 )
46 45 ralrimiva ( ( 𝐴 ⊆ ℝ* ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 ) → ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 )
47 46 ex ( 𝐴 ⊆ ℝ* → ( ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 → ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 ) )
48 23 47 impbid ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦𝐴 𝑦 < 𝑤 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦𝐴 𝑦𝑥 ) )