Metamath Proof Explorer

Theorem unb2ltle

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

Ref Expression
Assertion unb2ltle 
|- ( A C_ RR* -> ( A. w e. RR E. y e. A y < w <-> A. x e. RR E. y e. A y <_ x ) )

Proof

Step Hyp Ref Expression
1 nfv 
 |-  F/ w A C_ RR*
2 nfra1 
 |-  F/ w A. w e. RR E. y e. A y < w
3 1 2 nfan 
 |-  F/ w ( A C_ RR* /\ A. w e. RR E. y e. A y < w )
4 simpll 
 |-  ( ( ( A C_ RR* /\ A. w e. RR E. y e. A y < w ) /\ w e. RR ) -> A C_ RR* )
5 simpr 
 |-  ( ( ( A C_ RR* /\ A. w e. RR E. y e. A y < w ) /\ w e. RR ) -> w e. RR )
6 rspa 
 |-  ( ( A. w e. RR E. y e. A y < w /\ w e. RR ) -> E. y e. A y < w )
7 6 adantll 
 |-  ( ( ( A C_ RR* /\ A. w e. RR E. y e. A y < w ) /\ w e. RR ) -> E. y e. A y < w )
8 ssel2 
 |-  ( ( A C_ RR* /\ y e. A ) -> y e. RR* )
9 8 ad4ant13 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y < w ) -> y e. RR* )
10 simpllr 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y < w ) -> w e. RR )
11 10 rexrd 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y < w ) -> w e. RR* )
12 simpr 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y < w ) -> y < w )
13 9 11 12 xrltled 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y < w ) -> y <_ w )
14 13 ex 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) -> ( y < w -> y <_ w ) )
15 14 reximdva 
 |-  ( ( A C_ RR* /\ w e. RR ) -> ( E. y e. A y < w -> E. y e. A y <_ w ) )
16 15 imp 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ E. y e. A y < w ) -> E. y e. A y <_ w )
17 4 5 7 16 syl21anc 
 |-  ( ( ( A C_ RR* /\ A. w e. RR E. y e. A y < w ) /\ w e. RR ) -> E. y e. A y <_ w )
18 3 17 ralrimia 
 |-  ( ( A C_ RR* /\ A. w e. RR E. y e. A y < w ) -> A. w e. RR E. y e. A y <_ w )
19 breq2 
 |-  ( w = x -> ( y <_ w <-> y <_ x ) )
20 19 rexbidv 
 |-  ( w = x -> ( E. y e. A y <_ w <-> E. y e. A y <_ x ) )
21 20 cbvralvw 
 |-  ( A. w e. RR E. y e. A y <_ w <-> A. x e. RR E. y e. A y <_ x )
22 18 21 sylib 
 |-  ( ( A C_ RR* /\ A. w e. RR E. y e. A y < w ) -> A. x e. RR E. y e. A y <_ x )
23 22 ex 
 |-  ( A C_ RR* -> ( A. w e. RR E. y e. A y < w -> A. x e. RR E. y e. A y <_ x ) )
24 simpll 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A y <_ x ) /\ w e. RR ) -> A C_ RR* )
25 simpr 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A y <_ x ) /\ w e. RR ) -> w e. RR )
26 peano2rem 
 |-  ( w e. RR -> ( w - 1 ) e. RR )
27 26 adantl 
 |-  ( ( A. x e. RR E. y e. A y <_ x /\ w e. RR ) -> ( w - 1 ) e. RR )
28 simpl 
 |-  ( ( A. x e. RR E. y e. A y <_ x /\ w e. RR ) -> A. x e. RR E. y e. A y <_ x )
29 breq2 
 |-  ( x = ( w - 1 ) -> ( y <_ x <-> y <_ ( w - 1 ) ) )
30 29 rexbidv 
 |-  ( x = ( w - 1 ) -> ( E. y e. A y <_ x <-> E. y e. A y <_ ( w - 1 ) ) )
31 30 rspcva 
 |-  ( ( ( w - 1 ) e. RR /\ A. x e. RR E. y e. A y <_ x ) -> E. y e. A y <_ ( w - 1 ) )
32 27 28 31 syl2anc 
 |-  ( ( A. x e. RR E. y e. A y <_ x /\ w e. RR ) -> E. y e. A y <_ ( w - 1 ) )
33 32 adantll 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A y <_ x ) /\ w e. RR ) -> E. y e. A y <_ ( w - 1 ) )
34 8 ad4ant13 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y <_ ( w - 1 ) ) -> y e. RR* )
35 simpllr 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y <_ ( w - 1 ) ) -> w e. RR )
36 26 rexrd 
 |-  ( w e. RR -> ( w - 1 ) e. RR* )
37 35 36 syl 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y <_ ( w - 1 ) ) -> ( w - 1 ) e. RR* )
38 35 rexrd 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y <_ ( w - 1 ) ) -> w e. RR* )
39 simpr 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y <_ ( w - 1 ) ) -> y <_ ( w - 1 ) )
40 35 ltm1d 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y <_ ( w - 1 ) ) -> ( w - 1 ) < w )
41 34 37 38 39 40 xrlelttrd 
 |-  ( ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) /\ y <_ ( w - 1 ) ) -> y < w )
42 41 ex 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ y e. A ) -> ( y <_ ( w - 1 ) -> y < w ) )
43 42 reximdva 
 |-  ( ( A C_ RR* /\ w e. RR ) -> ( E. y e. A y <_ ( w - 1 ) -> E. y e. A y < w ) )
44 43 imp 
 |-  ( ( ( A C_ RR* /\ w e. RR ) /\ E. y e. A y <_ ( w - 1 ) ) -> E. y e. A y < w )
45 24 25 33 44 syl21anc 
 |-  ( ( ( A C_ RR* /\ A. x e. RR E. y e. A y <_ x ) /\ w e. RR ) -> E. y e. A y < w )
46 45 ralrimiva 
 |-  ( ( A C_ RR* /\ A. x e. RR E. y e. A y <_ x ) -> A. w e. RR E. y e. A y < w )
47 46 ex 
 |-  ( A C_ RR* -> ( A. x e. RR E. y e. A y <_ x -> A. w e. RR E. y e. A y < w ) )
48 23 47 impbid 
 |-  ( A C_ RR* -> ( A. w e. RR E. y e. A y < w <-> A. x e. RR E. y e. A y <_ x ) )