Metamath Proof Explorer

Theorem xrub

Description: By quantifying only over reals, we can specify any extended real upper bound for any set of extended reals. (Contributed by NM, 9-Apr-2006)

Ref Expression
Assertion xrub ⊢A⊆ℝ*∧B∈ℝ*→∀x∈ℝx<B→∃y∈Ax<y↔∀x∈ℝ*x<B→∃y∈Ax<y

Proof

Step Hyp Ref Expression
1 breq1 ⊢x=z→x<B↔z<B
2 breq1 ⊢x=z→x<y↔z<y
3 2 rexbidv ⊢x=z→∃y∈Ax<y↔∃y∈Az<y
4 1 3 imbi12d ⊢x=z→x<B→∃y∈Ax<y↔z<B→∃y∈Az<y
5 4 cbvralvw ⊢∀x∈ℝx<B→∃y∈Ax<y↔∀z∈ℝz<B→∃y∈Az<y
6 elxr ⊢x∈ℝ*↔x∈ℝ∨x=+∞∨x=−∞
7 pm2.27 ⊢x∈ℝ→x∈ℝ→x<B→∃y∈Ax<y→x<B→∃y∈Ax<y
8 7 a1i ⊢A⊆ℝ*∧B∈ℝ*∧∀z∈ℝz<B→∃y∈Az<y→x∈ℝ→x∈ℝ→x<B→∃y∈Ax<y→x<B→∃y∈Ax<y
9 pnfnlt ⊢B∈ℝ*→¬+∞<B
10 breq1 ⊢x=+∞→x<B↔+∞<B
11 10 notbid ⊢x=+∞→¬x<B↔¬+∞<B
12 9 11 imbitrrid ⊢x=+∞→B∈ℝ*→¬x<B
13 pm2.21 ⊢¬x<B→x<B→∃y∈Ax<y
14 12 13 syl6com ⊢B∈ℝ*→x=+∞→x<B→∃y∈Ax<y
15 14 ad2antlr ⊢A⊆ℝ*∧B∈ℝ*∧∀z∈ℝz<B→∃y∈Az<y→x=+∞→x<B→∃y∈Ax<y
16 15 a1dd ⊢A⊆ℝ*∧B∈ℝ*∧∀z∈ℝz<B→∃y∈Az<y→x=+∞→x∈ℝ→x<B→∃y∈Ax<y→x<B→∃y∈Ax<y
17 elxr ⊢B∈ℝ*↔B∈ℝ∨B=+∞∨B=−∞
18 peano2rem ⊢B∈ℝ→B−1∈ℝ
19 breq1 ⊢z=B−1→z<B↔B−1<B
20 breq1 ⊢z=B−1→z<y↔B−1<y
21 20 rexbidv ⊢z=B−1→∃y∈Az<y↔∃y∈AB−1<y
22 19 21 imbi12d ⊢z=B−1→z<B→∃y∈Az<y↔B−1<B→∃y∈AB−1<y
23 22 rspcv ⊢B−1∈ℝ→∀z∈ℝz<B→∃y∈Az<y→B−1<B→∃y∈AB−1<y
24 18 23 syl ⊢B∈ℝ→∀z∈ℝz<B→∃y∈Az<y→B−1<B→∃y∈AB−1<y
25 24 adantl ⊢A⊆ℝ*∧B∈ℝ→∀z∈ℝz<B→∃y∈Az<y→B−1<B→∃y∈AB−1<y
26 ltm1 ⊢B∈ℝ→B−1<B
27 id ⊢B−1<B→∃y∈AB−1<y→B−1<B→∃y∈AB−1<y
28 26 27 syl5com ⊢B∈ℝ→B−1<B→∃y∈AB−1<y→∃y∈AB−1<y
29 28 adantl ⊢A⊆ℝ*∧B∈ℝ→B−1<B→∃y∈AB−1<y→∃y∈AB−1<y
30 18 ad2antlr ⊢A⊆ℝ*∧B∈ℝ∧y∈A→B−1∈ℝ
31 mnflt ⊢B−1∈ℝ→−∞<B−1
32 30 31 syl ⊢A⊆ℝ*∧B∈ℝ∧y∈A→−∞<B−1
33 mnfxr ⊢−∞∈ℝ*
34 30 rexrd ⊢A⊆ℝ*∧B∈ℝ∧y∈A→B−1∈ℝ*
35 ssel2 ⊢A⊆ℝ*∧y∈A→y∈ℝ*
36 35 adantlr ⊢A⊆ℝ*∧B∈ℝ∧y∈A→y∈ℝ*
37 xrlttr ⊢−∞∈ℝ*∧B−1∈ℝ*∧y∈ℝ*→−∞<B−1∧B−1<y→−∞<y
38 33 34 36 37 mp3an2i ⊢A⊆ℝ*∧B∈ℝ∧y∈A→−∞<B−1∧B−1<y→−∞<y
39 32 38 mpand ⊢A⊆ℝ*∧B∈ℝ∧y∈A→B−1<y→−∞<y
40 39 reximdva ⊢A⊆ℝ*∧B∈ℝ→∃y∈AB−1<y→∃y∈A−∞<y
41 25 29 40 3syld ⊢A⊆ℝ*∧B∈ℝ→∀z∈ℝz<B→∃y∈Az<y→∃y∈A−∞<y
42 41 a1dd ⊢A⊆ℝ*∧B∈ℝ→∀z∈ℝz<B→∃y∈Az<y→−∞<B→∃y∈A−∞<y
43 1re ⊢1∈ℝ
44 breq1 ⊢z=1→z<B↔1<B
45 breq1 ⊢z=1→z<y↔1<y
46 45 rexbidv ⊢z=1→∃y∈Az<y↔∃y∈A1<y
47 44 46 imbi12d ⊢z=1→z<B→∃y∈Az<y↔1<B→∃y∈A1<y
48 47 rspcv ⊢1∈ℝ→∀z∈ℝz<B→∃y∈Az<y→1<B→∃y∈A1<y
49 43 48 ax-mp ⊢∀z∈ℝz<B→∃y∈Az<y→1<B→∃y∈A1<y
50 ltpnf ⊢1∈ℝ→1<+∞
51 43 50 ax-mp ⊢1<+∞
52 breq2 ⊢B=+∞→1<B↔1<+∞
53 51 52 mpbiri ⊢B=+∞→1<B
54 id ⊢1<B→∃y∈A1<y→1<B→∃y∈A1<y
55 53 54 syl5com ⊢B=+∞→1<B→∃y∈A1<y→∃y∈A1<y
56 mnflt ⊢1∈ℝ→−∞<1
57 43 56 ax-mp ⊢−∞<1
58 rexr ⊢1∈ℝ→1∈ℝ*
59 43 58 ax-mp ⊢1∈ℝ*
60 xrlttr ⊢−∞∈ℝ*∧1∈ℝ*∧y∈ℝ*→−∞<1∧1<y→−∞<y
61 33 59 60 mp3an12 ⊢y∈ℝ*→−∞<1∧1<y→−∞<y
62 57 61 mpani ⊢y∈ℝ*→1<y→−∞<y
63 35 62 syl ⊢A⊆ℝ*∧y∈A→1<y→−∞<y
64 63 reximdva ⊢A⊆ℝ*→∃y∈A1<y→∃y∈A−∞<y
65 55 64 sylan9r ⊢A⊆ℝ*∧B=+∞→1<B→∃y∈A1<y→∃y∈A−∞<y
66 49 65 syl5 ⊢A⊆ℝ*∧B=+∞→∀z∈ℝz<B→∃y∈Az<y→∃y∈A−∞<y
67 66 a1dd ⊢A⊆ℝ*∧B=+∞→∀z∈ℝz<B→∃y∈Az<y→−∞<B→∃y∈A−∞<y
68 xrltnr ⊢−∞∈ℝ*→¬−∞<−∞
69 33 68 ax-mp ⊢¬−∞<−∞
70 breq2 ⊢B=−∞→−∞<B↔−∞<−∞
71 69 70 mtbiri ⊢B=−∞→¬−∞<B
72 71 adantl ⊢A⊆ℝ*∧B=−∞→¬−∞<B
73 72 pm2.21d ⊢A⊆ℝ*∧B=−∞→−∞<B→∃y∈A−∞<y
74 73 a1d ⊢A⊆ℝ*∧B=−∞→∀z∈ℝz<B→∃y∈Az<y→−∞<B→∃y∈A−∞<y
75 42 67 74 3jaodan ⊢A⊆ℝ*∧B∈ℝ∨B=+∞∨B=−∞→∀z∈ℝz<B→∃y∈Az<y→−∞<B→∃y∈A−∞<y
76 17 75 sylan2b ⊢A⊆ℝ*∧B∈ℝ*→∀z∈ℝz<B→∃y∈Az<y→−∞<B→∃y∈A−∞<y
77 76 imp ⊢A⊆ℝ*∧B∈ℝ*∧∀z∈ℝz<B→∃y∈Az<y→−∞<B→∃y∈A−∞<y
78 breq1 ⊢x=−∞→x<B↔−∞<B
79 breq1 ⊢x=−∞→x<y↔−∞<y
80 79 rexbidv ⊢x=−∞→∃y∈Ax<y↔∃y∈A−∞<y
81 78 80 imbi12d ⊢x=−∞→x<B→∃y∈Ax<y↔−∞<B→∃y∈A−∞<y
82 77 81 syl5ibrcom ⊢A⊆ℝ*∧B∈ℝ*∧∀z∈ℝz<B→∃y∈Az<y→x=−∞→x<B→∃y∈Ax<y
83 82 a1dd ⊢A⊆ℝ*∧B∈ℝ*∧∀z∈ℝz<B→∃y∈Az<y→x=−∞→x∈ℝ→x<B→∃y∈Ax<y→x<B→∃y∈Ax<y
84 8 16 83 3jaod ⊢A⊆ℝ*∧B∈ℝ*∧∀z∈ℝz<B→∃y∈Az<y→x∈ℝ∨x=+∞∨x=−∞→x∈ℝ→x<B→∃y∈Ax<y→x<B→∃y∈Ax<y
85 6 84 biimtrid ⊢A⊆ℝ*∧B∈ℝ*∧∀z∈ℝz<B→∃y∈Az<y→x∈ℝ*→x∈ℝ→x<B→∃y∈Ax<y→x<B→∃y∈Ax<y
86 85 com23 ⊢A⊆ℝ*∧B∈ℝ*∧∀z∈ℝz<B→∃y∈Az<y→x∈ℝ→x<B→∃y∈Ax<y→x∈ℝ*→x<B→∃y∈Ax<y
87 86 ralimdv2 ⊢A⊆ℝ*∧B∈ℝ*∧∀z∈ℝz<B→∃y∈Az<y→∀x∈ℝx<B→∃y∈Ax<y→∀x∈ℝ*x<B→∃y∈Ax<y
88 87 ex ⊢A⊆ℝ*∧B∈ℝ*→∀z∈ℝz<B→∃y∈Az<y→∀x∈ℝx<B→∃y∈Ax<y→∀x∈ℝ*x<B→∃y∈Ax<y
89 5 88 biimtrid ⊢A⊆ℝ*∧B∈ℝ*→∀x∈ℝx<B→∃y∈Ax<y→∀x∈ℝx<B→∃y∈Ax<y→∀x∈ℝ*x<B→∃y∈Ax<y
90 89 pm2.43d ⊢A⊆ℝ*∧B∈ℝ*→∀x∈ℝx<B→∃y∈Ax<y→∀x∈ℝ*x<B→∃y∈Ax<y
91 rexr ⊢x∈ℝ→x∈ℝ*
92 91 imim1i ⊢x∈ℝ*→x<B→∃y∈Ax<y→x∈ℝ→x<B→∃y∈Ax<y
93 92 ralimi2 ⊢∀x∈ℝ*x<B→∃y∈Ax<y→∀x∈ℝx<B→∃y∈Ax<y
94 90 93 impbid1 ⊢A⊆ℝ*∧B∈ℝ*→∀x∈ℝx<B→∃y∈Ax<y↔∀x∈ℝ*x<B→∃y∈Ax<y