This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrsupsslem

Description: Lemma for xrsupss . (Contributed by NM, 25-Oct-2005)

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

Proof

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