Metamath Proof Explorer


Theorem rexabslelem

Description: An indexed set of absolute values of real numbers is bounded if and only if the original values are bounded above and below. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses rexabslelem.1 𝑥 𝜑
rexabslelem.2 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
Assertion rexabslelem ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rexabslelem.1 𝑥 𝜑
2 rexabslelem.2 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℝ )
3 simp2 ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → 𝑦 ∈ ℝ )
4 nfv 𝑥 𝑦 ∈ ℝ
5 nfra1 𝑥𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦
6 1 4 5 nf3an 𝑥 ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 )
7 2 3ad2antl1 ( ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
8 2 recnd ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
9 8 3ad2antl1 ( ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℂ )
10 9 abscld ( ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
11 3 adantr ( ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥𝐴 ) → 𝑦 ∈ ℝ )
12 7 leabsd ( ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥𝐴 ) → 𝐵 ≤ ( abs ‘ 𝐵 ) )
13 rspa ( ( ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦𝑥𝐴 ) → ( abs ‘ 𝐵 ) ≤ 𝑦 )
14 13 3ad2antl3 ( ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥𝐴 ) → ( abs ‘ 𝐵 ) ≤ 𝑦 )
15 7 10 11 12 14 letrd ( ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥𝐴 ) → 𝐵𝑦 )
16 15 ex ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( 𝑥𝐴𝐵𝑦 ) )
17 6 16 ralrimi ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ∀ 𝑥𝐴 𝐵𝑦 )
18 brralrspcev ( ( 𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 𝐵𝑦 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 )
19 3 17 18 syl2anc ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 )
20 3 renegcld ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → - 𝑦 ∈ ℝ )
21 2 adantlr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
22 simplr ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝑦 ∈ ℝ )
23 absle ( ( 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( - 𝑦𝐵𝐵𝑦 ) ) )
24 21 22 23 syl2anc ( ( ( 𝜑𝑦 ∈ ℝ ) ∧ 𝑥𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( - 𝑦𝐵𝐵𝑦 ) ) )
25 24 3adantl3 ( ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( - 𝑦𝐵𝐵𝑦 ) ) )
26 14 25 mpbid ( ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥𝐴 ) → ( - 𝑦𝐵𝐵𝑦 ) )
27 26 simpld ( ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ∧ 𝑥𝐴 ) → - 𝑦𝐵 )
28 27 ex ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( 𝑥𝐴 → - 𝑦𝐵 ) )
29 6 28 ralrimi ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ∀ 𝑥𝐴 - 𝑦𝐵 )
30 breq1 ( 𝑧 = - 𝑦 → ( 𝑧𝐵 ↔ - 𝑦𝐵 ) )
31 30 ralbidv ( 𝑧 = - 𝑦 → ( ∀ 𝑥𝐴 𝑧𝐵 ↔ ∀ 𝑥𝐴 - 𝑦𝐵 ) )
32 31 rspcev ( ( - 𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 - 𝑦𝐵 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 )
33 20 29 32 syl2anc ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 )
34 19 33 jca ( ( 𝜑𝑦 ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 ) )
35 34 3exp ( 𝜑 → ( 𝑦 ∈ ℝ → ( ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 ) ) ) )
36 35 rexlimdv ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 ) ) )
37 renegcl ( 𝑧 ∈ ℝ → - 𝑧 ∈ ℝ )
38 37 adantl ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - 𝑧 ∈ ℝ )
39 simpl ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → 𝑤 ∈ ℝ )
40 38 39 ifcld ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
41 40 ad5ant24 ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
42 nfv 𝑥 𝑤 ∈ ℝ
43 1 42 nfan 𝑥 ( 𝜑𝑤 ∈ ℝ )
44 nfra1 𝑥𝑥𝐴 𝐵𝑤
45 43 44 nfan 𝑥 ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 )
46 nfv 𝑥 𝑧 ∈ ℝ
47 45 46 nfan 𝑥 ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ )
48 nfra1 𝑥𝑥𝐴 𝑧𝐵
49 47 48 nfan 𝑥 ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 )
50 40 ad5ant23 ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
51 50 renegcld ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
52 simpllr ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → 𝑧 ∈ ℝ )
53 2 ad5ant15 ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
54 max2 ( ( 𝑤 ∈ ℝ ∧ - 𝑧 ∈ ℝ ) → - 𝑧 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
55 39 38 54 syl2anc ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - 𝑧 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
56 38 40 lenegd ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( - 𝑧 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ↔ - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ - - 𝑧 ) )
57 55 56 mpbid ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ - - 𝑧 )
58 recn ( 𝑧 ∈ ℝ → 𝑧 ∈ ℂ )
59 58 adantl ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → 𝑧 ∈ ℂ )
60 59 negnegd ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - - 𝑧 = 𝑧 )
61 57 60 breqtrd ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝑧 )
62 61 ad5ant23 ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝑧 )
63 rspa ( ( ∀ 𝑥𝐴 𝑧𝐵𝑥𝐴 ) → 𝑧𝐵 )
64 63 adantll ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → 𝑧𝐵 )
65 51 52 53 62 64 letrd ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝐵 )
66 65 adantl3r ( ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝐵 )
67 2 ad5ant15 ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
68 simp-4r ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝑤 ∈ ℝ )
69 40 ad5ant24 ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥𝐴 ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
70 rspa ( ( ∀ 𝑥𝐴 𝐵𝑤𝑥𝐴 ) → 𝐵𝑤 )
71 70 ad4ant24 ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝐵𝑤 )
72 max1 ( ( 𝑤 ∈ ℝ ∧ - 𝑧 ∈ ℝ ) → 𝑤 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
73 39 38 72 syl2anc ( ( 𝑤 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → 𝑤 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
74 73 ad5ant24 ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝑤 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
75 67 68 69 71 74 letrd ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝐵 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
76 75 adantlr ( ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → 𝐵 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
77 66 76 jca ( ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → ( - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝐵𝐵 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ) )
78 2 adantlr ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
79 78 3adant2 ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ∧ 𝑥𝐴 ) → 𝐵 ∈ ℝ )
80 40 adantll ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
81 80 3adant3 ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ∧ 𝑥𝐴 ) → if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ )
82 79 81 absled ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ∧ 𝑥𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ↔ ( - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝐵𝐵 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ) ) )
83 82 ad5ant135 ( ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → ( ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ↔ ( - if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ≤ 𝐵𝐵 ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ) ) )
84 77 83 mpbird ( ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) ∧ 𝑥𝐴 ) → ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
85 84 ex ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) → ( 𝑥𝐴 → ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ) )
86 49 85 ralrimi ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) → ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) )
87 brralrspcev ( ( if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ∈ ℝ ∧ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ if ( 𝑤 ≤ - 𝑧 , - 𝑧 , 𝑤 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 )
88 41 86 87 syl2anc ( ( ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ 𝑧 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝑧𝐵 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 )
89 88 exp31 ( ( ( 𝜑𝑤 ∈ ℝ ) ∧ ∀ 𝑥𝐴 𝐵𝑤 ) → ( 𝑧 ∈ ℝ → ( ∀ 𝑥𝐴 𝑧𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) )
90 89 exp31 ( 𝜑 → ( 𝑤 ∈ ℝ → ( ∀ 𝑥𝐴 𝐵𝑤 → ( 𝑧 ∈ ℝ → ( ∀ 𝑥𝐴 𝑧𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) ) )
91 90 rexlimdv ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 → ( 𝑧 ∈ ℝ → ( ∀ 𝑥𝐴 𝑧𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) ) )
92 91 imp ( ( 𝜑 ∧ ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 ) → ( 𝑧 ∈ ℝ → ( ∀ 𝑥𝐴 𝑧𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) ) )
93 92 rexlimdv ( ( 𝜑 ∧ ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 ) → ( ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) )
94 93 imp ( ( ( 𝜑 ∧ ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 ) ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 )
95 94 anasss ( ( 𝜑 ∧ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 )
96 95 ex ( 𝜑 → ( ( ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ) )
97 36 96 impbid ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∀ 𝑥𝐴 ( abs ‘ 𝐵 ) ≤ 𝑦 ↔ ( ∃ 𝑤 ∈ ℝ ∀ 𝑥𝐴 𝐵𝑤 ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑥𝐴 𝑧𝐵 ) ) )