Metamath Proof Explorer

Theorem xrinfmsslem

Description: Lemma for xrinfmss . (Contributed by NM, 19-Jan-2006)

Ref Expression
Assertion xrinfmsslem 
|- ( ( A C_ RR* /\ ( A C_ RR \/ -oo e. A ) ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )

Proof

Step Hyp Ref Expression
1 raleq 
 |-  ( A = (/) -> ( A. y e. A -. y < x <-> A. y e. (/) -. y < x ) )
2 rexeq 
 |-  ( A = (/) -> ( E. z e. A z < y <-> E. z e. (/) z < y ) )
3 2 imbi2d 
 |-  ( A = (/) -> ( ( x < y -> E. z e. A z < y ) <-> ( x < y -> E. z e. (/) z < y ) ) )
4 3 ralbidv 
 |-  ( A = (/) -> ( A. y e. RR* ( x < y -> E. z e. A z < y ) <-> A. y e. RR* ( x < y -> E. z e. (/) z < y ) ) )
5 1 4 anbi12d 
 |-  ( A = (/) -> ( ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) <-> ( A. y e. (/) -. y < x /\ A. y e. RR* ( x < y -> E. z e. (/) z < y ) ) ) )
6 5 rexbidv 
 |-  ( A = (/) -> ( E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) <-> E. x e. RR* ( A. y e. (/) -. y < x /\ A. y e. RR* ( x < y -> E. z e. (/) z < y ) ) ) )
7 infm3 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )
8 rexr 
 |-  ( x e. RR -> x e. RR* )
9 8 anim1i 
 |-  ( ( x e. RR /\ ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) ) -> ( x e. RR* /\ ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) ) )
10 9 reximi2 
 |-  ( E. x e. RR ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )
11 7 10 syl 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) )
12 elxr 
 |-  ( y e. RR* <-> ( y e. RR \/ y = +oo \/ y = -oo ) )
13 simpr 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) /\ ( y e. RR -> ( x < y -> E. z e. A z < y ) ) ) -> ( y e. RR -> ( x < y -> E. z e. A z < y ) ) )
14 ssel 
 |-  ( A C_ RR -> ( z e. A -> z e. RR ) )
15 ltpnf 
 |-  ( z e. RR -> z < +oo )
16 14 15 syl6 
 |-  ( A C_ RR -> ( z e. A -> z < +oo ) )
17 16 ancld 
 |-  ( A C_ RR -> ( z e. A -> ( z e. A /\ z < +oo ) ) )
18 17 eximdv 
 |-  ( A C_ RR -> ( E. z z e. A -> E. z ( z e. A /\ z < +oo ) ) )
19 n0 
 |-  ( A =/= (/) <-> E. z z e. A )
20 df-rex 
 |-  ( E. z e. A z < +oo <-> E. z ( z e. A /\ z < +oo ) )
21 18 19 20 3imtr4g 
 |-  ( A C_ RR -> ( A =/= (/) -> E. z e. A z < +oo ) )
22 21 imp 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> E. z e. A z < +oo )
23 22 a1d 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( x < +oo -> E. z e. A z < +oo ) )
24 23 ad2antrr 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) /\ y = +oo ) -> ( x < +oo -> E. z e. A z < +oo ) )
25 breq2 
 |-  ( y = +oo -> ( x < y <-> x < +oo ) )
26 breq2 
 |-  ( y = +oo -> ( z < y <-> z < +oo ) )
27 26 rexbidv 
 |-  ( y = +oo -> ( E. z e. A z < y <-> E. z e. A z < +oo ) )
28 25 27 imbi12d 
 |-  ( y = +oo -> ( ( x < y -> E. z e. A z < y ) <-> ( x < +oo -> E. z e. A z < +oo ) ) )
29 28 adantl 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) /\ y = +oo ) -> ( ( x < y -> E. z e. A z < y ) <-> ( x < +oo -> E. z e. A z < +oo ) ) )
30 24 29 mpbird 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) /\ y = +oo ) -> ( x < y -> E. z e. A z < y ) )
31 30 ex 
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) -> ( y = +oo -> ( x < y -> E. z e. A z < y ) ) )
32 31 adantr 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) /\ ( y e. RR -> ( x < y -> E. z e. A z < y ) ) ) -> ( y = +oo -> ( x < y -> E. z e. A z < y ) ) )
33 nltmnf 
 |-  ( x e. RR* -> -. x < -oo )
34 33 adantr 
 |-  ( ( x e. RR* /\ y = -oo ) -> -. x < -oo )
35 breq2 
 |-  ( y = -oo -> ( x < y <-> x < -oo ) )
36 35 notbid 
 |-  ( y = -oo -> ( -. x < y <-> -. x < -oo ) )
37 36 adantl 
 |-  ( ( x e. RR* /\ y = -oo ) -> ( -. x < y <-> -. x < -oo ) )
38 34 37 mpbird 
 |-  ( ( x e. RR* /\ y = -oo ) -> -. x < y )
39 38 pm2.21d 
 |-  ( ( x e. RR* /\ y = -oo ) -> ( x < y -> E. z e. A z < y ) )
40 39 ex 
 |-  ( x e. RR* -> ( y = -oo -> ( x < y -> E. z e. A z < y ) ) )
41 40 ad2antlr 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) /\ ( y e. RR -> ( x < y -> E. z e. A z < y ) ) ) -> ( y = -oo -> ( x < y -> E. z e. A z < y ) ) )
42 13 32 41 3jaod 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) /\ ( y e. RR -> ( x < y -> E. z e. A z < y ) ) ) -> ( ( y e. RR \/ y = +oo \/ y = -oo ) -> ( x < y -> E. z e. A z < y ) ) )
43 12 42 syl5bi 
 |-  ( ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) /\ ( y e. RR -> ( x < y -> E. z e. A z < y ) ) ) -> ( y e. RR* -> ( x < y -> E. z e. A z < y ) ) )
44 43 ex 
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) -> ( ( y e. RR -> ( x < y -> E. z e. A z < y ) ) -> ( y e. RR* -> ( x < y -> E. z e. A z < y ) ) ) )
45 44 ralimdv2 
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) -> ( A. y e. RR ( x < y -> E. z e. A z < y ) -> A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
46 45 anim2d 
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ x e. RR* ) -> ( ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) -> ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) )
47 46 reximdva 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> ( E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) )
48 47 3adant3 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> ( E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR ( x < y -> E. z e. A z < y ) ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) )
49 11 48 mpd 
 |-  ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A x <_ y ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
50 49 3expa 
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ E. x e. RR A. y e. A x <_ y ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
51 ralnex 
 |-  ( A. x e. RR -. A. y e. A x <_ y <-> -. E. x e. RR A. y e. A x <_ y )
52 rexnal 
 |-  ( E. y e. A -. x <_ y <-> -. A. y e. A x <_ y )
53 ssel2 
 |-  ( ( A C_ RR /\ y e. A ) -> y e. RR )
54 letric 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x <_ y \/ y <_ x ) )
55 54 ancoms 
 |-  ( ( y e. RR /\ x e. RR ) -> ( x <_ y \/ y <_ x ) )
56 55 ord 
 |-  ( ( y e. RR /\ x e. RR ) -> ( -. x <_ y -> y <_ x ) )
57 53 56 sylan 
 |-  ( ( ( A C_ RR /\ y e. A ) /\ x e. RR ) -> ( -. x <_ y -> y <_ x ) )
58 57 an32s 
 |-  ( ( ( A C_ RR /\ x e. RR ) /\ y e. A ) -> ( -. x <_ y -> y <_ x ) )
59 58 reximdva 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( E. y e. A -. x <_ y -> E. y e. A y <_ x ) )
60 52 59 syl5bir 
 |-  ( ( A C_ RR /\ x e. RR ) -> ( -. A. y e. A x <_ y -> E. y e. A y <_ x ) )
61 60 ralimdva 
 |-  ( A C_ RR -> ( A. x e. RR -. A. y e. A x <_ y -> A. x e. RR E. y e. A y <_ x ) )
62 61 imp 
 |-  ( ( A C_ RR /\ A. x e. RR -. A. y e. A x <_ y ) -> A. x e. RR E. y e. A y <_ x )
63 51 62 sylan2br 
 |-  ( ( A C_ RR /\ -. E. x e. RR A. y e. A x <_ y ) -> A. x e. RR E. y e. A y <_ x )
64 breq1 
 |-  ( y = z -> ( y <_ x <-> z <_ x ) )
65 64 cbvrexvw 
 |-  ( E. y e. A y <_ x <-> E. z e. A z <_ x )
66 65 ralbii 
 |-  ( A. x e. RR E. y e. A y <_ x <-> A. x e. RR E. z e. A z <_ x )
67 63 66 sylib 
 |-  ( ( A C_ RR /\ -. E. x e. RR A. y e. A x <_ y ) -> A. x e. RR E. z e. A z <_ x )
68 mnfxr 
 |-  -oo e. RR*
69 ssel 
 |-  ( A C_ RR -> ( y e. A -> y e. RR ) )
70 rexr 
 |-  ( y e. RR -> y e. RR* )
71 nltmnf 
 |-  ( y e. RR* -> -. y < -oo )
72 70 71 syl 
 |-  ( y e. RR -> -. y < -oo )
73 69 72 syl6 
 |-  ( A C_ RR -> ( y e. A -> -. y < -oo ) )
74 73 ralrimiv 
 |-  ( A C_ RR -> A. y e. A -. y < -oo )
75 74 adantr 
 |-  ( ( A C_ RR /\ A. x e. RR E. z e. A z <_ x ) -> A. y e. A -. y < -oo )
76 peano2rem 
 |-  ( y e. RR -> ( y - 1 ) e. RR )
77 breq2 
 |-  ( x = ( y - 1 ) -> ( z <_ x <-> z <_ ( y - 1 ) ) )
78 77 rexbidv 
 |-  ( x = ( y - 1 ) -> ( E. z e. A z <_ x <-> E. z e. A z <_ ( y - 1 ) ) )
79 78 rspcva 
 |-  ( ( ( y - 1 ) e. RR /\ A. x e. RR E. z e. A z <_ x ) -> E. z e. A z <_ ( y - 1 ) )
80 79 adantrr 
 |-  ( ( ( y - 1 ) e. RR /\ ( A. x e. RR E. z e. A z <_ x /\ A C_ RR ) ) -> E. z e. A z <_ ( y - 1 ) )
81 80 ancoms 
 |-  ( ( ( A. x e. RR E. z e. A z <_ x /\ A C_ RR ) /\ ( y - 1 ) e. RR ) -> E. z e. A z <_ ( y - 1 ) )
82 76 81 sylan2 
 |-  ( ( ( A. x e. RR E. z e. A z <_ x /\ A C_ RR ) /\ y e. RR ) -> E. z e. A z <_ ( y - 1 ) )
83 ssel2 
 |-  ( ( A C_ RR /\ z e. A ) -> z e. RR )
84 ltm1 
 |-  ( y e. RR -> ( y - 1 ) < y )
85 84 adantl 
 |-  ( ( z e. RR /\ y e. RR ) -> ( y - 1 ) < y )
86 76 ancri 
 |-  ( y e. RR -> ( ( y - 1 ) e. RR /\ y e. RR ) )
87 lelttr 
 |-  ( ( z e. RR /\ ( y - 1 ) e. RR /\ y e. RR ) -> ( ( z <_ ( y - 1 ) /\ ( y - 1 ) < y ) -> z < y ) )
88 87 3expb 
 |-  ( ( z e. RR /\ ( ( y - 1 ) e. RR /\ y e. RR ) ) -> ( ( z <_ ( y - 1 ) /\ ( y - 1 ) < y ) -> z < y ) )
89 86 88 sylan2 
 |-  ( ( z e. RR /\ y e. RR ) -> ( ( z <_ ( y - 1 ) /\ ( y - 1 ) < y ) -> z < y ) )
90 85 89 mpan2d 
 |-  ( ( z e. RR /\ y e. RR ) -> ( z <_ ( y - 1 ) -> z < y ) )
91 83 90 sylan 
 |-  ( ( ( A C_ RR /\ z e. A ) /\ y e. RR ) -> ( z <_ ( y - 1 ) -> z < y ) )
92 91 an32s 
 |-  ( ( ( A C_ RR /\ y e. RR ) /\ z e. A ) -> ( z <_ ( y - 1 ) -> z < y ) )
93 92 reximdva 
 |-  ( ( A C_ RR /\ y e. RR ) -> ( E. z e. A z <_ ( y - 1 ) -> E. z e. A z < y ) )
94 93 adantll 
 |-  ( ( ( A. x e. RR E. z e. A z <_ x /\ A C_ RR ) /\ y e. RR ) -> ( E. z e. A z <_ ( y - 1 ) -> E. z e. A z < y ) )
95 82 94 mpd 
 |-  ( ( ( A. x e. RR E. z e. A z <_ x /\ A C_ RR ) /\ y e. RR ) -> E. z e. A z < y )
96 95 exp31 
 |-  ( A. x e. RR E. z e. A z <_ x -> ( A C_ RR -> ( y e. RR -> E. z e. A z < y ) ) )
97 96 a1dd 
 |-  ( A. x e. RR E. z e. A z <_ x -> ( A C_ RR -> ( -oo < y -> ( y e. RR -> E. z e. A z < y ) ) ) )
98 97 com4r 
 |-  ( y e. RR -> ( A. x e. RR E. z e. A z <_ x -> ( A C_ RR -> ( -oo < y -> E. z e. A z < y ) ) ) )
99 0re 
 |-  0 e. RR
100 breq2 
 |-  ( x = 0 -> ( z <_ x <-> z <_ 0 ) )
101 100 rexbidv 
 |-  ( x = 0 -> ( E. z e. A z <_ x <-> E. z e. A z <_ 0 ) )
102 101 rspcva 
 |-  ( ( 0 e. RR /\ A. x e. RR E. z e. A z <_ x ) -> E. z e. A z <_ 0 )
103 99 102 mpan 
 |-  ( A. x e. RR E. z e. A z <_ x -> E. z e. A z <_ 0 )
104 83 15 syl 
 |-  ( ( A C_ RR /\ z e. A ) -> z < +oo )
105 104 a1d 
 |-  ( ( A C_ RR /\ z e. A ) -> ( z <_ 0 -> z < +oo ) )
106 105 reximdva 
 |-  ( A C_ RR -> ( E. z e. A z <_ 0 -> E. z e. A z < +oo ) )
107 103 106 mpan9 
 |-  ( ( A. x e. RR E. z e. A z <_ x /\ A C_ RR ) -> E. z e. A z < +oo )
108 107 27 syl5ibr 
 |-  ( y = +oo -> ( ( A. x e. RR E. z e. A z <_ x /\ A C_ RR ) -> E. z e. A z < y ) )
109 108 a1dd 
 |-  ( y = +oo -> ( ( A. x e. RR E. z e. A z <_ x /\ A C_ RR ) -> ( -oo < y -> E. z e. A z < y ) ) )
110 109 expd 
 |-  ( y = +oo -> ( A. x e. RR E. z e. A z <_ x -> ( A C_ RR -> ( -oo < y -> E. z e. A z < y ) ) ) )
111 xrltnr 
 |-  ( -oo e. RR* -> -. -oo < -oo )
112 68 111 ax-mp 
 |-  -. -oo < -oo
113 breq2 
 |-  ( y = -oo -> ( -oo < y <-> -oo < -oo ) )
114 112 113 mtbiri 
 |-  ( y = -oo -> -. -oo < y )
115 114 pm2.21d 
 |-  ( y = -oo -> ( -oo < y -> E. z e. A z < y ) )
116 115 2a1d 
 |-  ( y = -oo -> ( A. x e. RR E. z e. A z <_ x -> ( A C_ RR -> ( -oo < y -> E. z e. A z < y ) ) ) )
117 98 110 116 3jaoi 
 |-  ( ( y e. RR \/ y = +oo \/ y = -oo ) -> ( A. x e. RR E. z e. A z <_ x -> ( A C_ RR -> ( -oo < y -> E. z e. A z < y ) ) ) )
118 12 117 sylbi 
 |-  ( y e. RR* -> ( A. x e. RR E. z e. A z <_ x -> ( A C_ RR -> ( -oo < y -> E. z e. A z < y ) ) ) )
119 118 com13 
 |-  ( A C_ RR -> ( A. x e. RR E. z e. A z <_ x -> ( y e. RR* -> ( -oo < y -> E. z e. A z < y ) ) ) )
120 119 imp 
 |-  ( ( A C_ RR /\ A. x e. RR E. z e. A z <_ x ) -> ( y e. RR* -> ( -oo < y -> E. z e. A z < y ) ) )
121 120 ralrimiv 
 |-  ( ( A C_ RR /\ A. x e. RR E. z e. A z <_ x ) -> A. y e. RR* ( -oo < y -> E. z e. A z < y ) )
122 75 121 jca 
 |-  ( ( A C_ RR /\ A. x e. RR E. z e. A z <_ x ) -> ( A. y e. A -. y < -oo /\ A. y e. RR* ( -oo < y -> E. z e. A z < y ) ) )
123 breq2 
 |-  ( x = -oo -> ( y < x <-> y < -oo ) )
124 123 notbid 
 |-  ( x = -oo -> ( -. y < x <-> -. y < -oo ) )
125 124 ralbidv 
 |-  ( x = -oo -> ( A. y e. A -. y < x <-> A. y e. A -. y < -oo ) )
126 breq1 
 |-  ( x = -oo -> ( x < y <-> -oo < y ) )
127 126 imbi1d 
 |-  ( x = -oo -> ( ( x < y -> E. z e. A z < y ) <-> ( -oo < y -> E. z e. A z < y ) ) )
128 127 ralbidv 
 |-  ( x = -oo -> ( A. y e. RR* ( x < y -> E. z e. A z < y ) <-> A. y e. RR* ( -oo < y -> E. z e. A z < y ) ) )
129 125 128 anbi12d 
 |-  ( x = -oo -> ( ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) <-> ( A. y e. A -. y < -oo /\ A. y e. RR* ( -oo < y -> E. z e. A z < y ) ) ) )
130 129 rspcev 
 |-  ( ( -oo e. RR* /\ ( A. y e. A -. y < -oo /\ A. y e. RR* ( -oo < y -> E. z e. A z < y ) ) ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
131 68 122 130 sylancr 
 |-  ( ( A C_ RR /\ A. x e. RR E. z e. A z <_ x ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
132 67 131 syldan 
 |-  ( ( A C_ RR /\ -. E. x e. RR A. y e. A x <_ y ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
133 132 adantlr 
 |-  ( ( ( A C_ RR /\ A =/= (/) ) /\ -. E. x e. RR A. y e. A x <_ y ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
134 50 133 pm2.61dan 
 |-  ( ( A C_ RR /\ A =/= (/) ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
135 pnfxr 
 |-  +oo e. RR*
136 ral0 
 |-  A. y e. (/) -. y < +oo
137 pnfnlt 
 |-  ( y e. RR* -> -. +oo < y )
138 137 pm2.21d 
 |-  ( y e. RR* -> ( +oo < y -> E. z e. (/) z < y ) )
139 138 rgen 
 |-  A. y e. RR* ( +oo < y -> E. z e. (/) z < y )
140 136 139 pm3.2i 
 |-  ( A. y e. (/) -. y < +oo /\ A. y e. RR* ( +oo < y -> E. z e. (/) z < y ) )
141 breq2 
 |-  ( x = +oo -> ( y < x <-> y < +oo ) )
142 141 notbid 
 |-  ( x = +oo -> ( -. y < x <-> -. y < +oo ) )
143 142 ralbidv 
 |-  ( x = +oo -> ( A. y e. (/) -. y < x <-> A. y e. (/) -. y < +oo ) )
144 breq1 
 |-  ( x = +oo -> ( x < y <-> +oo < y ) )
145 144 imbi1d 
 |-  ( x = +oo -> ( ( x < y -> E. z e. (/) z < y ) <-> ( +oo < y -> E. z e. (/) z < y ) ) )
146 145 ralbidv 
 |-  ( x = +oo -> ( A. y e. RR* ( x < y -> E. z e. (/) z < y ) <-> A. y e. RR* ( +oo < y -> E. z e. (/) z < y ) ) )
147 143 146 anbi12d 
 |-  ( x = +oo -> ( ( A. y e. (/) -. y < x /\ A. y e. RR* ( x < y -> E. z e. (/) z < y ) ) <-> ( A. y e. (/) -. y < +oo /\ A. y e. RR* ( +oo < y -> E. z e. (/) z < y ) ) ) )
148 147 rspcev 
 |-  ( ( +oo e. RR* /\ ( A. y e. (/) -. y < +oo /\ A. y e. RR* ( +oo < y -> E. z e. (/) z < y ) ) ) -> E. x e. RR* ( A. y e. (/) -. y < x /\ A. y e. RR* ( x < y -> E. z e. (/) z < y ) ) )
149 135 140 148 mp2an 
 |-  E. x e. RR* ( A. y e. (/) -. y < x /\ A. y e. RR* ( x < y -> E. z e. (/) z < y ) )
150 149 a1i 
 |-  ( A C_ RR -> E. x e. RR* ( A. y e. (/) -. y < x /\ A. y e. RR* ( x < y -> E. z e. (/) z < y ) ) )
151 6 134 150 pm2.61ne 
 |-  ( A C_ RR -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
152 151 adantl 
 |-  ( ( A C_ RR* /\ A C_ RR ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
153 ssel 
 |-  ( A C_ RR* -> ( y e. A -> y e. RR* ) )
154 153 71 syl6 
 |-  ( A C_ RR* -> ( y e. A -> -. y < -oo ) )
155 154 ralrimiv 
 |-  ( A C_ RR* -> A. y e. A -. y < -oo )
156 breq1 
 |-  ( z = -oo -> ( z < y <-> -oo < y ) )
157 156 rspcev 
 |-  ( ( -oo e. A /\ -oo < y ) -> E. z e. A z < y )
158 157 ex 
 |-  ( -oo e. A -> ( -oo < y -> E. z e. A z < y ) )
159 158 ralrimivw 
 |-  ( -oo e. A -> A. y e. RR* ( -oo < y -> E. z e. A z < y ) )
160 155 159 anim12i 
 |-  ( ( A C_ RR* /\ -oo e. A ) -> ( A. y e. A -. y < -oo /\ A. y e. RR* ( -oo < y -> E. z e. A z < y ) ) )
161 68 160 130 sylancr 
 |-  ( ( A C_ RR* /\ -oo e. A ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )
162 152 161 jaodan 
 |-  ( ( A C_ RR* /\ ( A C_ RR \/ -oo e. A ) ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) )