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 ⊢ ( 𝐴 ⊆ ℝ* → ( ∀ 𝑤 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 < 𝑤 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑦 ∈ 𝐴 𝑦 ≤ 𝑥 ) )