Metamath Proof Explorer

Theorem unb2ltle

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

Ref Expression
Assertion unb2ltle ⊢A⊆ℝ*→∀w∈ℝ∃y∈Ay<w↔∀x∈ℝ∃y∈Ay≤x

Proof

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